Microsoft scales formal verification for production cryptography using Rust, Lean, and AI agents

Microsoft Research is deploying a novel approach to cryptographic software verification that harnesses Rust's memory safety, the Lean proof framework, the Aeneas toolchain, and AI-driven automation to ensure that cryptographic code provably matches formal specifications. The effort centers on SymCrypt, Microsoft's open-source cryptography library used across Windows, Azure, and other products.

Why formal verification for cryptography matters#

Cryptographic implementations are scrutinized globally because security flaws—even tiny ones—can compromise entire systems. Traditional testing and code audits, while valuable, cannot guarantee correctness across all possible inputs and edge cases. Production cryptographic code is often heavily optimized, uses platform-specific instructions, and employs constant-time implementations to resist timing attacks. This complexity makes human review alone insufficient.

Formal verification addresses this by replacing manual testing with machine-checked mathematical proofs. Rather than assuming code behaves correctly on tested inputs, formal methods establish a precise guarantee: for all inputs meeting the stated preconditions, the implementation produces the correct output.

From standards to executable specifications#

The first step translates a cryptographic standard into a formal Lean specification. Rather than rewrite the algorithm from scratch, researchers map the standard's structure directly into Lean code—keeping loops, variable names, and operations syntactically close to the original. This proximity allows cryptographers and proof engineers to review the specification by comparing it line-by-line with the published standard.

Crucially, the Lean specification is executable. Engineers run it against official test vectors to catch transcription errors and verify it captures the algorithm's intent. For complex operations like the number-theoretic transform (NTT) in ML-KEM, they can prove deeper mathematical properties—ensuring the formal model correctly represents the underlying algebra.

Connecting Rust code to formal proofs#

Rather than requiring developers to rewrite code in a specialized verification language, the methodology verifies the idiomatic, performance-oriented Rust that engineers already write. The Aeneas toolchain translates Rust's memory model into a functional representation in Lean. Rust's ownership and borrowing rules allow Aeneas to eliminate much of the complex reasoning about pointers and aliases that makes verification of C code expensive.