Scaling Verification of Cryptographic Software with Aeneas, Rust, and Lean

Son Ho, Cédric Fournet, Jonathan Protzenko +7

We develop a new methodology for verifying cryptographic software. We target production code written in Rust for performance and system integration, rather than verification conven…