一行の証明も書かずに Rust コードの正しさを証明できる。その仕事をするのがモデル検査器であり、現時点で Rust に最も実用的なものは AWS が開発した Kani だ。通常の Rust の表明を書けばよい。Kani はそれを数学的な命題に変換し、あり得るすべての入力について検証する。定理証明系も、証明支援系統も、半年も Coq に没頭する必要もない。

問題は、「あり得るすべての入力」は、入力空間が十分小さく、網羅的に調べられる場合にのみ機能するということだ。関数が百万要素の Vec<u8> を受け取る場合、Kani はすべての並び替えを調べるわけではない。指定した境界まで調べるか、ノートパソコンのメモリが尽きるまで実行する。証明は本物だが、有界なものだ。

「証明なき証明」とは何を意味するか

形式的検証とは、通常、Coq のような証明支援系統でプログラムを書き、不変条件を手作業で定義し、ソルバーを戦術的な段階で導くことを意味する。CompCert のような検証済みコンパイラの開発には数年を要した。ほとんどのチームにそんな年月はない。

モデル検査は異なる。通常の Rust を書く。#[kani::proof] と注釈した検証関数を追加する。その中で kani::any() で記号的値を生成し、対象のコードを呼び出して性質を表明する。Kani はコードを論理式にコンパイルし、SMT ソルバーに渡す。ソルバーは、境界内のすべての入力で性質が成り立つことを確認するか、具体的な反例を出力する。

証明を書いたのではない。全称量化子を伴う検証を書いたのだ。証明を書いたのはツールである。

Kani が Rust を論理に変換する仕組み

Kani は有界モデル検査器だ。コードを論理式に展開し、SMT ソルバーに、どの実行経路が表明を違反できるかを問う。ソルバーは変数を記号的に扱う。通常の検証では x に値 5 を与える。Kani の証明では x に、あり得るすべての u32 を表す記号を与える。

以下は自明な例だ。オーバーフローしてはならない関数があり、それを証明したいとする。

// src/lib.rs
pub fn saturating_double(x: u32) -> u32 {
    x.saturating_mul(2)
}

#[cfg(kani)]
mod proofs {
    use super::*;

    #[kani::proof]
    fn check_saturating_double_never_overflows() {
        let x: u32 = kani::any();
        let result = saturating_double(x);
        if x > u32::MAX / 2 {
            assert_eq!(result, u32::MAX);
        } else {
            assert_eq!(result, x * 2);
        }
    }
}

cargo kani を実行すれば、Kani は数秒でこれを検証する。x のあり得る 4,294,967,296 通りすべてを、一つずつ実行することなく検証する。SMT ソルバーは記号的表現から論じ、反例が存在しないと結論づける。

#[cfg(kani)] ガードは、このコードが Kani 下でのみコンパイルされることを意味する。リリースビルドを肥大化させない。

実例：パーサのクラッシュしないことを証明する

オーバーフローは簡単だ。面白いのはデータに依存するケースだ。小さなプロトコルヘッダを解析する関数があり、どんなバイト列を渡しても絶対にパニックしないことを証明したいとしよう。

// src/protocol.rs
#[derive(Debug, PartialEq)]
pub enum ParseError {
    TooShort,
    InvalidVersion,
}

pub struct Header {
    pub version: u8,
    pub length: u16,
}

/// Parse a 4-byte header:
/// - byte 0: version (must be 1)
/// - byte 1: reserved (ignored)
/// - bytes 2-3: length in big-endian
pub fn parse_header(buf: &[u8]) -> Result<Header, ParseError> {
    if buf.len() < 4 {
        return Err(ParseError::TooShort);
    }
    let version = buf[0];
    if version != 1 {
        return Err(ParseError::InvalidVersion);
    }
    let length = u16::from_be_bytes([buf[2], buf[3]]);
    Ok(Header { version, length })
}

#[cfg(kani)]
mod proofs {
    use super::*;

    #[kani::proof]
    #[kani::unwind(5)]
    fn check_parse_header_no_panic() {
        let len: usize = kani::any();
        kani::assume(len <= 8);
        let buf: [u8; 8] = kani::any();
        let _ = parse_header(&buf[..len]);
    }
}

Kani は、parse_header が長さ 0 から 8 のすべての入力バッファに対してパニックしないことを検証する。境界検査、バージョン検査、配列の添え字アクセスをすべて検証する。もし長さの確認を先に行わずに buf[1] と書いていたら、Kani は反例を発見するだろう。1 バイトのバッファで buf[1] が範囲外になるケースだ。

#[kani::unwind(5)] 注釈は、Kani にループを何回展開するかを指示する。この関数にループがないため、これは保守的な値だ。

境界化の問題：モデル検査が壁にぶつかる場所

モデル検査は、境界内では網羅的だ。境界の外では何も言えない。これが根本的なトレードオフだ。

ループが最初の壁だ。Kani はすべてのループを固定回数だけ展開しなければならない。関数が Vec を反復処理し、アンワインド境界を 10 に設定すれば、Kani は長さ 0 から 10 のベクタに対して正しさを証明する。長さ 11 については何も言わない。境界を 1 増やすたびに状態空間が倍加する。アンワインド 50 なら数分で終わるかもしれない。アンワインド 500 なら永久に終わらないかもしれない。

再帰も同様だ。呼び出しごとに論理式が膨張する。深い再帰はメモリ使用量を爆発させる。

データサイズが二番目の壁だ。Kani は固定長配列を得意とする。動的に割り当てられたコレクションは、明示的にサイズを制限しない限り苦手だ。

標準ライブラリが三番目の壁だ。Kani はその多くをモデル化しているが、すべてではない。Kani が理解しないものを呼び出すと、証明は関数定義の欠如により失敗する。

Kani が証明できることと、限界

Kani は、有界なコードにおけるパニック、整数オーバーフロー、表明違反の発見に長けている。暗号プリミティブ、プロトコルパーサ、小さなステートマシンには最適だ。悪い入力一つで大惨事になり、かつコードが自然に有界な場所だ。

Kani は活性などのライブネス性質の証明には向かない。「すべての要求が最終的に応答を受け取る」という性質は、無限実行についての推論を必要とし、有界モデル検査はあえてそれを行わない。ライブネスには TLA+ のような時間的モデル検査器が必要だ。

Kani はテストの代替でもない。証明が通れば、境界内に反例がないことが分かる。テストが通れば、気に入る特定の入力でコードが正しく動くことが分かる。Kani は思いつかなかった境界値を捕まえる。テストは Kani の見えない統合問題を捕まえる。

ランナーを溶かさずに CI で Kani を回す

小さな関数に対する Kani の証明一つは数秒だ。実際の crate に対するスイートは数分だ。アンワインド境界の高い証明は数時間かかるかもしれない。二時間の SMT 求解を CI パイプラインが待ちたくはないだろう。

Kani の証明は小さく速く保つ。安全上重要な関数、つまりバグがインシデントになる関数を証明する。ウェブフレームワーク全体を証明しようとするな。タイムアウトを設定し、証明ごとにたとえば 5 分とし、タイムアウトは「証明の失敗」ではなく「証明不能」として扱う。

以下は有効な Makefile のパターンだ：

# Makefile
kani:
	cargo kani --only-codegen --output-format=terse
	cargo kani --timeout 300 --all-functions --enable-unstable

kani-fast:
	cargo kani --only-codegen --output-format=terse
	cargo kani --timeout 60 --all-functions --enable-unstable

kani-fast はすべてのプルリクエストで CI を回す。kani は毎晩回す。証明が劣化しても、出荷後ではなく一日以内に気づく。

公開 API を提供する場合、公開関数ごとに完全に記号的な入力で呼び出す Kani 証明を一つ書く。これが形式的契約検証に最も近いものだ。実装が正しいことを証明するわけではないが、任意の正当な入力で実装がクラッシュしないことを証明する。

本物の証明支援系統が必要になる場面

「この連結リストは常に非巡回である」といった、無界なデータ構造に関する性質を証明する必要がある場合、Kani は助けにならない。アンワインド境界が主張を打ち破る。これには Creusot のようなツールが必要だ。Rust を WhyML に翻訳し、証明支援系統を使う。手間はかかるが、無界な構造を扱える。

等価性の証明や未定義動作の検出が必要なら、MIRI や KLEE のようなツールは労力と網羅性のスペクトル上の異なる点に位置する。Kani は「有界なコードがあり、パニックするかどうか知りたい」という場面のスイートスポットだ。パーサ、デコーダ、シリアライザ、設定検証器はすべて該当する。Rust の型システムはすでに多くのバグクラスを排除している。Kani は型システムの届かないものを排除する。

まず試すべきこと

不安を覚える関数がある Rust crate を持っているなら、Kani を追加しよう。不安な関数とは、通常、信頼できない入力を解析したり、ビット操作をしたり、配列に添え字アクセスしたりするものだ。kani::any() で呼び出す証明ハーネスを書く。cargo kani を実行する。通れば、クラッシュしないことの有界な証明を得た。落ちれば、バグ報告になり得た具体的な反例を得た。

新しい言語を学ぶ必要はない。シーケント計算を理解する必要もない。Rust の表明を書き、ソルバーに成り立つかどうかを問えばよい。それは学術的な意味での形式的証明ではない。実用的な意味での機械的証明だ。そしてほとんどのソフトウェアにとって、実用的こそがまさに必要なものだ。

よくある質問

ソフトウェア検証におけるモデル検査とは何か

モデル検査は、指定された性質が成り立つかどうかを確認するため、システムのあり得るすべての状態を網羅的に探索する自動化技法だ。Rust では、Kani のようなツールが有界モデル検査を用い、定義された境界内のすべての可能な入力に対する表明を証明し、手作業での証明構築を不要にする。

Kani は単体検証の作成と何が違うのか

単体検証は特定の入力一つを調べる。Kani の証明は境界内のすべての入力を調べる。Kani の証明が通れば、有界な状態空間内に反例が存在しないことが分かる。証明はより強力だが、設定した境界によって制限される。

Kani は Rust アプリケーション全体の正しさを証明できるか

いいえ。Kani は小さく有界な関数で最も効果を発揮する。状態空間は、ループの反復回数、再帰の深さ、データサイズとともに指数関数的に増大する。パーサやプロトコルハンドラーのような安全上重要なコンポーネントに Kani を使い、アプリケーションレベルの論理には使わないようにしよう。

固定境界のないループに Kani が遭遇するとどうなるか

Kani はループのアンワインド境界を必要とする。ループが境界を超えて実行される可能性がある場合、Kani は失敗するアンワインド表明を挿入する。境界を上げるか、コードを静的に既知の回数に再構成する必要がある。これが有界モデル検査の主な限界だ。