Microsoft researchers describe a methodology for formally verifying cryptographic code written in Rust using the Lean proof assistant together with the Aeneas toolchain. The approach converts cryptographic standards into executable Lean specifications, translates the corresponding Rust implementations into pure Lean models, and produces machine-checked proofs that the code correctly implements those standards. AI agents are used as part of the workflow, helping translate standards into formal specifications and helping draft and maintain proofs, while Lean’s deterministic kernel independently checks the resulting proofs for correctness. Verified code and proofs already cover the SHA-3 and ML-KEM algorithms used in Windows Insider builds, with AES-GCM and ML-DSA planned next.
