Microsoft releases verified ML-KEM and SHA-3 code in SymCrypt using Lean and Aeneas

Microsoft has open-sourced a branch of its SymCrypt cryptographic library containing formal specifications and proofs for the Rust implementations of ML-KEM and SHA-3. This release demonstrates a methodology where production algorithms are written in safe Rust and verified against standards-derived Lean models using the Aeneas toolchain.

• The approach uses Aeneas to translate Rust's mid-level representation into pure Lean models, leveraging Rust's ownership rules to simplify reasoning about memory safety.
• Formal specifications are designed to closely mirror public standards like NIST or IETF RFCs, allowing for executable testing against official vectors and line-by-line human review.
• The open-sourced branch includes complete proofs for ML-KEM and SHA-3 code currently used in Windows insider builds, with plans to extend this workflow to AES-GCM, FrodoKEM, and ML-DSA.

This methodology provides two layers of assurance by combining Rust's memory safety guarantees with Lean proofs of functional correctness, aiming to scale formal verification for production cryptographic algorithms.