Microsoft’s SymCrypt Proofs Turn Verified Cryptography Into Routine Engineering

Microsoft Research said on July 13 that it has open-sourced formal, machine-checked proofs showing that new Rust implementations of two cryptographic algorithms inside SymCrypt, the company’s core cryptography library, behave exactly as their published standards require. The proofs cover SHA-3 and ML-KEM, the NIST-standardized post-quantum key encapsulation algorithm, and Microsoft says the verified Rust code is already running in Windows Insider builds today. The release is less interesting as a single research result than as an answer to a harder question: whether formally verified cryptography, long an expensive, hard-to-adopt specialty, can become routine enough to keep pace with a codebase that changes every day. Microsoft’s answer leans on AI agents that draft proofs for humans, checked at the end by a separate, deterministic prover.

What Microsoft Actually Released

In its post, the SymCrypt team describes the release as “verified code, specs, properties, and proofs” for SHA-3 and ML-KEM, built using Rust, the Lean proof assistant, and a Rust-to-Lean translation tool called Aeneas. The team has published an open-sourced SymCrypt branch containing the specifications and proofs alongside the Rust implementations they validate, so outside engineers can inspect the actual proof artifacts rather than take Microsoft’s summary on faith. Microsoft is explicit that this is not a research prototype bolted onto a demo library: SymCrypt is used in Windows, Azure Linux, Xbox, and other Microsoft platforms, and the newly verified ML-KEM and SHA-3 code is already shipping inside Windows Insider builds. Microsoft says it plans to extend the same Rust, Lean, and Aeneas workflow to more Rust-native algorithms across production versions of Windows and Linux.

Why Microsoft Is Rewriting Code That Already Works

The push began more than a year earlier. Microsoft Research announced on June 10, 2025 that it would rewrite SymCrypt, until then written mostly in cross-platform C with hardware-specific intrinsics and assembly, in Rust. The stated reason was blunt: outdated, memory-unsafe C code puts cryptographic libraries at risk of crashes, data corruption, flawed implementations, and side-channel attacks, and Microsoft judged that memory-safe languages like Rust, paired with formal verification tooling, had finally matured enough to use at that scale. SymCrypt already implemented a wide range of algorithms in C, including AES-GCM, SHA, ECDSA, and the newer post-quantum algorithms ML-KEM and ML-DSA. Rewriting a production cryptography library that ships inside Windows is not a decision Microsoft could make lightly, so the 2025 post also introduced Eurydice, a Rust-to-C compiler built by Microsoft Azure Research that compiles directly from Rust’s MIR intermediate language. Eurydice lets Microsoft check generated C code into the SymCrypt repository alongside the original Rust, so customers who build SymCrypt from source but are not ready to adopt a Rust toolchain keep working without changes. The stated long-term goal, in Microsoft’s own words, is “an industrial-grade, Rust-based, FIPS-certified cryptographic library.”

How a Standard Becomes a Machine-Checked Proof

Why Rust Makes This Tractable at All

Formal verification is not new to cryptography, but it has historically been expensive because production crypto code rarely resembles the clean pseudocode in a standards document. Real implementations are optimized, constant-time, and architecture-specific: full of SIMD intrinsics, bit manipulation, and portability layers for different CPUs, none of which appears in the textbook version of an algorithm. Proving that this optimized code still matches the original specification, for every input that satisfies its preconditions, is what formal verification offers that testing alone cannot. Rust helps because its type system enforces what Microsoft calls “aliasing xor mutability”: a discipline where the compiler, not the programmer, guarantees that two mutable references never overlap. Proving that same non-overlap property in C often requires reasoning about external client code the verifier cannot see. That guarantee is why tools built specifically to verify Rust, rather than C, have emerged at all.

Aeneas and Lean Do the Heavy Lifting

Microsoft picked Aeneas, a verification toolchain built by Microsoft Azure Research in partnership with Inria, the French National Institute for Research in Digital Science and Technology, according to the June 2025 announcement. Aeneas translates Rust’s memory model and borrow semantics, including loops and mutable borrows, into a purely functional representation that a proof assistant, in SymCrypt’s case Lean, can reason about directly. Lean’s own project documentation describes this as preserving the semantics of Rust’s borrow system “without requiring reasoning about memory addresses or pointer arithmetic,” which is what let Microsoft draw on Lean’s existing body of mathematical proofs and its active user community instead of building a bespoke logic from scratch. The result, per Microsoft, is two independent layers of assurance stacked on top of each other: Rust’s compiler rules out broad classes of memory-safety bugs before verification even starts, and Lean’s proofs separately establish functional correctness against specifications derived from the standards themselves.

Proving the Code That Actually Ships

The harder problem is that shipping cryptography is not one algorithm; it is one algorithm times every CPU architecture and optimization Microsoft supports. Microsoft’s post addresses this directly under a section on supporting intrinsics and multiple architectures, rather than verifying an idealized version of an algorithm and hoping the optimized build still matches it. That is also why Microsoft frames this as a workflow, not a one-time audit: as engineers change the Rust implementation, the corresponding Lean models and proofs get regenerated and replayed. A broken proof becomes a signal, either the implementation changed in a way that genuinely needs an updated proof, or the change introduced a real discrepancy against the specification. Microsoft describes the shift explicitly: it turns formal verification “from a one-time research artifact into part of the engineering workflow.”

The New Ingredient: Agents That Propose, a Kernel That Decides

What is genuinely new in this release, compared with the original 2025 announcement, is the role AI agents now play. Microsoft says agents are used in two places: translating cryptographic standards into executable Lean specifications, and drafting the proofs and intermediate properties that show the Rust code satisfies those specifications. Neither use is a leap of faith, because Lean’s proof checker is a small, independently trusted kernel: an agent may propose a proof script, but Lean itself verifies whether that proof is actually valid before anything is accepted. Compilation, code extraction, and the final proof-checking step all stay deterministic and non-agentic; only the drafting is delegated. Microsoft frames the economics of that split plainly: work that previously required months of specialist effort can be accelerated dramatically, and the proof engineer’s role shifts from writing every proof by hand toward designing specifications, curating automation, reviewing the resulting theorem statements, and steering agents to complete their proofs.

Why This Reaches Beyond One Library

SymCrypt’s ML-KEM implementation is not an academic exercise. ML-KEM is the algorithm specified in FIPS 203, the key-encapsulation standard NIST finalized in August 2024, letting two parties establish a shared secret key over a public channel using math believed to remain secure even against an adversary with a quantum computer. Every vendor shipping ML-KEM, not just Microsoft, is answering a version of the same question this release addresses: how do you know an optimized, multi-architecture implementation of a newly standardized algorithm actually matches the math, when the algorithm has not had decades of real-world scrutiny the way older public-key systems have? Microsoft’s bet is that formally verified Rust, checked by a trusted kernel rather than relying on specialist manual review alone, is a more scalable answer than auditing by itself, especially for standards this young. If agent-assisted proof drafting holds up as engineering teams add more algorithms, it also chips away at the long-standing argument that formal verification is too slow and specialized for anything but flagship research code, an argument that has kept most production cryptography, at Microsoft and elsewhere, unverified.

What to Watch Next

Microsoft has committed to extending the same Rust, Lean, and Aeneas pipeline to more algorithms across production Windows and Linux, beyond the SHA-3 and ML-KEM code now running in Windows Insider builds. Because the specifications and proofs are open-sourced alongside the code, outside researchers can check Microsoft’s proof artifacts directly instead of trusting a blog post’s summary, which is exactly the kind of scrutiny a newly standardized, still-young algorithm like ML-KEM benefits from. The open question is durability: whether Lean’s trusted-kernel check keeps agent-drafted proofs honest as the SymCrypt team scales this approach from two algorithms to the rest of a library that underpins Windows and Azure, without the human review burden creeping back up as coverage grows.

Sources

• Microsoft Research: Verifying Rust cryptography in SymCrypt, from standards to code
• Microsoft Research: Rewriting SymCrypt in Rust to modernize Microsoft’s cryptographic library
• NIST: FIPS 203, Module-Lattice-Based Key-Encapsulation Mechanism Standard
• Lean Lang: Aeneas, bridging Rust to Lean for formal verification
• GitHub: microsoft/SymCrypt

Featured image: Rust source code with syntax highlighting on a laptop screen, the same language Microsoft is using to rewrite and formally verify SymCrypt’s cryptographic algorithms. Photo by Slashme, CC0 1.0 Universal (CC0) via Wikimedia Commons; cropped, resized, and converted to WebP.