Об этом проекте

Kani — это битово-точный модельный чекер для программ на Rust, разработанный в рамках организации model-checking. Он предназначен для помощи разработчикам в проверке как безопасности, так и корректности кода на Rust. С точки зрения безопасности Kani автоматически проверяет множество видов неопределённого поведения. Это делает его особенно ценным для верификации небезопасных блоков кода в Rust, где компилятор не обеспечивает обычные гарантии безопасности. С точки зрения корректности он автоматически проверяет паники (например, вызов unwrap() на None), арифметические переполнения и пользовательские свойства корректности, выраженные либо в виде утверждений (assert!(...)), либо в виде контрактов функций. Использование напоминает рабочий процесс, похожий на тестирование. Разработчики пишут обвязку, аннотированную с помощью #[kani::proof], и используют kani::any() для создания недетерминированных входных данных. Затем Kani пытается доказать, что все допустимые входные данные дают выходные данные, удовлетворяющие спецификации, без паник и неожиданного поведения. Учебное пособие и справочная документация доступны в книге Kani. Установка выполняется через Cargo: cargo install --locked kani-verifier, после чего выполняется cargo kani setup. Инструмент поддерживает Rust 1.58+ на Linux или macOS. GitHub Action (model-checking/kani-github-action) позволяет интегрировать его в конвейеры CI. Проект распространяется под лицензиями MIT и Apache 2.0 и содержит код из проекта Rust. У него есть академическое цитирование (статья ASE 2026) и документация для разработчиков, желающих внести вклад.