Microsoft: When AI Rewrites Millions of Lines of Code, Trust Is the Bottleneck
Microsoft says generating code is becoming the easy part of agentic software engineering, and that knowing whether to trust it is the real challenge. In a new post, two corporate vice presidents describe how the company uses AI agents on codebases such as Windows and Azure, backed by static analysis, testing and formal verification.
- Microsoft says AI agents are transforming large codebases including Windows and Azure, such as a 400-million-line toolchain migration.
- The company says generating code is becoming easy, while knowing whether to trust it is the real challenge.
- Migration uses a small expert team that approves a knowledge base, which agents then apply across the codebase.
- For C and C++ to Rust, Microsoft uses feature-by-feature validation, differential testing and Verus proofs.
- It is also inferring formal specifications such as TLA+ from existing code to validate agent changes.
Agents that transform some of the largest codebases
According to Microsoft, it is building and running AI agents that transform some of the world's largest codebases, including Windows and Azure. The work ranges from migrating a 400-million-line codebase to a new compiler toolchain to modernizing legacy C and C++ code into Rust, increasingly backed by formal verification.
The post is written by Sriram Rajamani and Tim Bozarth, both corporate vice presidents at Microsoft. It is the first in a series about what the company is building and what it has learned. Microsoft says it has combined AI agents with static analysis, testing and formal verification since 2024.
The company describes a shift in how the systems are built. It began by hard-coding workflows that called LLMs as subroutines. By May 2025, according to Microsoft, agents had become better planners than its pipelines, and the engineers' job became building the tools that agents call. The most valuable of those tools tell an agent and the engineers behind it whether a change is right.
Migration: a small expert team, amplified by agents
Microsoft defines migration as a transformation applied across a codebase to reach a specific engineering objective, such as upgrading dependencies, adopting a new compiler, remediating static-analysis findings or moving to a new platform. Its case studies include adding support for the Clang/LLVM toolchain across the entire Windows codebase, which spans several hundred million lines of code, fixing findings from CodeQL, PREfast and Roslyn analyzers, and retargeting services from x86 to ARM.
The company has made a deliberate choice about who does the work: a very small team of migration experts should drive a large migration, rather than spreading ownership across the wider engineering organization. The process works in stages:
- Agents learn a candidate knowledge base from sampled findings.
- A reviewer agent scores each proposed fix for correctness, minimality, consistency with file conventions and maintainability.
- Experts approve the knowledge base rather than individual fixes.
- Agents then apply it across the codebase, with reviewer feedback refining the knowledge base at each stage.
Grouping similar fixes for review reduces the load on reviewers further. Microsoft says human attention has become the scarcest resource in agentic software engineering, and that its tools are designed to spend it where it matters most.
Moving legacy C and C++ to Rust
Microsoft notes that languages like C and C++ make memory-safety bugs easy to introduce and hard to eliminate. Rewriting in Rust promises safety by construction, but only if the rewrite preserves exactly what the original code did. At the scale of real systems, a manual rewrite is rarely practical, and an automated one is only useful if it can be trusted.
The company outlines a timeline of progress. In January 2025, generated Rust code did not compile. By June 2025 it compiled but did not run correctly or pass tests. In September 2025 Microsoft had working translations of approximately 30,000 lines, with manual guidance. From February 2026 onward, it says it has been modernizing large codebases with significant automation.
Each step moved the bottleneck, from compiling to passing tests to validated behavior at scale. Microsoft says migrating feature by feature works better than translating a component line by line, because a feature is a unit of user-visible behavior that can be validated end to end with scenario-driven tests. Differential testing compares source and target behavior, and tests held out from the agent measure robustness. Most recently, the company has begun extracting formal specifications from the source, carrying them into the target language and using Verus to prove that the modernized code satisfies them.
Specification-driven development and what it signals
Microsoft argues that agents can produce changes faster than people can assess them, and that locally plausible code can still violate architectural assumptions, distributed protocols, security boundaries or operational invariants. Tests and reviewers catch some problems, but neither keeps pace, the company says. Its answer is to make intent explicit, so that developers' attention shifts from writing code to managing the specifications that guide agents and validate their output.
As a first step, Microsoft uses agents to infer formal specifications, such as TLA+, from existing codebases. Tools like TLC then check that execution traces of the implementation are admitted by the specification. If a trace is not admitted, the cause may be an implementation defect, an inaccurate specification or an invalid test, and agents revise whichever is wrong. The company adds that this shows the specifications admit the observed behavior, while whether they capture what the system is supposed to do is a harder question. It also says it is building a TLA+-to-F* and TLA+-to-Lean compiler to prove properties for all configurations.
For engineering teams, the message from Microsoft is that scaling AI-driven code changes depends on verification tooling and well-placed human review rather than on code generation alone.
