websec
Findings and evidence
Microsoft Research describes verification of Rust cryptographic implementations using Aeneas and Lean. Its initial public artifacts cover SHA-3 and ML-KEM, connecting code with specifications derived from standards and making proof results visible to developers.
Why it matters
The scientific contribution is inspectable evidence about specified code properties. Review the theorem, implementation version and assumptions together rather than treating a verified badge as a blanket assurance.
Scope and limits
Functional correctness against a model does not by itself prove every property of a deployed system. Toolchain assumptions, integration and properties outside the theorem remain relevant.
Primary source
Microsoft Research: original publication. Source published 2026-07-13. Brief prepared by websec.gr on 26 September 2026. This is an editorial research summary, not a claim of independent replication.