Cryptographic code is the foundation of modern security, and a single arithmetic error or missing bounds check can undermine an otherwise sound design. Microsoft is now addressing this with a verification methodology that combines safe Rust, the Lean proof assistant, and AI agents to produce machine-checked guarantees for the code that protects Windows, Azure, and open-source users worldwide.
The project centers on SymCrypt, Microsoft's open-source cryptographic library. New implementations are being written in Rust, which eliminates broad classes of memory-safety bugs by design, then verified in Lean using the Aeneas toolchain. This dual-layer approach gives both memory safety and functional correctness against specifications derived directly from public standards like NIST.
From Standards to Executable Proofs
The verification pipeline starts with formalizing the algorithm as described in its standard. For the Number Theoretic Transform in ML-KEM, Microsoft's Lean specification mirrors the NIST standard's loop structure, array updates, and mathematical operations closely enough for line-by-line human review. Because the specification is executable, it can be tested against official vectors to catch transcription errors.
Aeneas then translates the Rust implementation into a pure Lean model. Rust's ownership and borrowing discipline are crucial here: they let Aeneas eliminate much of the pointer aliasing and mutation reasoning that makes C verification so expensive. A mutable borrow in Rust becomes an explicit value transformation in Lean, presenting proof engineers with a functional model that is far easier to reason about.
The theorem for the NTT function, for example, states that if the input array satisfies a well-formedness invariant, the Rust implementation returns the same result as the mathematical specification, modulo the conversion between low-level arrays and high-level polynomials.
Hardware and Optimization
Production cryptography cannot ignore hardware. SymCrypt runs across environments from embedded systems to cloud services, and takes advantage of platform-specific instructions when available. The verification methodology handles this by compiling the code for each target architecture (x86-64, aarch64), translating each variant through Aeneas, and merging the models in Lean. This turns static dispatch in Rust into dynamic dispatch in the proof, allowing a single theorem to cover multiple optimized paths.
Intrinsics that manipulate raw pointers or expose platform instructions are modeled with small, carefully reviewed Lean specifications. The surrounding safe Rust code is then verified against those models, keeping the trusted surface narrow while preserving performance.
AI Agents in the Proof Loop
Microsoft is using AI agents at two points in the workflow. First, they assist in translating standards into Lean specifications. Because the resulting specs are executable, aligned to standards, and tested against vectors, they remain auditable even when an agent helped draft them. Second, agents help write and maintain proofs, handling routine obligations like unfolding generated models, applying helper function specifications, and discharging arithmetic. The proof engineer's role shifts from writing every line by hand to designing specifications, curating automation, and steering agents.
This is possible because Lean's small trusted kernel independently verifies every proof an agent proposes. The agent operates on the proof side; the Rust implementation never needs modification to satisfy a proof.
Developer-Facing Verification
To make verification visible to engineers who do not open Lean, Microsoft generates dashboards that summarize theorems in plain terms: preconditions, postconditions, covered functions, trusted models, and remaining assumptions. As Rust code changes, Lean models and proofs regenerate automatically. When a proof breaks, it signals either that the implementation changed in a way needing proof updates, or that the change exposed a real discrepancy with the specification.
The first public release includes complete proofs for Rust ML-KEM and SHA3 code already shipping in Windows insider builds. Microsoft is extending the same workflow to AES-GCM, FrodoKEM, and ML-DSA.
The long-term bet is that formal verification can become part of normal cryptographic engineering rather than a one-time research exercise: code that remains fast, portable, and developer-owned, while carrying machine-checked evidence that it implements the standard it claims to follow.