kani-proof

前提条件

証明を書く前に、ツールがインストールされていることを確認してください。

1. Kani： cargo kani --version を実行します。インストールされていない場合：

   cargo install --locked kani-verifier
   cargo kani setup
   

2. リンター（任意ですが推奨）： Node.js が必要です。npx -p @workersio/klint klint で実行します。

Kani による形式検証

Kani は有界モデル検査ツールです。範囲内のシンボリック入力のあらゆる値を探索するため、証明は網羅的です（ファジングのようにサンプリングするわけではありません）。

重要なルール

次のルールに従うと、よくある証明の失敗を防げます。いずれかに違反すると、証明が失敗する可能性が高くなります。

1. 最初の試行では #[kani::unwind] や #[kani::solver] を使わないでください。 どちらのデコレーターも完全に省略してください。「unwinding assertion」エラーが発生した後にのみ #[kani::unwind(N)] を追加し、タイムアウトした場合にのみ #[kani::solver(kissat)] を追加してください。Kani のデフォルト設定は、推測で指定する設定よりうまく機能します。

2. 対象のプロパティはヘルパーメソッド経由ではなく、インラインでアサートしてください。 複数の不変条件を確認したり、コレクションを反復処理したりするメソッドは呼び出さないでください。ループや追加のアサーション、無関係な失敗要因が生じます。構造体のフィールドを直接読み取り、比較を自分で記述してください。

   // WRONG — helper checks more than the target property, adds loops
   assert!(engine.check_all_invariants());
   
   // RIGHT — asserts exactly what you're proving, no extra logic
   assert!(engine.x.get() >= engine.y.get() + engine.z.get());
   

3. まずは kani::assume() による制約を付けずに kani::any() を使ってください。 assume 制約を追加するのは、タイムアウトまたは OOM が発生した後に限ります。制約のないシンボリック値は、範囲を制約した値よりソルバーで扱いやすいことがよくあります。

4. 状態の構築には公開 API のみを使ってください。 コンストラクター、add_user()、deposit() などを使用します。構造体のフィールドに直接値を代入しないでください。到達不可能な状態が作られ、誤検出の失敗につながります。例外は、セッター API がない vault などの最上位フィールドのみです。

5. Box ではなく、スタック割り当てを使ってください。 Box::new(Engine::new(params)) ではなく、let mut engine = Engine::new(params) を使います。Box を使うと、ソルバーのヒープ追跡オーバーヘッドが増加します。

6. 設定パラメーターは小さくしてください。 コンストラクターがループを制御するサイズ／容量パラメーター（例：max_accounts）を受け取る場合は、アナライザーエージェントが見つけた #[cfg(kani)] 定数に合わせて、小さな値（4～8）を渡してください。

ワークフロー

証明を分類する

ワークフローを選ぶ前に、証明を分類してください。

• シンプル： 対象が純粋関数（&mut self なし）である、またはパターンが P7（算術安全性）／P11（既知の不具合を持つ具体例）／安全性／同値性であり、かつ呼び出しグラフにループがなく、かつ複数エンティティの状態構築が不要な場合。
• 標準： それ以外すべて。状態を変更する処理、P1～P6／P8～P10／P12、ループ、複数エンティティの状態などが該当します。

---

シンプルな手順（エージェントの起動なし）

シンプルな証明では、サブエージェントを起動せず、インラインで作業します。

1. 証明を記述する： パターンテンプレートを直接参照します。該当する references/templates/ ファイル（例：P7 なら arithmetic-safety.rs、安全性／同値性なら safety.rs）を読み、適用してください。共有マクロについては references/templates/infrastructure.rs から始めます。

2. インラインでリンターを実行する： リンターを直接実行します。

   npx -p @workersio/klint klint <file>
   

   続行する前に、エラーや警告を修正してください。

3. インラインで検証する： Kani を直接実行します。

   cargo kani --harness <harness_name>
   

   失敗した場合は、失敗の診断に記載されている修正を適用してから、再実行してください。

---

標準の手順（エージェントあり）

コードベースの分析、状態構築、または反復的なデバッグが必要な複雑な証明の場合：

ステップ 1 — コードベースを分析する

references/agents/kani-analyzer-agent.md に従って Explore エージェントを起動します。ループの上限、既存のインフラストラクチャ、状態構築のパターンが返されます。このステップは省略しないでください。

ステップ 2 — 証明を記述する

エージェントの出力を使ってハーネスを記述します。パターン表からパターンを選び、テンプレートについては references/proof-patterns.md を参照してください。テンプレートファイルは references/templates/ にあります。適切なテンプレートを読み、適用してください。共有マクロ（assert_ok!、assert_err!、スナップショット型）については infrastructure.rs から始めます。

ステップ 3 — 証明をリントする

証明を記述した後、cargo kani を実行する前に、references/agents/kani-linter-agent.md に従ってリンターエージェントを起動します。リンターは、23 種類のよくあるアンチパターン（矛盾する assume、unwind の不足、空虚な証明のリスク、過剰な制約のある入力など）を数秒で静的に検出します。これは、数分かかる cargo kani の実行よりはるかに高速です。

• エラー → 検証に進む前に必ず修正します（矛盾する assume、デッドアサーション、ハーネスのパラメーター）
• 警告 → ハング／OOM／空虚な証明を避けるため、修正してください（unwind の不足、シンボリック入力がない、大きな状態空間）
• 提案 → 証明の品質向上のために検討してください（cover の不足、assume の順序）

すべてのエラーを修正し、警告に対処したうえで、ステップ 4 に進む前に、問題がなくなるまでリンターを再実行します。

ステップ 4 — 検証して反復する

リンターで問題がなくなったら、references/agents/kani-verifier-agent.md に従って検証エージェントを起動します。このエージェントは cargo kani を実行し、出力を解析して、構造化された診断結果を返します。

検証エージェントが FAIL を報告した場合：

• unwinding assertion → エラーに示された N を使って #[kani::unwind(N)] を追加します
• OOM → シンボリック範囲を縮小し、設定パラメーターを下げ、Box を削除します
• assertion failed → 失敗したアサーションを確認し、証明ロジックを修正します
• timeout → #[kani::solver(kissat)] を試し、範囲を狭めます
• covers UNSATISFIABLE → 仮定が矛盾しているため、制約を緩めます

反復します。診断結果に基づいて証明を修正し、リンターを再実行してから、検証エージェントを再実行します。検証されていない証明を提出しないでください。

Kani API 全般（コントラクト、スタブ化、具体的な再生、分割検証）については、references/kani-features.md を参照してください。

Kani 固有の概念

空虚でないこと

証明は、何も証明していないのに SUCCESS と報告することがあります。これは、操作が入力に対して常に失敗する、仮定が矛盾している、結果が破棄される、または状態が空／自明であるなどの理由で、アサーションに到達する実行経路がない場合に発生します。

kani::cover!(condition, "message") で検出します。Kani が UNSATISFIABLE と報告した場合、その経路は一度も実行されません。

結果を明示的に処理して防止します。

// VACUOUS — if operation always fails, nothing is checked
if result.is_ok() { assert!(invariant); }

// NON-VACUOUS — proof fails if operation can't succeed
match result {
    Ok(_) => { /* assert properties */ },
    Err(_) => { kani::assert(false, "must succeed"); unreachable!() }
};

矛盾する仮定： すべての経路で assume(false) に到達する場合、またはすべての kani::cover!() チェックが UNSATISFIABLE の場合、kani::assume() の制約が矛盾しています。有効な入力は存在しません。制約を削除し、制約なしの状態から始めてください。

ループのアンワインド

「unwinding assertion」エラーが発生した場合にのみ関係します。N = 最大反復回数 + 1 として、#[kani::unwind(N)] を追加します。呼び出しグラフ内のすべてのループ（対象関数 + 呼び出し先 + コンストラクター）を追跡します。コレクションのサイズを小さくする #[cfg(kani)] 定数がないか確認してください。

パラメーターで決まるループ： コンストラクターが設定パラメーター上でループする場合（例：for i in 0..capacity）、そのパラメーターは小さい値（4～8）でなければなりません。#[cfg(kani)] 定数がある場合は使用してください。

失敗の診断

Kani の出力	修正方法
unwinding assertion	N = ループ回数 + 1 として #[kani::unwind(N)] を追加します
タイムアウト／ソルバーのハング	kani::assume() を追加して範囲を狭めるか、#[kani::solver(kissat)] を試します
VERIFICATION:- FAILED	cargo kani -Z concrete-playback --concrete-playback=print --harness name を使用します
OOM／メモリ不足	状態サイズを小さくし、Box を削除し、シンボリック変数を減らします
すべての経路で assume(false)	kani::assume() の制約を削除します。これらは矛盾しています
VERIFICATION:- SUCCESSFUL	kani::cover!() 文が SATISFIED であること（空虚でないこと）を確認します

反復的なアプローチ： まずはシンプルな状態から始めます（デコレーターなし、制約のない入力、API で構築した状態）。タイムアウト／OOM の場合にのみ制約を追加し、unwinding エラーの場合にのみ unwind を追加し、タイムアウトの場合にのみソルバーを切り替えます。

Kani を使用すべきでない場合

Kani には実際の制限があります。以下の状況では、証明が成功しないことに多くの時間を費やすことになります。

状況	Kani が苦手とする理由	より適したツール
浮動小数点演算	シンボリックな f32/f64 に対応していません	proptest、bolero
非同期コード	ランタイムがモデル化されていません	tokio::test + proptest
ネットワーク／I/O	システムコールをモデル化できません	統合テスト
コントラクトのない深い再帰	展開回数に上限がありません	関数コントラクトまたは proptest
非常に大きな状態（>1000 要素）	ソルバーがタイムアウトします	#[cfg(kani)] で範囲を絞るか、ファジングを使用します

証明パターン

パターンの詳細については、references/proof-patterns.md を参照してください。テンプレートファイルは references/templates/ にあります。適切なテンプレートを読み、必要に応じて調整してください。共通マクロ（assert_ok!、assert_err!、スナップショット型）を含む infrastructure.rs から始めてください。

パターン	使用する場面	証明する内容
保存性	数量を移動、生成、または破棄する場合	会計式が維持されること
フレーム／分離	複数エンティティのシステムで、1 つのエンティティを対象とする場合	対象外のエンティティが変更されないこと
INV の維持	状態を変更する場合	正準不変条件が変更前後で成立すること
エラーパス	入力検証／事前条件	特定のエラーが返され、状態が完全に変更されないこと
単調性	カウンター、タイムスタンプ、累積値	値が一方向にのみ変化すること
冪等性	決済、同期、再計算	2 回適用した結果が 1 回適用した結果と同じであること
算術安全性	数値計算	オーバーフロー／アンダーフロー／ゼロ除算が発生しないこと
アクセス制御	特権操作	権限のない呼び出し元が拒否されること
状態機械	ライフサイクルの遷移	有効な遷移のみが発生すること
帰納的デルタ	コアの会計処理（最も強力な形式）	生のプリミティブでも方程式が成立すること
ライフサイクル／シーケンス	複数ステップにわたるユーザーフロー	連鎖する操作を通じてプロパティが成立すること

ハーネスの骨組み

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

    #[kani::proof]
    // NO #[kani::unwind] — only add after getting unwinding assertion error
    // NO #[kani::solver] — only add after getting timeout
    fn proof_name() {
        // 1. Build state through public API (NOT field mutation)
        // 2. Symbolic inputs: kani::any() with NO kani::assume() bounds
        // 3. Call function, handle result explicitly (no if result.is_ok())
        // 4. Assert ONLY the target property using raw field access
        //    (NOT check_conservation or other aggregate methods)
        // 5. kani::cover!() for non-vacuity
    }
}

コードベースの準備

Explore エージェントが必要な準備を特定します。よくある準備は次のとおりです。

• #[cfg(kani)] const MAX_ITEMS: usize = 4; — コレクションのサイズを小さくします
• Cargo.toml に [workspace.metadata.kani] flags = { tests = true } を追加します
• クレートのルートに #[cfg(kani)] extern crate kani; を追加します

参考ファイル

• references/proof-patterns.md — テンプレートと例を含むパターン一覧
• references/templates/ — 各証明パターンに対応する Rust テンプレートファイル（infrastructure、conservation、frame-isolation、arithmetic-safety、inductive-delta、safety）
• references/kani-features.md — Kani API：コントラクト、スタブ化、具体的な再生、分割検証
• references/invariant-design.md — 階層化された不変条件の設計手法
• references/anchor-verification.md — OtterSec アノテーションを用いた Anchor プログラムの検証
• references/agents/kani-analyzer-agent.md — 証明前のコードベース分析を行う Explore エージェント
• references/agents/kani-linter-agent.md — 静的 lint チェックを行う Explore エージェント（検証前に実行）
• references/agents/kani-verifier-agent.md — 証明後の検証と診断を行う Explore エージェント