kani

KaniはRustプログラム向けのビット精度モデルチェッカーであり、model-checking組織の下で開発されている。Rustコードの安全性と正確性の両方を開発者が検査できるように設計されている。 安全性の面では、Kaniは多くの種類の未定義動作を自動的にチェックする。これにより、コンパイラが通常の安全性保証を強制しないRustのunsafeコードブロックを検証する際に特に価値がある。正確性の面では、パニック（Noneに対するunwrap()の呼び出しなど）、算術オーバーフロー、およびアサーション（assert!(...)）または関数コントラクトとして表現されたカスタムの正確性プロパティを自動的にチェックする。 使用方法はテストに似たワークフローに従う。開発者は#[kani::proof]で注釈を付けたハーネスを書き、kani::any()を使って非決定的な入力を作成する。その後Kaniは、すべての有効な入力がパニックや予期しない動作を起こすことなく、仕様を満たす出力を生成することを証明しようと試みる。チュートリアルとリファレンスドキュメントはKani bookで利用できる。 インストールはCargoを通じて行う。cargo install --locked kani-verifierを実行し、続いてcargo kani setupを行う。このツールはLinuxまたはmacOS上のRust 1.58以降をサポートする。GitHub Action（model-checking/kani-github-action）によりCIパイプラインへの統合が可能である。 このプロジェクトはMITライセンスとApache 2.0ライセンスの両方の下で配布されており、Rustプロジェクトのコードを含んでいる。学術的な引用（ASE 2026論文）があり、コントリビューター向けの開発者ドキュメントを提供している。