当 AI 智能体重写数百万行代码的速度，比人类评审代码的速度快出几个数量级时，会发生什么？
在微软，我们正致力于解决的正是这个问题。
我们正在构建并运行 AI 智能体，去改造世界上规模最大的部分代码库，包括 Windows 和 Azure。我们的工作范围很广：从把一个 4 亿行规模的代码库迁移到新的编译器工具链，到把遗留的 C/C++ 代码现代化为 Rust——并且越来越多地辅以形式化验证。
生成代码正在变成容易的部分，真正的挑战在于知道是否可以信任它。当智能体在数亿行代码中做出修改时，我们如何确保它没有破坏某些微妙的东西？如何保持行为、安全性和架构意图不变？一个工程师小团队，又如何能有信心地为 AI 智能体在如此规模下做出的修改背书？
自 2024 年以来，我们一直在将 AI 智能体与静态分析、测试和形式化验证结合起来，使大规模软件改造变得切实可行且值得信任。
这些问题是我们工作的核心。自 2024 年以来，我们一直在将 AI 智能体与静态分析、测试和形式化验证结合起来，使大规模软件改造变得切实可行且值得信任。
在这个过程中，控制权发生了反转。起初，我们把工作流硬编码好，再把 LLM 当作子例程来调用；到 2025 年 5 月，智能体已经成为比我们流水线更优秀的规划者，我们的工作变成了构建供智能体调用的工具。这些工具中最有价值的，是那些能告诉智能体——以及智能体背后的工程师——某次修改是否正确的工具。
我们正在通过灵活的执行框架（harness）持续更新我们的方法：利用形式化方法、在复杂系统中分解大规模目标，并应对那些拥有庞大复杂代码库的成熟公司所面临的问题。我们也在重新思考人类与智能体的协作方式。尽管模型和智能体框架在不断进步，人类专家的认知负担却在加重。在智能体软件工程中，人类的注意力已成为最稀缺的资源，因此我们设计工具时，力求把它花在最关键的地方。
在智能体软件工程中，人类的注意力已成为最稀缺的资源，因此我们设计工具时，力求把它花在最关键的地方。
这是本系列的第一篇文章，我们将介绍正在构建的东西、学到的东西，以及仍在努力回答的问题。在本文中，我们先介绍正在研究的一些问题，以及把它们联系起来的核心理念。
迁移
想象一下：需要在由数千名工程师维护的数亿行代码中，进行成千上万处同类修改——这就是大规模代码迁移的挑战。生成任何一处单独的修改都很容易，难的是让成千上万处修改都以同样的方式做对：捕捉专家所掌握的知识、验证这些知识，并一致地应用它们——同时不把组织里的每一位工程师都卷入这项工作。
我们把"迁移"定义为：为达成特定工程目标而在整个代码库上实施的变换，例如升级依赖、采用新的编译器、修复静态分析发现的问题，或迁移到新平台。我们的案例研究包括：让整个 Windows 代码库（数亿行代码）增加对 Clang/LLVM 工具链的支持；在各个代码库中修复 CodeQL、PREfast 和 Roslyn 分析器发现的问题；以及将服务从 x86 重定向到 ARM。
我们对运营模式做出了一个审慎的选择：一个非常小的迁移专家团队可以——也应该——驱动一场大规模迁移。我们不把迁移的所有权分散到整个工程组织，而是集中专业知识，并用智能体将其放大。
智能体首先从抽样发现的问题中学习出一个候选知识库。评审智能体针对每一项提出的修复，从正确性、最小化程度、与文件约定的一致性以及可维护性进行打分，其评审结果用于精炼知识库。随后，专家审批的是知识库本身，而不是逐一审批每处修复，再由智能体将知识库应用到整个代码库。人类的反馈仍然必不可少，但我们把它引导到杠杆最高的地方：审批知识，以及处理新奇或模糊的个案。将类似的修复分组评审，也进一步减轻了评审者的认知负担。
语言现代化
世界上许多最关键的软件都是用 C/C++ 这类语言编写的，它们让内存安全缺陷易于引入、难以根除。用 Rust 重写承诺了"构造即安全"——但前提是重写必须精确保留原始代码的行为。在真实系统的规模下，手动重写很少可行；而自动化重写只有在我们可以信任它时才有价值。
我们的工作聚焦于将遗留代码库迁移到 Rust，而模型与智能体的快速进步，正在不断改写"可能"的边界：
| 1 | 2025 年 1 月 生成的 Rust 代码无法通过编译。 |
| 2 | 2025 年 6 月 代码能通过编译，但运行不正确，也无法通过测试。 |
| 3 | 2025 年 9 月 在人工指导下，完成了约 30,000 行可正常工作的翻译。 |
| 4 | 2026 年 2 月起 以高度的自动化对大型代码库进行现代化改造。 |
每一步都在推移瓶颈——从"能编译"到"能通过测试"，再到"在大规模下验证行为"。随着生成能力的提升，挑战变成了：决定要现代化什么，并证明结果是正确的。
我们构建了交互式工具，帮助工程师可视化代码库的模块结构与分层，并决定要现代化哪些组件、以什么顺序进行。随后，我们的工具会同时产出现代化后的代码及其验证策略。
我们发现，按特性（feature）逐个迁移，比逐行翻译整个组件效果更好。特性是用户可见行为的一个单元，可以用场景驱动的测试端到端地验证，每个特性都有自己的验证门。差分测试用于比较源代码与目标代码的行为；而对智能体保密的测试（这样它就无法过拟合）则用来衡量翻译的健壮性。最近，我们已经开始从源代码中提取形式化规范，将其带入目标语言，并使用 Verus 证明现代化后的代码满足这些规范。
规范驱动开发
智能体产出修改的速度已经超过了人们评估修改的速度，而局部上看似合理的代码，仍可能违反架构假设、分布式协议、安全边界或运行不变量。测试能发现其中一部分问题，评审者能发现另一部分，但两者的速度都跟不上智能体产出修改的速度。我们相信答案是让意图显式化。随着智能体编写我们越来越多的代码，开发者的注意力正从"编写代码"转向"管理规范"——用规范来引导智能体并验证其产出。我们正在构建工具，把形式化、可解释的规范置于软件开发生命周期的中心。
我们的第一步，是用智能体从现有代码库中推断出形式化规范（例如 TLA+）。这些规范刻画了并发、容错等关键软件组件的特性。我们使用 TLC 等工具来检查：实现的执行轨迹是否被规范所允许。这为"规范允许实现所观测到的行为"提供了证据；至于规范是否也刻画了系统本应做的事，是一个更难的问题——我们将在下文中再回到这一点。当某条轨迹不被允许时，差异可能指向实现缺陷、不准确的规范，或无效的测试，智能体负责修订出错的那一方。
一旦拥有了规范，我们就让它们发挥作用。规范是"雨天测试用例"的绝佳来源，可以覆盖那些棘手的并发交错与故障场景。我们在小型、有限配置上对候选性质和归纳不变量做模型检查，以便快速发现反例；并使用我们正在构建的 TLA+ 到 F*、TLA+ 到 Lean 的编译器，在 F* 和 Lean 中证明这些性质对所有配置成立。对于遗留（brownfield）代码库，这层由规范、测试用例和性质构成的体系，会成为未来 AI 驱动的修改的护栏。
我们的目标是把形式化方法的力量带给每一位工程师，而不要求他们成为 TLA+ 或形式化验证的专家。工程师负责评审并批准系统必须满足的性质；智能体则负责找到证明这些性质所需的归纳不变量。随着规范日趋完备，它们还可以成为现代化改造的锚点——这正是我们推进 C/C++ 到经 Verus 验证的 Rust 的翻译工作的思路。
待解问题
以下是我们正在努力应对的一些开放问题：
-
我们能信任 AI 编写的规范吗？Can we trust specifications written by AI?当智能体从它要检查的同一份代码中推断出规范时，我们如何知道规范刻画的是系统应该做什么，而不仅仅是系统当前做了什么？
-
我们能否验证功能正确性之外的东西？Can we verify more than functional correctness?智能体能否帮助我们推理安全性、性能和可靠性，而不仅仅是检查代码是否产生预期的输出？
-
工程师最终会不再阅读代码吗？Will engineers eventually stop reading code?如果智能体生成代码、验证工具证明代码满足经过批准的规范，工程师能否不再阅读代码，只在规范的层面上工作？
-
当每个智能体都能修改一切时，代码归谁所有？Who owns code when every agent can change everything?传统的代码所有权假定工程师在相对明确的边界内工作。智能体开发挑战了这一假设，那么取而代之的会是什么？
对我们来说，这些都不是假设性问题，它们正在塑造我们接下来要构建的东西。
我们很乐意听到你在自己工作中的观察、你与我们的分歧，以及你认为最重要的问题。欢迎随时联系我们，分享你的想法。