kani

The Kani Rust Verifier is a bit-precise model checker for Rust. Kani is particularly useful for verifying unsafe code blocks in Rust, where the "unsafe superpowers" are unchecked by the compiler. Kani verifies: * Memory safety (e.g., null pointer dereferences) * User-specified assertions (i.e., assert!(...)) * The absence of panics (e.g., unwrap() on None values) * The absence of some types of unexpected behavior (e.g., arithmetic overflows)