Verifying Rust Cryptography in SymCrypt, from Standards to Code

Microsoft Research describes a formal-verification workflow for SymCrypt that connects cryptographic standards to production Rust code. The approach combines Rust, the Aeneas translation and verification framework, and Lean proofs. Microsoft says it is initially releasing verified code, specifications, properties, and proofs for SHA-3 and ML-KEM, a post-quantum cryptographic algorithm. AI agents are used to scale proof construction while keeping the resulting proofs independently checkable. The work targets stronger assurance for implementations used in operating systems, cloud services, firmware, messaging, and network protocols.