智能体代码生成改变了工作的基本单位。过去由一位开发者编写并审查一个规模不大的拉取请求；现在，一个智能体可以生成数十种候选实现、跨服务脚手架代码以及自动迁移方案。结果是，产出数量和多样性不断增加，审查范围也随之扩大。团队面临两方面压力：既要提高吞吐量、持续交付功能，又要保障安全、防止回归和供应链问题。本节将说明自动化如何扩大审查范围、审查者为何成为瓶颈，以及哪些岗位受影响最大：发布工程师、安全团队和关键库的维护者。

测试会在选定场景中验证预期行为，最适合防止与测试用例相符的回归。静态分析和代码检查工具能在运行前发现类型错误、内存问题以及许多 API 误用。AI 驱动的代码审查可以大规模协助排查可读性问题、疑似逻辑错误和风格回归，但可能漏掉细微的语义错误，或产生虚构的逻辑。相比之下，形式化验证在提供精确规范后，可以证明所有输入下都满足特定属性。实际应用中：用测试覆盖行为，用静态工具发现结构性问题，用 AI 审查辅助分流，并用证明验证不变量，以及测试无法穷尽覆盖的并发或密码学保证。

形式化方法很强大，但并非万能。它需要精确的规范——这本身就是一项不容小觑的设计工作——而且代码往往必须使用适合证明的子集，或添加带注释的契约。对于 UI 布局问题、性能调优，或依赖模糊现实输入的行为预期，形式化方法的帮助有限。如果团队试图对规模庞大且快速变化的代码库进行全面形式化验证，过度使用证明反而会造成瓶颈。本节将介绍常见陷阱：规范漂移、证明维护成本、与 CI 集成不畅，以及证明所依赖的假设有误却仍让人产生虚假安全感的风险。

采用分层流水线：1）规范优先生成——在要求智能体实现功能前，先编写精确的 API 契约、类型定义和基于属性的测试；2）沙箱合成——在隔离的 CI 运行器中运行智能体，并对生成的模块进行插桩和模糊测试；3）自动化门禁——在人工作审查前，要求通过单元测试、集成测试、基于属性的测试以及 GitHub AI Scan 安全检查；4）有针对性的形式化证明——将证明用于关键不变量（如共识、密码学和授权），或影响范围较大的模块；5）人工验证——让审查者聚焦设计、规范遵循情况和对抗性思维，而不是逐行检查正确性。通过工具集成，让每个步骤都能非阻塞运行，并在拉取请求仪表板中清晰可见。

从小处着手：先在一项关键服务中试点形式化证明，收集指标来衡量缺陷暴露时长和审查时间，并培训 SRE 与安全工程师编写规范和证明框架。设立新岗位或轮值职责，例如证明工程师或验证负责人，帮助将产品需求转化为机器可检查的契约。从长远看，代码验证方式可能分化为两类：大多数代码由快速的概率型工具和人工审查者验证；少数高价值模块则通过形式化证明加固。这种组合既能保持开发效率，又能在最关键的领域大幅降低系统性风险。