「コードは法なり」から「仕様は法なり」へ：形式検証（Formal Verification）が DeFi の 34 億ドル規模の不正流出危機をいかに解決するか
たった 1 つの丸め誤差 — Solidity の整数除算における 1 ペニー未満の精度損失 — により、Balancer から 9 つのブロックチェーンにわたり 30 分足らずで 1 億 2,800 万ドルが流出しました。これらのプールは数年間稼働していました。複数の監査がコードをレビューしていました。しかし、誰も気づきませんでした。これが 2026 年における DeFi セキュリティの現状です。実証的に、そして繰り返し失敗してきたパラダイムによって、何十億ドルもの資産が守られているのです。
現在、a16z crypto は根本的な再考を提案しています。2026 年の「Big Ideas」レポートの中で、同ベンチャーキャピタルは、業界は「Code Is Law（コードは法なり）」— デプロイされたスマートコントラクトのコードが最終的な権威であるという根本的な信念 — を捨て、「Spec Is Law（仕様は法なり）」— 数学的に定義された安全特性が強制的な標準となる — に置き換えるべきだと主張しています。この転換は、プロトコルがどのように構築、監査、防御されるかを根本的に再構築する可能性があります。
監査では解決できない 34 億ドルの問題
数字は衝撃的な事実を物語っています。2025 年だけでも、暗号資産（仮想通貨）業界は窃盗により 34 億ドル以上を失い、そのうち Bybit の侵害が 15 億ドルを占めました。スマートコントラクトのバグは、2025 年上半期だけで約 2 億 6,300 万ドルの被害をもたらしました。累計で、上位の DeFi 悪用事例（エクスプロイト）により、プロトコルから 107.7 億ドル以上が引き出されています。
「コードを書き、監査人を雇い、デプロイして、祈る」という従来のセキュリティモデルは限界に達しています。一流企業による複数の監査を受けた、資金力のあるプロトコルでさえ脆弱なままです。Balancer の悪用はこれを疑いようもなく証明しました。何年も目の前に隠れていた脆弱性が、プロのセキュリティレビューで見逃され、発見されると数分で悪用されたのです。
さらに厄介なのは、攻撃の巧妙化が進んでいることです。2024 年にはフラッシュローンによる悪用が急増し、対象となる悪用事例の 83.3% を占めま した。2025 年の主要なハッキングのほとんどは、2 つから 4 つの脆弱性タイプを同時に組み合わせていました。北朝鮮のハッカーだけで 2025 年に 20 億 2,000 万ドルを盗み出し、前年比で 51% 増加しました。攻撃者は防御者よりも速く賢くなっています。
1 億 2,800 万ドルの丸め誤差の解剖学
Balancer の悪用事例は、「Code Is Law」がなぜ失敗するのかを完璧に示しているため、詳細な調査に値します。2025 年 11 月 3 日、攻撃者は Balancer の ComposableStablePools が少額のスワップを処理する方法における数学的な脆弱性を悪用しました。
何が起きたのか：トークンの残高が特定の範囲（8-9 wei）に追い込まれると、Solidity の整数除算によって大幅な精度損失が発生します。_upscaleArray 関数はスケーリング中に切り捨てを行い、プールのインバリアント（不変条件）— 公正な交換レートを支配すべき数学的定数 — を過小評価させます。これにより、BPT（Balancer Pool Token）の価格が人為的に抑制されます。
攻撃者は、65 以上の操作を含む 1 つの batchSwap トランザクション内で 3 段階のスワップシーケンスを実行することで、これを武器化しました：
- 価格抑制: 大量の BPT を原資産トークンとスワップし、1 つのトークンの残高を丸め誤差が最大化するクリティカルな 8-9 wei の閾値に追い込む。
- 格安取得: 人為的に抑制された価格で BPT をミント（鋳造）または購入する。
- 全額償還: 直ちに BPT を原資産に対して全額で償還する。
攻撃全体は、デプロイされたスマートコントラクトのコンストラクタ内で実行されました。Ethereum、Base、Arbitrum、Avalanche、Optimism、Gnosis、Polygon、Berachain、Sonic にわたる 1 億 2,864 万ドルを流出させた、単一のトランザクションです。コミュニティの迅速な対応により約 1,900 万ドルが回収されましたが、大部分は失われました。
重要な教訓：これはエキゾチックな脆弱性ではありませんでした。数学的なインバリアントの違反でした — 定義上、形式仕様（Formal Specification）があれば捕捉できていたはずの種類のバグです。
「Spec Is Law」が実際に意味すること
a16z の提案は、静的（デプロイ前）と動的（デプロイ後）の 2 つのレベルで機能します。
静的な側面では、DeFi セキュリティは、厳選されたローカルなプロパティの検証から、グローバルなインバリアントを体系的に証明することへと移行する必要があります。「この関数はエッジケースを正しく処理しているか？」と問うのではなく、「このシステム全体は、考えられるすべての入力と状態の下で、その核心的な数学的特性を維持しているか？」が問いとなります。
ここで、Certora Prover や Runtime Verification の K Framework といった形式手法ツールが登場します。これらのツールは、スマートコントラクトのバイトコードを、期待される動作を定義する数学的ルールと比較し、考えられるすべてのコントラクトの状態と実行パスをチェックします。たとえば Certora Prover は、CVL（Certora Verification Language）で記述された仕様を使用して、静的解析と制約解消を通じてプロパティ違反を検出します。
動的な側面では、それらと同じインバリアントがライブ・ガードレール — すべてのトランザクションが満たさなければならないランタイム・アサーション — になります。トランザクションが核心的な安全特性に違反する場合、それは自動的にリバート（差し戻し）されます。これが「最後の防衛線」という概念です。たとえ斬新で、これまで見たことのない攻撃であっても、システムの基本的な安全特性を満たさなければなりません。
このアプローチの優雅さは、その非対称性にあります。攻撃者は違反を見つけなければなりませんが、防御者は「正しさ」がどのようなものかを定義するだけで済みます。a16z が述べているように、「斬新な攻撃であっても、システムを無傷に保つのと同じ安全特性を満たさなければならないため、残された攻撃はごくわずかであるか、実行が極めて困難なものだけになる」のです。
すでにこの手法で構築しているプロジェクト
「仕様が法である（spec is law）」というビジョンは、単なる理論ではありません。いくつかの主要なプロトコルは、開発プロセスの核として形式検証を採用し始めています。
TVL（預かり資産）で最大のレンディングプロトコルである Aave は、Certora Prover を継続的インテグレーション（CI）パイプラインに直接統合しました。すべてのコード変更は、マージされる前に形式仕様に照らして自動的に検証されます。これは時折行われる監査ではなく、すべてのコミットに対して実行される数学的証明です。
Uniswap V2 は、Runtime Verification の K Framework を使用して、その核となる「x * y = k」マーケットメイカーモデルの形式検証を行いました。この検証は、数学モデルの定式化、スマートコントラクトの実装、および 4 つの重要な関数に対するコンパイル済みバイトコードのシンボリック実行をカバーしました。
Solana ベースのレンディングプロトコルである Kamino は、2025 年初頭に Certora Prover を使用して重要な不変条件（インバリアント）のチェックを開始しました。XRP Ledger もプロトコルレベルで不変条件チェックを実装しています。これらは Ethereum 限定の動向ではありません。「仕様が法である」というアプローチは、ブロックチェーンのエコシステム全体に広がっています。
AI と形式検証の融合：Certora の Composer
形式検証における最大の障壁の 1 つは、その複雑さでした。形式仕様を記述するには、ほとんどの開発チームが持ち合わせていない専門知識が必要です。しかし、状況は変わりつつあります。
2025 年 12 月、Certora は AI Composer をリリースしました。これは、コード生成プロセスに形式検証を直接組み込むオープンソースの AI コーディングプラットフォームです。スピードを優先する一般的な AI コーディングツールとは異なり、AI Composer は AI が生成したすべてのコードスニペットが実行前に数学的な安全規則に準拠していることを保証します。
このプラットフォームは、形式検証の民主化の可能性を示しています。AI が仕様の記述、不変条件の提案、手動の証明エンジニアリングコストの削減を支援できれば、「仕様が法である」という考え方は、現在専任の形式検証エンジニアを雇う余裕がある少数のチーム以外にも手が届くものになります。
この AI と検証の融合は、現在の DeFi セキュリティが「厳選された局所的な不変条件を検証するのではなく、グローバルな不変条件を体系的に証明する」べきであるという a16z の指摘にも対応しています。AI は人間よりも広範囲に仕様空間を探索できるため、Balancer の丸め誤差のように手動レビューをすり抜けてしまうような、微妙な数学的違反を捉えられる可能性があります。
法的およびガバナンスへの影響
「仕様が法である」という考え方は、コード以外の部分にも影響を及ぼします。プロトコルがその意図された動作を定義する形式仕様を公開すれば、その仕様はプロトコルが判断される際の法的基準になる可能性があります。
「コードが法である（code is law）」という体制下では、デプロイされたコードの悪用は、技術的には「意図通りに動作している」ことになります。たとえそれが開発者の意図したものではなくても、コードはプログラムされた通りに正確に実行されたからです。対照的に「仕様が法である」の下では、形式仕様が意図を定義します。プロトコルの開発者は、公開された仕様からの逸脱については責任を負いますが、仕様の範囲外にあるあらゆる悪用ベクトルに対して責任を負うわけではありません。
これにより、より明確な責任の枠組みが構築されます。もし Balancer が、取引の順序に関係なくプールの不変条件が定義された範囲内に留まらなければならないという形式仕様を公開していたなら、丸め誤差の悪用は明らかな仕様違反となり、法的救済や保険金の支払請求の根拠となった可能性があります。
課題と限界
「仕様が法である」というテーゼは説得力がありますが、現実的な障害にも直面しています。
仕様の完全性は根本的な課題です。重要なすべてのプロパティをどのように形式的に指定するのでしょうか？ 仕様は人間によって書かれるものであり、監査人が重要なバグを見逃すのと同じように、人間も重要なプロパティを見逃す可能性があります。正しい不変条件を捉えていない仕様は、誤った安心感を与えてしまいます。
コンポーザビリティ（構成可能性）のリスクも別の層の課題です。DeFi の価値は、プロトコル同士の相互作用から生まれます。単一のプロトコルの不変条件を形式的に検証したとしても、そのプロトコルが予想外の方法で他のプロトコルと組み合わされたときの安全性を保証するものではありません。プロトコル間の相互作用の領域は、依然として大部分が仕様化されていない未開拓の分野です。
パフォーマンスとコストは実用面での懸念事項です。形式検証は計算コストが高くなります。実行時の不変条件チェックは、すべてのトランザクションにガス代を追加します。毎秒数千件のトランザクションを処理する高頻度のプロトコルにとって、これらのコストは重要です。
採用への慣性が最大の障害かもしれません。ほとんどの DeFi チームは、激しい競争圧力の下でコードをリリースしています。開発パイプラインに形式検証を追加すると、デプロイが遅れます。市場が検証済みのプロトコルに対して、より高い TVL や低い保険料といった形で報いるようになるまでは、採用のインセンティブは弱いままです。
今後の展望
これらの課題にもかかわらず、進むべき方向は明確です。悪用による被害額（2025 年には 34 億ドル、累計で 107.7 億ドル）を考えると、現状維持は不可能です。保険市場、機関投資家、および規制の枠組みは、証明可能なセキュリティ保証をますます求めるようになるでしょう。
AI 支援による仕様記述、成熟した形式検証ツール、および実行時の強制インフラの融合により、採用の障壁は低くなっています。Aave がすべてのコミットで Certora Prover を実行でき、Kamino が Solana 上で不変条件をチェックできるようになり、ツールは学術研究から本番のインフラへと移行しました。
業界が「コードは法である」から「仕様は法である」へと進化することは、成熟したあらゆる工学分野で見られるパターンを反映しています。「構築してみたところ、うまく動いているようだ」から「仕様を満たしていることを数学的に証明できる」への移行です。航空、原子力工学、半導体設計はすべてこの移行を経てきました。1,000 億ドル以上の TVL が数学的正しさに依存している DeFi にとって、この移行はむしろ遅すぎると言えます。
問題は「仕様が法である」ことが標準になるかどうかではありません。それが実現するまでに、さらに何十億ドルが失われるかということです。
BlockEden.xyz は、複数のチェーンにわたる DeFi アプリケーションを支えるエンタープライズグレードのブロックチェーン API インフラストラクチャを提供しています。形式検証が業界標準になるにつれ、信頼性の高いノードインフラストラクチャは、検証済みプロトコルの相互作用の基盤となります。API マーケットプレイスを探索して、セキュリティ優先の時代に合わせて設計されたインフラストラクチャ上で構築を開始してください。