Here's a 2020 overview of Rust verification tools https://alastairreid.github.io/rust-verification-tools/ https://alastairreid.github.io/rust-verification-tools

Here's a 2020 overview of Rust verification tools https://alastairreid.github.io/rust-verification-tools/ https://alastairreid.github.io/rust-verification-tools/ - it says > Auto-active verification tools > While automatic tools focus on things not going wrong, auto-active verification tools help you verify some key properties of your code: data structure invariants, the results of functions, etc. The price that you pay for this extra power is that you may have to assist the tool by adding function contracts (pre/post-conditions for functions), loop invariants, type invariants, etc. to your code. > The only auto-active verification tool that I am aware of is Prusti. Prusti is a really interesting tool because it exploits Rust’s unusual type system to help it verify code. Also Prusti has the slickest user interface: a VSCode extension that checks your code as you type it! > https://marketplace.visualstudio.com/items?itemName=viper-admin.prusti-assistant https://marketplace.visualstudio.com/items?itemName=viper-ad... Now, on that list, there is also https://github.com/facebookexperimental/MIRAI https://github.com/facebookexperimental/MIRAI that, alongside the crate https://crates.io/crates/contracts https://crates.io/crates/contracts (with the mirai_assertion feature enabled) enables writing code like this #[ensures(person_name.is_some() -> ret.contains(person_name.unwrap()))] fn geeting(person_name: Option<&str>) -> String { let mut s = String::from("Hello"); if let Some(name) = person_name { s.push(' '); s.push_str(name); } s.push('!'); s } And have it checked at compile time that the assertion holds! Which is a bit like Liquid Haskell in capability: https://ucsd-progsys.github.io/liquidhaskell/ https://ucsd-progsys.github.io/liquidhaskell/ ... and now I just noticed that prusti has a crate prusti_contracts that can do the same thing!! https://github.com/viperproject/prusti-dev/blob/master/prusti-tests/tests/verify_overflow/pass/overflow/bisect.rs https://github.com/viperproject/prusti-dev/blob/master/prust... Now I'm wondering which tool is more capable (as I understand, they leverage a SMT solver like Z3 to discharge the proof obligations, right?)