Scaling Rust Verification

The AeneasVerif organization is an umbrella for Rust verification projects. Its flagship project is Aeneas (pronunced [Eh-nee-as]), a toolchain to verify Rust programs in a variety of proof assistants, with Lean as its main backend.