Review
Sep 2026
Scaling Verification of Cryptographic Software with Aeneas, Rust, and Lean
This work develops a new methodology for verifying cryptographic software and extends SymCrypt with experimental optimizations and implementations of algorithms such as FrodoKEM, ML-DSA, and HPKE to explore the scalability of writing, adapting, and verifying cryptographic code.
Ho Son, C. Fournet, Jonathan Protzenko et al.
· 0 citations