Microsoft: Formal Verification of Rust Cryptography in SymCrypt with AI Agents and Lean

Two Layers of Guarantee Instead of One

Formal verification is a mathematical proof that code behaves exactly according to its specification — not just for tested cases, but for every possible input. Microsoft has built a dual protection into SymCrypt, its foundational cryptographic library that underpins Windows, Azure, and other products: the Rust language eliminates an entire class of memory-management errors (memory-safety bugs), while the Lean proof assistant confirms functional correctness — that the algorithm operates exactly as the standard requires.

Lean is a tool that verifies mathematical proofs through its own trusted kernel. Unlike unit tests that cover selected scenarios, a Lean proof covers absolutely all possible inputs. The combination of these two layers makes verified code significantly more robust than the conventional approach.

What Has Already Been Verified?

Microsoft has published verified code for SHA-3, a widely used hashing algorithm, and for ML-KEM — a post-quantum key exchange algorithm standardized by NIST in 2024. ML-KEM is particularly important because it is designed to withstand attacks from quantum computers, which could break RSA and ECDH that currently protect the vast majority of internet traffic.

On the roadmap are AES-GCM (symmetric encryption), FrodoKEM, and ML-DSA — two more post-quantum algorithms. The common denominator of all these algorithms is their complexity and the high cost of error: an implementation flaw in cryptography typically does not cause a program crash, but rather a silent vulnerability that can be exploited.

AI Agents Accelerate Proof Writing

Writing Lean proofs for cryptographic code is slow and demanding. Microsoft uses AI agents to accelerate this process: agents propose proofs that are then independently verified through Lean’s trusted kernel. The key difference from ordinary code generation is that AI output must pass mathematical verification — it is not enough to look correct. This means errors by AI agents cannot go unnoticed.

Integration into SymCrypt makes this approach practically relevant today, not merely an academic experiment. The toolchain Microsoft uses — Aeneas — translates Rust code into a form that Lean can analyze, bridging the gap between production code and formal methods.