Kani: Rust 用モデルチェッカー

Kani は、Rust の所有権型システムでは検証できないプロパティ（unsafe 操作の健全性、機能的正当性、ランタイムパニックの不存在など）に対して形式的な正しさの保証を提供するオープンソースのモデルチェッカーです。Rust の中間表現（MIR）を CBMC のビット精密検証エンジンにコンパイルすることで、Kani はユーザーによる注釈を必要とせずに安全性プロパティを自動的に検証できます。

有界検証と無界検証

Kani は有界モデルチェックと無界検証の 2 つのレベルの検証を提供します。有界モデルチェックでは、ツールがユーザーの介入なしに包括的な安全性プロパティを自動的にチェックできます。無界検証が必要なより複雑なプロパティに対しては、Kani は関数契約、ループ契約、量化子、関数スタブを含む仕様言語を導入しています。

技術的実装

Kani のアーキテクチャは、Rust の中間表現（MIR）から証明ハーネスを ƒBMC ビット精密検証エンジンが使用する論理へとコンパイルします。このプロセスにより、Kani は定義された境界内のすべての入力に対してコードの振る舞いをビット単位で正確に検証でき、unsafe コードにおけるメモリエラー、裸ポインタのデリファレンス、ランタイムパニックをチェックします。

産業応用とスケール

Kani は産業規模の Rust プロジェクトでも実用可能であることが実証されています。具体的な事例では、契約を用いることで検証が単なるパニック回避から完全な機能的正当性へと拡張され、これまで未知だった 6 件のバグが発見されました。

Kani は現在、プロダクション CI 環境でスケールして運用されています。Rust 標準ライブラリの検証キャンペーンにおいて、Kani はコード変更ごとに 16,000 件以上のハーネスを検証し、モダンなソフトウェア開発ワークフローへの大規模統合が可能であることを示しています。

学術的評価

Kani の研究は第 39 回 IEEE/ACM International Conference on Automated Software Engineering (ASE 2026) の Industry Showcase Track で採択されました。