also what https://github.com/facebookexperimental/MIRAI https://github.com/facebookexperimental/MIRAI does for rust: you add contracts (preconditions, postcondi

also what https://github.com/facebookexperimental/MIRAI https://github.com/facebookexperimental/MIRAI does for rust: you add contracts (preconditions, postconditions, and invariants) using https://docs.rs/contracts/0.6.0/contracts/ https://docs.rs/contracts/0.6.0/contracts/ and it checks whether they are true here is an example using mirai and contracts: https://github.com/facebookexperimental/MIRAI/blob/master/examples/shopping_cart/src/main.rs https://github.com/facebookexperimental/MIRAI/blob/master/ex... (note: the contracts crate can be used for verifying at runtime as well)