The Kani Rust Verifier
source link: https://model-checking.github.io/kani/
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
The Kani Rust Verifier
Getting started with Kani
Kani is a Rust verification tool based on model checking. With Kani, you can ensure that broad classes of problems are absent from your Rust code by writing proof harnesses, which are broadly similar to tests (especially property tests). Kani is especially useful for verifying unsafe code in Rust, where many of the language's usual guarantees can no longer be checked by the compiler. But Kani is also useful for finding panics in safe Rust, and it can check user-defined assertions.
Project Status
Kani is currently in the initial development phase, and has not yet made an official release. It is under active development, but it does not yet support all Rust language features. (The Book runner can help you understand our current progress.) If you encounter issues when using Kani we encourage you to report them to us.
Kani usually syncs with the main branch of Rust every week, and so is generally up-to-date with the latest Rust language features.
Getting started
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK