Safety-Critical Tool Submission: The Kani Rust Verifier #380
Description
What is the name of the tool?
The Kani Rust Verifier
What is a description of the tool, what it does, how it would be used?
From the documentation:
Kani is an open-source verification tool that uses model checking to analyze Rust programs. Kani is particularly useful for verifying unsafe code blocks in Rust, where the "unsafe superpowers" are unchecked by the compiler. Some example properties you can prove with Kani include memory safety properties (e.g., null pointer dereferences, use-after-free, etc.), the absence of certain runtime errors (i.e., index out of bounds, panics), and the absence of some types of unexpected behavior (e.g., arithmetic overflows). Kani can also prove custom properties provided in the form of user-specified assertions. As Kani uses model checking, Kani will either prove the property, disprove the property (with a counterexample), or may run out of resources.
Link to the tool repo or homepage
https://model-checking.github.io/kani/
What is your role/connection to this tool?
Other
Tool category
formal-verification