Microsoft verifies Rust crypto in SymCrypt with Lean and AI agents

Microsoft announced the formal verification of Rust-written cryptographic algorithms in SymCrypt, the library used across Windows and Azure. The verification workflow combines safe Rust with Lean (a proof assistant) and the Aeneas toolchain to translate Rust code into Lean. This allows engineers to write machine-checked proofs that the code correctly implements standards like NIST’s SHA-3 and ML-KEM. The first verified release is already shipping in Windows Insider builds, with proofs open-sourced alongside the Rust implementations.

AI agents play a key role in scaling the proof process: they autonomously write intermediate lemmas and proof steps that are then independently verified by Lean’s deterministic checker. This keeps human effort focused on high-level specification and property review. The methodology also preserves performance-oriented implementation choices (constant-time, SIMD, architecture-specific optimizations) because verification works directly on the production code, not an idealized version. Microsoft plans to extend this to AES-GCM, FrodoKEM, and ML-DSA, setting a new standard for provably secure cryptography at scale.