不変条件テストの書き方｜Foundry・Echidnaで単体テストが見逃すバグを探す

ある開発チームが、預けた資産を運用する保管庫（vault）のコントラクトを作っています。入金、引き出し、手数料の計算。関数ごとの単体テストは全部通りました。ところが、別々の利用者が入金と引き出しを特定の順番で重ねると、保管庫の残高と帳簿の数字が少しずつ合わなくなります。

このバグは、操作が積み重なった先で起きます。1回の関数呼び出しを調べるテストでは、長い操作列や利用者どうしの状態までは扱えません。

こうしたバグを探すのが不変条件テストです。「どんな順番で操作しても、これだけは崩れてはいけない」という関係を書いておきます。ツールが複数の利用者と操作順を自動で作り、そのたびに関係が保たれているかを調べます。

崩れる操作列（反例）が見つかったら、それを再現できる回帰テストとして残します。単発の関数テストの穴を、こうして埋めていきます。

以下では、この保管庫を例に、FoundryとEchidnaに共通するテストの組み立て方を4つの手順で追います。

1. 業務上、失ってはいけない価値を決める
2. それを、テストで確かめられる式にする
3. 操作する利用者・呼ぶ関数・入力の範囲を、Handlerという仲介役にまとめる
4. 見つかった反例を、毎回同じ結果になる回帰テストとして残す

何を「壊れてはいけない関係」にするか

不変条件テストが調べるのは、書いておいた関係だけです。書かなかった性質は調べられません。ですから、ツールを選ぶより先に、何が崩れたら困るかを決めます。

不変条件は、今の実装の値を言い換えたものではありません。利用者資産、会計、権限などについて、仕様として常に成り立つべき関係です。候補には次のようなものがあります。

• ERC-20の総供給量と、全口座の残高の合計
• ERC-4626保管庫の資産と持分
• 貸付の担保と債務、ブリッジのロック量と発行量

考える観点は4つあります。前半の表では、観点ごとの問いと式の例を示します。

それぞれに見落としやすい条件があります。

• 会計保存：手数料、丸め、寄付、未実現損益
• 権限：代理呼び出し、ロール移管、初期化
• 状態機械：同一ブロック、期限の境目、部分実行
• 利用者保護：流動性不足、待ち行列、外部依存の停止

ただし、条件の中には、バグを見分ける力のないものもあります。

• 弱い例：「残高が0以上」。型だけで必ず成り立つ
• 弱い例：テスト対象の実装と同じ計算で期待値を出す。同じ誤りを二度書くだけになる
• 強い例：仕様、独立した簡易モデル、保存則、単調性、上限・下限から導いた条件

つまり「実装とは別の理由で正しいと説明できる条件」を選びます。こうした判定の拠り所を、テストの世界ではテストoracleと呼びます。

不変条件は「何を見るか・どの操作で変わるか・例外は何か」で書く

「保管庫は支払能力を保つ」だけでは、テストになりません。何を足すのか、どの時点で見るのか、どんな例外を許すのかが決まっていないからです。

そこで条件ごとに、次の3つを書き出します。

• 見る状態
• その状態を変える操作
• 許す例外

チェーン上の値だけで判定できないこともあります。そのときは、入出金の累計などをHandler側のghost variableで記録します。保管庫の会計条件なら、次のように書けます。

Invariant ID: VAULT-ACCOUNTING-01
Scope: deposit / mint / withdraw / redeem / fee accrual
Actors: depositor, receiver, fee recipient
Predicate: assets_out + current_assets + recognized_fees
           >= assets_in - bounded_rounding_loss
Exceptions: documented emergency loss realization only
Evidence: seed, call sequence, sender, calldata, pre/post state

丸め誤差は、何でも許す幅にしません。操作回数や小数の桁数から導ける上限にします。

外部の価格情報（オラクル）や、フォーク上の流動性に頼る条件もあります。フォークとは、本番チェーンのある時点の状態を手元に写して動かすことです。この場合は、次の扱いも固定しておきます。

• 値を取ったブロック、価格の鮮度
• 代わりの取得手段（fallback）
• チェーン再編が起きたときの扱い

固定しないと、コントラクトの欠陥なのか、テスト環境の変動なのかを見分けられません。

どの利用者が、どの順で操作するかを作る

検査式が正しくても、調べたい状態までテストが進まなければ反例は見つかりません。

まず業務の流れを状態機械として描きます。遷移ごとに書き出すのは次のことです。

• その遷移を起こす操作者と、前提条件
• 成功した後の状態
• revert（取り消し）したときに変わってはいけない状態

保管庫なら、操作と操作者は次のとおりです。

boundは、ランダムな入力を指定の範囲に収めるFoundryの関数です。

Foundryの不変条件テスト（Invariant Testing）は、指定したコントラクトと関数へのランダムな呼び出し列を作ります。既定では、呼び出しのたびにinvariant_*関数を評価します。間隔はcheck_intervalで変えられます。

公式ドキュメントでは、runsが作る列の数、depthが1列の中の呼び出し数です。この値をただ増やす前に、測るものがあります。重要な遷移が呼ばれた回数、revert率、たどり着いた状態です。

Handlerの役目は、意味のある操作の割合を増やすこと

複雑なプロトコルに何も工夫せずランダムな関数呼び出しを浴びせると、「approveしていない」「残高が足りない」「呼び出し元が違う」といった理由で大量に失敗します。テストは入口で足踏みし、本当に調べたい深い状態までたどり着けません。

そこでHandlerに、次の仕事を任せます。

• 操作者の切り替え
• 入力のboundと、必要な前処理
• ghost variableの更新

こうして、実際の運用で意味のある操作列の割合を増やします。入金のHandlerは次のようになります。

contract VaultHandler is Test {
    Vault public vault;
    ERC20 public asset;
    address[] internal actors;
    uint256 constant MAX_OPERATION = 1e24;
    uint256 public ghostDeposited;
    uint256 public ghostWithdrawn;

    function deposit(uint256 actorSeed, uint256 amount) external {
        address actor = actors[actorSeed % actors.length];
        amount = bound(amount, 1, MAX_OPERATION);
        deal(address(asset), actor, amount);
        vm.startPrank(actor);
        asset.approve(address(vault), amount);
        uint256 before = asset.balanceOf(actor);
        vault.deposit(amount, actor);
        ghostDeposited += before - asset.balanceOf(actor);
        vm.stopPrank();
    }
}

ただし、Handlerが本体と同じ分岐を書き直すと、同じ誤解を二重に書くだけです。追跡する値は、観測した事実から更新します。たとえば「実際に移動した資産」「呼び出しが成功した回数」です。期待値を本体の内部計算に頼らせません。

上の例も、入金の前後の残高差から、実際に移動した量を記録しています。

入力の絞り方にも差が出ます。vm.assumeは条件に合わない入力を捨てる関数です。これで大量に捨てるより、boundや今の状態から有効な範囲を作る方が、探索の効き具合を確かめやすくなります。

テストの対象範囲も、はっきり書いておきます。

• Foundryでは、forge-stdのtargetContract・targetSender・targetSelectorで、対象のコントラクト・呼び出し元・関数を指定できる。除外用のexclude*もある
• EchidnaはABIをもとに呼び出し列を作り、反例を最小化できる

管理関数、テスト用の設定関数、依存コントラクトを黙って対象に入れると、現実にはありえない状態を作ってしまいます。対象に入れた理由と外した理由は、テストコードに残します。

「PASS」をそのまま信じないために何を見るか

Foundryの既定設定はfail_on_revert = falseです。呼び出しがrevertしても、探索全体（campaign）は失敗になりません。その間もdepthは消費されます。

ですから「PASS」の表示だけで安心してはいけません。次の数字もあわせて見ます。

• 関数セレクタごとの呼び出し数とrevert数（show_metricsで表示）
• たどり着いた状態
• 探索にかかった時間

revert率が高いときは、その中身を3種類に仕分けます。

• 期待されたrevert：権限のない操作者、上限超過、期限後の操作など。拒否すること自体が仕様である。
• 探索を妨げるrevert：approveや残高の準備が足りず、本来試したい本体ロジックへ届いていない。Handlerの前提作りを直す。
• 欠陥を示すrevert：仕様では成功すべき退出・清算・精算が、特定の操作列でできなくなる。

反例が出たら、どう残すか

反例が出たら、次の情報を保存します。Foundryは、失敗した操作列を保存して再実行できます。

• シード値と、最小化された操作列
• 呼び出し元、calldata、初期状態
• ツールのバージョン

直す前に、同じ列を毎回同じ結果になる単体テストか回帰テストに移します。直した後は、2つのことを確かめます。その反例が消えたこと。広く探索し直しても、別の反例が出ないことです。

シード値を変えて反例を見えなくするだけ、というやり方は禁物です。

不変条件テストで分かること、分からないこと

検証の手法ごとに、答えられる問いが違います。そのため不変条件テストは、ほかの手法の代わりにはなりません。

それぞれの手法について、不変条件テストでは代わりが利かない点は次のとおりです。

• 単体テスト：意図した全分岐を明示して確かめること
• 単発のファズテスト：長い操作列と、操作者どうしの間の状態
• 不変条件テスト：探索しなかった状態についての完全な証明
• 形式検証：モデル・仕様そのものの正しさ
• 監査・レビュー：継続的な回帰の検知と本番の監視

不変条件テストは、ランダムな探索か、網羅率を手がかりにした探索（coverage-guided）です。すべての状態を数え上げる安全証明ではありません。しかも、書かなかった性質は調べられません。

外部プロトコル、アップグレード、署名者、フロントエンド、オラクル障害などは、ほかの手段に任せます。統合テスト、フォークテスト、形式検証、監査、運用監視です。形式検証をどこまで足すべきかはスマートコントラクトの形式検証｜採用すべき範囲と判断基準で扱っています。

CIでは短い回帰テストと長い探索を使い分ける

プルリクエストのたびに同じ短い設定だけを回すと、再現はしやすくなります。その代わり、深い操作列はなかなか探せません。そこで、場面ごとに回し方を変えます。

• プルリクエスト：固定シードを含む短時間の探索と、既知の反例の回帰テスト
• 夜間実行・リリース候補：runs・depth・タイムアウトを増やし、複数のシードと、Echidnaなど別のエンジンを併用

あわせて、CIで次のことをそろえておきます。

• コンパイラ、EVMバージョン、依存ライブラリ、フォークするブロック、Foundry/Echidnaのバージョンを固定する。
• 不変条件ID、対象セレクタ、操作者、runs、depth、シード、revert率、網羅率、所要時間を成果物として保存する。
• 失敗時の最小の操作列をCIから取り出せるようにする。機密のRPC URLや鍵は出力しない。
• 重大な会計・権限の条件を消したり弱めたりする変更を、普通のテスト修正に紛れさせない。
• アップグレードでは、旧実装から引き継いだ状態を初期状態にする。ストレージレイアウトと、移行後の不変条件を調べる。

本番の監視に、同じ条件を使う

本番では、同じ不変条件をそのままチェーン上で動かせないことがあります。それでも条件IDと意味は共有できます。イベント、状態のスナップショット、会計の突き合わせ、アラートに置き換えれば、開発時に確かめた条件と本番の監視がつながります。

監視と緊急停止の設計はスマートコントラクト本番運用の記事で詳しく扱っています。

導入・リリースの前に確かめること

• 利用者資産、会計、権限、状態機械について、不変条件IDと根拠がある。
• 各条件に、見る状態、対象の操作、操作者、例外、許容誤差が書いてある。
• Handlerの追跡値が、本体ロジックの写しではなく、観測した事実から更新される。
• 重要な正常系と拒否系のセレクタが呼ばれ、revert率とたどり着けなかった状態を説明できる。
• 失敗時にシード、最小の操作列、初期状態、バージョンを保存し、毎回同じ結果になるテストに移せる。
• プルリクエスト、夜間実行、リリース候補で、探索の時間・シード・エンジンを変えている。
• フォークや外部依存を使う場合、ブロックと依存先の状態を再現できる。
• 不変条件テストで保証できない範囲を、単体テスト、形式検証、監査、運用監視に割り振っている。

これを満たさずにrunsやdepthだけを増やしても、意味のない状態を長く探すだけになりかねません。監査の工程やほかの検証手法も含めた計画は、スマートコントラクト監査の工程と費用目安も参照してください。

XTELAができること

私たちは、スマートコントラクトの業務要件と状態遷移を整理し、不変条件、操作者、Handler、ghost variable、CI、フォーク環境、監視ルールへ落とす設計・PoC・開発を行います。不変条件テストだけで安全性を保証するのではなく、コードレビュー、監査、権限設計、リリース後の監視と組み合わせて検証計画を組みます。貴社のプロトコルで検証範囲を整理したい場合はお問い合わせからご相談ください。

主要参考資料

• Foundry: Invariant Testing（実行モデル、runs/depth、対象指定、Handler、ghost variable。2026年9月24日確認）
• foundry-rs/forge-std（Foundryテスト用標準ライブラリ。対象指定関数を2026年9月24日確認）
• crytic/echidna（性質ベースのファジング、反例列の最小化、網羅率、テストモード。2026年9月24日確認）
• Trail of Bits: Building Secure Contracts — Echidna（性質の設計と探索の実践資料。2026年8月12日確認）
• ethereum.org: スマートコントラクトのテスト（テスト手法全体の位置付け。2026年8月12日確認）
• ethereum.org: スマートコントラクトの形式的検証（形式検証との責任分界。2026年8月12日確認）

資料の確認日と注意

Foundry・Echidnaの仕様は2026年9月24日に最終確認しました。ここで述べたのは、公開一次資料にもとづく一般的な技術設計の解説です。特定のスマートコントラクトの安全性を保証するものではありません。使うコンパイラ、EVM、フレームワーク、依存プロトコルの公式仕様とバージョンは、導入時に確かめ直してください。