https://aeneasverif.github.io/
AeneasVerif
A verification toolchain for Rust programs
Interface with the rustc compiler for the purpose of program verification
