Microsoft Research· Research / Phi

Verifying Rust cryptography in SymCrypt, from standards to code

How Rust, Lean, Aeneas, and AI agents are helping scale formal verification for production cryptographic algorithms At a glance SymCrypt develops new verified cryptography using Rust, Aeneas, and Lean to provide higher security assurance. We prove that their code safely and correctly implements standard algorithms, notably for post-quantum cryptography. We are releasing verified code, specs, properties, and proofs initially for SHA-3 and ML-KEM. Aeneas allows verifying a large subset of Rust code and provides efficient automation in Lean to support the proof effort. Agents allow scaling automation by writing proofs that are independently-verifiable. Introduction and motivation for formal verification Cryptographic code sits at the foundation of modern computing. It protects operating systems, cloud services, firmware, messaging systems, and the protocols that connect them. Small mistakes can have outsized consequences: a single arithmetic slip, missing bounds check, or incorrect state transition can undermine the security of an otherwise sound design. Testing and auditing remain essential, but they are not enough on their own. …

Announced

13 Jul 2026 16:00 UTC