zakrad/certora-prover-skill

Certora Prover (CVL / EVM)

Certora Prover はスマートコントラクトを形式的に検証します。CVL (Certora Verification Language) でプロパティ（ルールや不変条件）を記述し、Prover はそれらをすべての入力と状態について証明するか、具体的な反例（CEX） を返します。

中心的な考え方 — 最初に読んでください:

• テストではなく証明。 単体テストやファジング（少数の入力をサンプリング）とは異なり、Prover はモデルで許容されるすべての入力、呼び出し元、ストレージ状態について記号的推論を行います。
• 完全ではないが健全。 モデル内では違反を見逃しませんが、タイムアウトする可能性があり、仕様が実際に主張する内容しかチェックしません。空/弱い仕様は役に立ちません。
• 「検証済み」= モデル内で、前提条件の範囲内で反例がないこと。 すべての require、サマリー、ループアンロール、楽観的フラグはモデルを狭めます。緑のチェックマークはその前提条件と同じだけの強さしかありません — これを正しく理解することがすべてです。

ワークフロー：ゼロからのアプリ検証

1. インストール + キー。 pip install certora-cli; CERTORAKEY を設定します。（→ references/running-and-config.md）
2. プロジェクト構成。 コントラクトは src/、仕様は certora/specs/、ターゲットごとに .conf ファイルを配置します。（→ references/running-and-config.md）
3. 最初のサニティ/パラメトリックルールを作成。 非常に小さく始めます：任意の関数の後に基本的なプロパティが成立することをアサートするパラメトリックルール（method f）を作成し、ハーネスがコンパイルおよび実行されることを確認します。（→ references/rules-invariants.md、references/spec-patterns-cookbook.md）
4. 実行。 certoraRun MyContract.conf（または .sol/.spec を直接指定）を実行し、レポートリンクを開きます。（→ references/running-and-config.md）
5. レポートを読む。 CEX の呼び出しトレースとストレージを調査し、仕様を修正するか、実際のバグを確認します。（→ references/running-and-config.md、references/debugging-and-timeouts.md）
6. 不変条件 + ゴーストを追加。 実際のプロパティを記述します：誘導不変条件、さらに会計用のゴースト/フック（例：sumOfBalances == totalSupply）。（→ references/rules-invariants.md、references/hooks-and-ghosts.md）
7. 健全性と正気性を強化。 必ず --rule_sanity basic を実行し、すべてのサマリーと前提を見直し、不健全なショートカットを削除するか正当化します。（→ references/soundness-and-approximations.md、references/methods-and-summaries.md）
8. ミューテーションテスト。 Gambit を使用して、ルールが注入されたバグを実際にキャッチすることを確認します — ミュータントを生き残る仕様は前提が強すぎます。（→ references/debugging-and-timeouts.md）

10秒クイックスタート

pip install certora-cli
export CERTORAKEY=<your-key>

// Counter.spec — increment() が値を厳密に増加させることを証明
methods {
    function get() external returns (uint256) envfree;
}

rule incrementIncreases(env e) {
    uint256 before = get();
    increment(e);
    assert get() > before, "increment must increase the counter";
}

certoraRun src/Counter.sol:Counter \
    --verify Counter:certora/specs/Counter.spec \
    --solc solc8.20 \
    --rule_sanity basic \
    --msg "counter increment"

このスキルの使い方 / リファレンスマップ

目の前のタスクに一致するファイルを読んでください：

• references/cvl-language.md — 読むタイミング： CVL 構文が必要な場合：ファイル構造、型（mathint/env/method/calldataarg/storage）、キャストとその健全性、演算子/量化子、require vs assert vs satisfy vs havoc、関数 vs 定義、コントラクトメソッドの呼び出し方（env、envfree、withrevert、lastReverted）。
• references/rules-invariants.md — 読むタイミング： ルール、パラメトリックルール（method f）、satisfy 証人、または preserved ブロックと requireInvariant を使用した誘導不変条件を記述する場合。
• references/methods-and-summaries.md — 読むタイミング： methods ブロックを設定する場合：エントリの種類、envfree/optional、完全なサマリーカタログ + 健全性テーブル、式/ゴーストサマリー、マルチコントラクト設定（using、links、DISPATCHER）。
• references/hooks-and-ghosts.md — 読むタイミング： ストレージをミラーリングするか、会計を証明する必要がある場合：ストレージ/オペコード/トランジェントフック、ゴースト変数/関数、サムゴースト、persistent ゴースト。
• references/running-and-config.md — 読むタイミング： インストール、certoraRun の実行、.conf ファイルの作成、フラグの選択、プロジェクトのレイアウト、Web レポートの解釈に関する場合。
• references/spec-patterns-cookbook.md — 読むタイミング： すぐに使えるレシピが欲しい場合：アクセス制御、「何が変更できるか」、残高合計、単調性、フレーム条件、状態機械、ラウンドトリップ、可換性、リバート条件、単体テストスタイルのルール。
• references/advanced-defi-patterns.md — 読むタイミング： 実際のプロトコルを検証していて、基本的なクックブックでは不十分な場合：ERC4626 ボールト交換レートの単調性（クロス乗算、無料ランチなし、プレビュー境界）、AMM k-不変条件と価値抽出なし、レンディングのソルベンシー/ヘルス/「不良債権なし」とアンチロックアップ活性、報酬ドリフト会計、リエントランシー as CEI、および大規模なロールベースのアクセス制御 — 各イディオムはそれが由来するプロダクションリポジトリ（Morpho/OZ/Aave/Certora）に帰属します。
• references/tooling-and-ecosystem.md — 読むタイミング： Certora を CI（GitHub Actions、キャッシング、PR ゲーティング）に組み込む場合、またはどのツールがプロパティに適しているかを決定する場合：Certora vs Halmos vs Foundry（不変条件/ファズ）vs Echidna の決定ガイド、それぞれを使用すべきトレードオフ。
• references/learning-resources.md — 読むタイミング： さらに深く学びたい、またはオンボーディングする場合：厳選された外部リンク — RareSkills/Certora チュートリアル、公式ドキュメント、トーク、実世界の公開仕様リポジトリ（Morpho、Aave、OpenZeppelin、Compound）の実例。
• references/soundness-and-approximations.md — 読むタイミング： 何を仮定し、何をアサートするかを決定する場合：健全/悲観的 vs 不健全/楽観的、ループ/ハッシュ化/ハボック近似、楽観的フラグファミリー、合格ルールが保証するもの、健全性レビューチェックリスト。
• references/debugging-and-timeouts.md — 読むタイミング： ルールが空虚、低速、または疑わしい場合：--rule_sanity、タイムアウト緩和策（サマリー、分割、範囲制約）、TAC 困難レポート、Gambit ミューテーションテスト、VSCode LSP、「このパスを信頼すべきか？」チェックリスト。
• cheatsheet.md — 読むタイミング： 1ページのクイックリファレンスが欲しい場合：最も使用される CVL キーワード、ルール/不変条件のスケルトン、一般的な certoraRun フラグ、よくある落とし穴。
• examples/ERC20.spec — 読むタイミング： 完全な動作仕様が必要な場合：methods ブロック、残高合計ゴースト+フック、供給不変条件、パラメトリック/整合性/リバート/加法性ルール、ミントアクセス制御。
• examples/ERC20.conf — 読むタイミング： 実行可能な JSON5 conf テンプレートが必要で、すべての一般的なキー（files、verify、solc、packages、optimistic_loop、rule_sanity...）をカバーしている場合。

黄金のルール / よくある落とし穴

• require ≠ リバート。 require は事実を仮定し（モデルを刈り込みます）、コントラクトのリバートをチェックしません。リバートについて推論するには withrevert + lastReverted を使用してください。
• 空性に注意。 過度に制約された require は、入力を生き残らせないため、ルールを簡単に通過させることがあります。必ず --rule_sanity basic を実行してください（advanced を推奨）。
• 楽観的フラグは健全ではありません。 --optimistic_loop、--optimistic_hashing、--optimistic_fallback などは、ケースを仮定して除外します。意図的に使用し、その理由を文書化し、可能であれば必要性を排除することを優先してください。
• filtered よりも preserved を優先。 不変条件の場合、メソッドを黙って除外するのではなく、preserved ブロック（requireInvariant を使用）で仮定をエンコードしてください。
• アキュムレータには mathint を使用。 uint256 の合計やカウンターはオーバーフローして誤った CEX を生成する（または実際の CEX を隠す）可能性があります。無制限の mathint で計算し、境界でキャストしてください。
• パスしたルールは、その前提条件と同じだけの価値しかありません。 すべてのサマリー、リンク、ループ境界、require は証明の穴です。ミューテーションテストを行い、ルールが実際に失敗できることを確認してください。

---

最も使用されるファイル： 適切なレシピについては references/spec-patterns-cookbook.md から、完全な動作仕様を適応させるには examples/ERC20.spec から始めてください。