From Testing to Mathematical Proof
Cryptographic code protects operating systems, cloud services, firmware, and messaging protocols. A single arithmetic error or missing bounds check can compromise security across millions of devices. Microsoft is addressing this with a new verification methodology that combines safe systems programming with machine-checked mathematical proofs, and they are using AI to make the process scalable.
The company's SymCrypt library, which underpins cryptography across Windows and Azure, is being rewritten in safe Rust and formally verified using the Lean proof assistant and the Aeneas toolchain. The first public release includes complete proofs for the Rust implementations of ML-KEM and SHA3, algorithms that are already shipping in Windows insider builds.
Why Rust, Why Lean
The choice of Rust is strategic. Its ownership and borrowing system eliminates broad classes of memory-safety bugs that have historically plagued cryptographic implementations in C. For verification, Rust's disciplined mutation model allows the Aeneas tool to translate Rust's mid-level representation into pure Lean functions, where mutable borrows become explicit value transformations. This eliminates the expensive pointer aliasing reasoning that makes C verification so difficult.
Lean serves as both the specification language and the proof environment. Specifications are written to mirror public standards (NIST specifications, IETF RFCs) as closely as possible, making them auditable by cryptographers who are not proof experts. These specifications are executable, allowing them to be tested against official test vectors to catch transcription errors.
The NTT Example
A concrete example is the number-theoretic transform (NTT) from ML-KEM. The NIST standard describes the algorithm as an in-place transformation over 256 coefficients with three nested loops. The Lean specification follows this structure line for line, using mathematical types that can be tested against known vectors and connected to higher-level theorems about the NTT's algebraic properties.
The Rust implementation uses a mutable borrow to update an array in place. Aeneas translates this into a pure Lean function that explicitly returns the updated array. The verification theorem then states that, for any well-formed input, the Rust function returns exactly the result specified by the standard. This separation of concerns, engineers write idiomatic Rust, verification engineers prove properties about generated models, keeps the proof burden from distorting the production code.
Scaling with Automation and AI
The key to making this practical is automation. Lean's tactic system handles routine proof obligations: symbolic execution, arithmetic, array reasoning, and bit-vector operations. But the real acceleration comes from AI agents.
Microsoft uses agents in two roles. First, they assist in translating standards into Lean specifications. Because the resulting specifications are executable, tested, and mathematically grounded, they can be thoroughly audited even when an agent helped draft them. Second, agents write and maintain proofs. Because Lean independently verifies every proof script, an agent's output is accepted only if the kernel validates it. This means agents can operate autonomously on the proof side without risking the integrity of the production Rust code.
The result is a significant shift in the economics of verification. Work that previously required months of specialist proof engineering can now be accelerated, with human engineers focusing on specification design, automation curation, and theorem review rather than writing every proof step manually.
Hardware and Production Realities
Production cryptography cannot ignore platform-specific optimizations. SymCrypt runs across environments from embedded systems to cloud servers, using SIMD intrinsics and architecture-specific dispatch logic. The verification methodology handles this by compiling the Rust code per target architecture, merging the resulting models in Lean, and modeling intrinsics with small, carefully reviewed specifications. The surrounding safe Rust code is then verified against these models.
Verification results are exposed through automatically generated dashboards that summarize theorems, preconditions, postconditions, and trusted assumptions in developer-facing terms. This makes the guarantees visible to engineers who do not open Lean, and creates a feedback loop where proof breaks signal either implementation changes or real discrepancies with the specification.
The Long-Term Vision
Microsoft's approach aims to resolve a long-standing tension in verified cryptography. The strongest guarantees have historically come from specialized toolchains and generated code that product teams struggle to adopt. By verifying the Rust code that engineers actually write, deriving specifications from public standards, and using AI to scale the proof effort, the company is trying to make formal verification a normal part of cryptographic engineering rather than a post-hoc research exercise.
The open-source release of proof artifacts alongside the Rust implementations they validate makes the methodology transparent and auditable. As SymCrypt extends this workflow to additional algorithms including AES-GCM, FrodoKEM, and ML-DSA, it sets a precedent for how production cryptographic libraries might be built in the post-quantum era: fast, portable, maintainable, and accompanied by machine-checked evidence of correctness.