kani README

The project's README from github.com/model-checking/kani. As one markdown file: README.md.

Kani regression Nightly: CBMC Latest

The Kani Rust Verifier is a bit-precise model checker for Rust.

Kani is useful for checking both safety and correctness of Rust code.

Installation

To install the latest version of Kani (Rust 1.58+; Linux or Mac), run:

cargo install --locked kani-verifier
cargo kani setup

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():

use my_crate::{function_under_test, meets_specification};

#[kani::proof]
fn check_my_property() {
   // Create a nondeterministic input
   let input: u8 = kani::any();

   // Call the function under verification
   let output = function_under_test(input);

   // Check that it meets the specification
   assert!(meets_specification(input, output));
}

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.

Citing Kani

If you use Kani in your research, please cite our ASE 2026 paper.

ACM Reference Format:

Rémi Delmas, Zyad Hassan, Qinheping Hu, Rahul Kumar, Felipe R. Monteiro, Thanh Nguyen, Adrián Palacios, Celina Val, Michael Tautschnig, Justus Adam, Daniel Schwartz-Narbonne, and Carolyn Zech. 2026. Kani: A Model Checker for Rust. In Proceedings of the 41st IEEE/ACM International Conference on Automated Software Engineering (ASE '26), October 12–16, 2026, Munich, Germany. ACM, New York, NY, USA, 13 pages. https://doi.org/10.1145/3832783.3834499

BibTeX:

@inproceedings{kani-ase-2026,
  author    = {Delmas, R{\'e}mi and Hassan, Zyad and Hu, Qinheping and Kumar, Rahul and
               Monteiro, Felipe R. and Nguyen, Thanh and Palacios, Adri{\'a}n and
               Val, Celina and Tautschnig, Michael and Adam, Justus and
               Schwartz-Narbonne, Daniel and Zech, Carolyn},
  title     = {{Kani}: A Model Checker for {Rust}},
  year      = {2026},
  publisher = {Association for Computing Machinery},
  address   = {New York, NY, USA},
  url       = {https://doi.org/10.1145/3832783.3834499},
  doi       = {10.1145/3832783.3834499},
  booktitle = {Proceedings of the 41st IEEE/ACM International Conference on Automated Software Engineering},
  numpages  = {13},
  location  = {Munich, Germany},
  series    = {ASE '26}
}

The same citation is available in machine-readable form in CITATION.cff, which powers GitHub's Cite this repository button.

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 for details.

Rust

Kani contains code from the Rust project. Rust is primarily distributed under the terms of both the MIT license and the Apache License (Version 2.0), with portions covered by various BSD-like licenses.

See the Rust repository for details.

kani (model-checking/kani)

Searching Database…

3.5K ·GitHub
Kani
Что это такое?Kani — это точный до бита верификатор моделей (model checker) для программ на Rust: вместо перебора случайных входных данных, как это делает набор тестов, он доказывает, что в вашем коде нет определённых видов багов и неопределённого поведения.
Это библиотека, которую я добавляю в свой проект, или отдельный инструмент?Отдельный инструмент с интерфейсом командной строки: ваша программа остаётся как есть, вы лишь добавляете harness-функции, похожие на тесты, а Kani проверяет их на этапе разработки или в CI.
Будет ли он работать на Windows?В официальных инструкциях по установке упомянуты только Linux и Mac — в README про Windows ничего не сказано, так что рассчитывайте на машину с Unix-подобной системой или на CI.
С чего мне начать после установки?В README настоятельно рекомендуют учить Kani по официальному туториалу, а Kani book — это полная документация, включая раздел про GitHub Action для CI.
Чем Kani особенно полезен для unsafe-кода?Компилятор Rust не проверяет гарантии внутри unsafe-блоков, а Kani автоматически проверяет многие виды неопределённого поведения — как раз там, где супервозможности unsafe остаются без проверки.
Kani — это исследовательский проект или инструмент, готовый к продакшену?И то и другое: для реального использования в CI есть официальный GitHub Action, а команда также публикует исследования — академических пользователей просят сослаться на статью о Kani с ASE 2026.
What are similar projects?rust-clippy, perch, openqodex, knip, rector, fallow, golangci-lint, bashka
Which topics is it in?automated-testing, verification, code-analysis, academic, code-quality, static-analysis, github-actions, ci, security-tools, testing, command-line, documentation
Creator
model-checking
Size
36.8 MB
Stars
3.5K
Updated
CommitOct 14Releasekani-0.68.0Sep 16
Age
5y
Commits · 90 Days