スマートコントラクトの形式検証は必要か｜監査・テストとの違いと対象の絞り方

監査も受けた。テストも書いた。それでも、大きな資産を預かるコントラクトを本番に出す前には迷いが残ります。形式検証まで足すべきなのか。やるなら、どこまで対象にするのか。費用に見合うのか。

形式検証は、「この約束は、どんな入力でも破れない」ことを数式で確かめる方法です。ただし確かめられるのは、あらかじめ書いた約束と前提の範囲に限られます。

そこで対象は、コントラクト全体ではなく、破れたら損失に直結する約束に絞ります。預かった資産が減らない。権限のない人が管理操作をできない。こうした約束です。そのうえで、監査・テストとどう分担するか、仕様を変えたときに証明し直す費用はどれくらいか、を見積もります。

以下では、スマートコントラクトの本番導入を決める責任者と設計者が、形式検証を足すかどうかを判断する順に見ていきます。証明する約束の選び方、証明の範囲の決め方、小さく試して費用を測る方法、リリース後も続ける仕組みまでです。

形式検証を使うべきかは、5つの問いで決まる

「大金を扱うから全部を形式検証しよう」と決めても、費用に見合うか、何が保証されるのかは決まりません。次の5つの問いに順に答えます。

少なくとも最初の3つ、「壊れたら大損するか」「守るべき約束を式で書けるか」「その部分だけを切り出せるか」にはっきり答えられる部分から始めます。

約束の候補は、たとえば次のようなものです。

• 保管庫（Vault）：「どの入力でも、預かり資産以上を引き出せない」「持分（share）の総供給と持分の会計が一致する」
• ブリッジ：「元のチェーンでロックまたは焼却（burn）されていない資産を、移転先で発行（mint）できない」
• 権限管理：「タイムロックを経ずに、アップグレード権限を使えない」

注意したいのは、形式検証が比べるのは形式仕様と実装だという点です。Solidity公式ドキュメントもそう説明しています。仕様そのものが意図を表しているか、意図しない効果を見落としていないかは、別に確かめる必要があります（Solidity SMTChecker and Formal Verification）。

何を証明するか：損失に直結する約束の一覧を作る

形式検証で確かめられるのは、書いた約束だけです。だから計画は、「何行チェックしたか」ではなく、「どんな約束を守らせるか」の一覧として作ります。資産・権限・状態の移り変わりごとに約束を書きます。

Ethereum.orgは形式仕様を3種類に整理しています。どの実行でも保たれる不変条件、関数の実行前・実行後の条件、時間を含む安全性・活性の性質です（Ethereum.org「スマート・コントラクトの形式的検証」）。安全性は「悪いことが起きない」、活性は「必要なことがいつか起きる」という性質です。

損失に直結する約束の型は、次の5つです。

• 資産保存：外から入出金しない操作では、利用者残高・手数料・準備金の合計が変わらない。
• 権限：管理操作は、指定された役割と待機時間の条件を満たす呼び出しからしか実行できない。
• 状態の移り変わり：清算済みの注文が未処理に戻らない。同じ目的の処理が二度成功しない。
• 上限と境界：発行上限、担保率、価格の有効期限、小数・丸めの境界を越えない。
• 活性：正当な利用者が必要な条件を満たせば、資金を永久に引き出せない状態に閉じ込められない。

形式検証には相応の費用がかかるので、最初からすべてを証明しようとはしません。約束ごとに、次の項目を1枚の台帳にまとめます。

• 守る資産と、操作を許される主体
• 前提
• 反例が見つかったら何を失うか
• 対象のコード

反例が見つかったら、原因を3つに分けます。実装の誤りか、仕様の誤りか、環境のモデルが足りないかです。証明が通った場合も、使った前提と対象外の範囲を、同じ成果物に残します。

証明の範囲をどこで区切るか

証明の結果は、モデルの外まで自動では広がりません。たとえば次のように仮定したなら、それぞれが残るリスクです。

• トークンが標準どおりに真偽値を返す
• オラクルの価格が期限内で正しい
• 管理者の鍵が盗まれない
• プロキシが想定した実装を指している

外部コントラクトの呼び出しをどう扱うかも決めます。何をしてくるか分からない相手として扱うのか。それとも、呼び出し先に実行前・実行後の条件を置くのか、です。

特に注意が要るのは、アップグレードできる構成です。今の実装を証明しても、証明していない実装へ差し替えられる権限が残っていれば、話は別です。「今の実装は仕様を満たす」と「運用期間中ずっと満たす」は、別の主張になります。

そこで、次の仕組みを組み合わせます。

• タイムロック、マルチシグ
• 監視、緊急停止
• 証明し直した成果物だけを通すリリース時のチェック

形式検証で扱えない部分は、ほかの方法に任せます。脅威モデリング、単体・結合テスト、ファジング、監査、バグバウンティ、オンチェーン監視です。操作の並びを作って不変条件を確かめるテストの設計はスマートコントラクトの不変条件テストで、報奨金制度の運用はバグバウンティの解説で扱っています。

Ethereum.orgのテスト解説も、形式検証は通常のテストより強い保証を出せる一方、使うのが難しく相応の費用がかかる、としています。ほかの検証手段と組み合わせる位置付けです（Ethereum.org: Testing smart contracts）。

ツールは、何を証明したいかで選ぶ

形式検証の手法には、得意な問いの違いがあります。関数ごとの条件を証明する、多数の入力や分岐から反例を探す、複数の取引の順番を調べる、といった違いです。だから責任者が押さえておくべきことは一つです。ツールは「Solidityを読めるか」ではなく、「何を証明したいか」で選びます。

比べるときは、次の点を確かめます。

• バイトコードとソースコードのどちらを対象にするか
• 複数の取引・複数のコントラクトを扱えるか、アップグレードや外部呼び出しをどう扱うか
• CIで同じ結果を再現できるか、反例を開発者が追えるか

ツールの名前や提供形態は変わるので、採用する時点の公式ドキュメントで確かめます。手法ごとの向き不向きと代表的なツールは、後半の「技術者向けの詳細」にまとめています。

小さく試して、証明と運用の費用を測る

費用と期間は、コードの量よりも次の3つで大きく変わります。

• 証明する約束の数と難しさ
• 外部呼び出しやアップグレードを、どこまでモデルに入れるか
• 仕様がどれだけ安定しているか

だから、まず試して測ります。採用前のPoCでは、最も危険な1〜3個の不変条件と、それを担う中核コントラクトに絞ります。正常な操作だけでなく、再入（処理の途中で外部から同じコントラクトが再び呼び出されること）、境界値、順序の入れ替え、権限の変更、外部呼び出しの失敗も含めます。そして、反例が開発の中で直せる形で返ってくるかを確かめます。

1. 脅威モデルと損失の場面から、証明する約束と対象外を承認する。
2. 言葉で書いた受入条件、形式仕様、テストの合否を、同じ番号で結ぶ。
3. 対象のコミット、コンパイラ、依存ライブラリ、ソルバー、設定、タイムアウトを固定する。
4. わざと欠陥を入れ、ツールが反例を見つけ、担当者が原因を再現できるか試す。
5. 仕様の変更を1件入れ、証明し直し・レビュー・CIにかかる時間を測る。

成果の物差しは「証明した行数」ではありません。次の数字を見ます。

• 仕様を変えた後、証明し直しにかかる時間
• 重要な約束の証明率
• 未解決・タイムアウトの数、置いた仮定の数
• 反例が見つかってから直すまでの時間

最初の5つの問いでも、変更のたびの証明し直しをリリースの工程に組み込めるかを見ました。証明し直しにかかる時間は、その判断の材料になります。

証明できない部分を「ここは正しいと仮定する」で片付けると、その分だけ安全の裏付けが弱くなります。証明できなかったことは、そのまま「未解決」としてリスクの記録に残します。

形式検証を使わない、または範囲を縮めるのはどんなときか

形式検証を採用しない判断もあります。仕様がよく変わり、何が正しい状態かを関係者が合意できない段階なら、先に別のことを進めます。

• 状態の移り変わりの設計
• 性質ベーステスト（property-based testing）、ファジング
• 監査しやすい単位へのコードの分割

主な失敗の原因が、外部API、価格の入力、鍵の運用、人の承認にある場合もそうです。コントラクトだけを証明しても、主なリスクは下がりません。

一方、全面的な採用が難しくても、小さく安定した中核に絞る価値はあります。資産保存、発行上限、アクセス制御、清算の会計などです。

監査と形式検証は、どちらかを選ぶものではありません。監査は、仕様が妥当か、設計に抜けがないか、統合・運用のリスクはどうかを、人が文脈から検討します。形式検証は、合意した約束とモデルについて、実装が合っているかを漏れなく調べます。監査の進め方はスマートコントラクト監査の工程と費用目安を参照してください。

リリース後も証明を続けるには

リリースの後も、コード・コンパイラ・依存ライブラリ・プロキシ構成が変われば、そのたびに影響する約束を証明し直す必要があります。そのため形式検証は、一度きりの報告書PDFで終わらせず、対象のコミットに結び付いたリリースの成果物として管理します。保存するのは次のものです。

• 仕様、対象範囲、仮定
• ツールの版、設定、結果
• 未解決の項目、レビューの担当者

CIは「ツールが終了した」で通さず、失敗、反例、不明（unknown）、タイムアウト、対象外を見分けて止めます。

本番では、証明した不変条件を監視の指標に置き換えます。総供給と準備金、権限の変更、アップグレードの予定、一時停止（pause）、おかしな状態の移り変わりを見張ります。違反したときの停止権限、連絡、資産の保全、復旧手順も決めておきます。

証明が保証する範囲と、運用で守る範囲を1枚の責任表にまとめておきましょう。「形式検証済みだから安全」という言い過ぎを避けられます。

よくある質問

形式検証と監査は何が違いますか

監査は、人が仕様の妥当性、設計の抜け、他システムとの統合や運用のリスクまで含めて、文脈から評価します。形式検証は、合意した約束について、決めたモデルと前提の範囲で、実装が必ず満たすかを漏れなく調べます。形式検証は「書いた約束」しか確かめません。何を約束として書くべきかを見つける監査と、組み合わせて使います。

費用と期間はどう見積もればよいですか

費用と期間は、コード量よりも「証明する約束の数と難しさ」「外部呼び出しやアップグレードをどこまでモデルに入れるか」「仕様がどれだけ安定しているか」で大きく変わります。まず1〜3個の約束と中核コントラクトに絞ったPoCで、仕様作成、証明、反例への対応、変更後の証明し直しにかかった時間を実測します。その結果から、対象を広げるかを判断します。

技術者向けの詳細

ここからは、ツールを選んで実際に証明を組む設計者向けに、手法とツールの違いをまとめます。

手法とツールの使い分け

主なツールの特徴

• Solidity SMTChecker：requireを仮定、assertを証明対象として解析できます。ただし、すべての業務仕様を自動で見つける機能ではありません。公式ドキュメントでは、複数トランザクションにわたるコントラクトの生存期間を扱うCHCエンジンが推奨され、関数を単独で解析するBMCエンジンは非推奨とされています。
• Certora Prover：専用の仕様言語CVLで規則と不変条件を書きます。GPLv3のオープンソースとして公開されています。
• Halmos・Kontrol：Foundryのテストを記号的に実行する形で使えます。
• hevm：バイトコードの性質の証明や、2つのバイトコードの等価性検査にも使えます。

アップグレードできる構成で対象に含めるもの

実装単体の証明に加えて、ストレージレイアウト（変数の保存位置の並び）、初期化関数（initializer）、プロキシ管理者、アップグレード後も維持すべき不変条件を対象にします。

XTELAができること

私たちは、スマートコントラクトの状態遷移、権限、不変条件、検証境界を整理し、証明対象の性質を決めるところから、小さな中核でのPoC、実装、テスト・監査工程への接続までを設計・開発します。形式証明そのものに独立した評価が必要な場合は、対象技術と保証水準に合う専門家を含めて体制を組みます。貴社のコントラクトでどこまで形式検証を使うべきか検討する際は、お問い合わせからご相談ください。

主要参考資料

• Ethereum.org「スマート・コントラクトの形式的検証」（2026年8月13日確認）
• Solidity Docs: SMTChecker and Formal Verification（2026年9月24日確認）
• Certora Prover Documentation（2026年9月24日確認）
• a16z/halmos（2026年9月24日確認）
• hevm（2026年9月24日確認）
• Runtime Verification: Kontrol（2026年9月24日確認）
• Ethereum.org: Testing smart contracts（2026年8月13日確認）
• Solidity Docs: Security Considerations（2026年8月13日確認）

資料の確認日と注意

ツールの仕様と提供状況は、2026年9月24日に一次資料で確認し直しました。SMTCheckerのエンジンの推奨・非推奨は、2026年9月24日時点の公式ドキュメントによります。

一般的な技術設計の解説です。形式検証は、明示した仕様・モデル・仮定の範囲で実装の性質を評価するものであり、システム全体の無欠陥、経済的安全性、外部データや鍵運用の正しさを保証するものではありません。