Kani is an open-source verification tool that uses model checking to analyze Rust programs. Kani is useful for checking both safety and correctness of Rust code.
unwrap() on None), arithmetic overflows, and custom correctness properties, either in the form of assertions (assert!(...)) or function contracts.Since Kani uses model checking, Kani will either prove the property, disprove the property (with a counterexample), or may run out of resources.
Kani uses proof harnesses to analyze programs. Proof harnesses are similar to test harnesses, especially property-based test harnesses.
Project StatusKani is currently under active development. Releases are published here. Major changes to Kani are documented in the RFC Book. We also publish updates on Kani use cases and features on our blog.
There is support for a fair amount of Rust language features, but not all (e.g., concurrency). Please see Limitations for a detailed list of supported features.
Kani releases every month. As part of every release, Kani will synchronize with a recent nightly release of Rust, and so is generally up-to-date with the latest Rust language features.
If you encounter issues when using Kani, we encourage you to report them to us.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4