Verifying Rust cryptography in SymCrypt, from standards to code

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. 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…