A Lean 4 formal verification of the SymCrypt-Rust implementations of SHA-3/SHAKE (FIPS 202) and ML-KEM (FIPS 203), using the Aeneas Rust-to-Lean pipeline to prove every public function, including SIMD fast paths, correct against audited specifications of the NIST standards.
Want to contribute? Help formally verify SymCrypt — verified SymCrypt-Rust SHA-3 and ML-KEM. Click on the button to view remaining issues on GitHub.
This table shows the verification status of all functions in the project. Click on a function to see more details.
