{"repo":"model-checking/kani","free":true,"listed":false,"github":"https://github.com/model-checking/kani","clone":"git clone https://github.com/model-checking/kani.git","description":"Kani Rust Verifier","language":"Rust","stars":3329,"topics":["rust","model-checking","verification"],"license":"Apache-2.0","category":"dev-tools","readme_excerpt":"The Kani Rust Verifier is a bit-precise model checker for Rust. Kani is useful for checking both safety and correctness of Rust code. - Safety : Kani automatically checks for many kinds of undefined behavior. This makes it particularly useful for verifying unsafe code blocks in Rust, where the \"unsafe superpowers\" are unchecked by the compiler. - Correctness : Kani automatically checks panics (e.g. unwrap() on None ), arithmetic overflows, and custom correctness properties, either in the form of assertions ( assert!(...) ) or function contracts. Installation To install the latest version of Kani (Rust 1.58+; Linux or Mac), run: See the installation guide for more details. How to use Kani Similar to testing, you write a harness, but with Kani you can check all possible values using kani::any() : Kani will try to prove that all valid inputs produce outputs that satisfy the specification, without panicking or exhibiting unexpected behavior. This example is simple; we highly recommend following the tutorial to learn more about how to use Kani. GitHub Action Use Kani in your CI with model-checking/kani-github-action@VERSION . See the GitHub Action section in the Kani book for details. Security See SECURITY for more information. Contributing If you are interested in contributing to Kani, please take a look at the developer documentation. License Kani Kani is distributed under the terms of both the MIT license and the Apache License (Version 2.0). See LICENSE-APACHE and LICENSE-MIT ","default_branch":null,"files":null,"tree":[],"storefront":"/r/model-checking","claimed":false,"request_supported":{"post":"https://gitbuyer.com/r/model-checking/kani/request-supported","requests":0},"note":"indexed from public GitHub; nothing is for sale on this page. Clone it from GitHub. Paid listings live at /search."}