形式的検証とは、数理論理学を用いてシステムの正確性を証明する手法だ。スマートコントラクトに適用する場合、コントラクトのコードと、事前に定義された「仕様」（通常はコントラクトがどのような状況下でも決して違反してはならないルールを記述したもので、不変条件〔invariant〕と呼ばれる）を突き合わせ、自動定理証明やモデル検査といった数学的なツールを用いて、あらゆる可能な実行経路と入力の組み合わせを網羅的に検査し、コードがそのの仕様を数学的に満たしていることを証明する。これはスマートコントラクト監査で一般的に用いられるテストやファジングとは本質的に異なる。テストは誰かが思いついてテストコードとして書き起こしたその特定のシナリオしか検証できず、コード内の条件分岐が一つ増えるごとに実行可能な経路の数は倍増しかねないため、テストではあらゆる経路を網羅することは決してできない。一方で形式的検証は数学的証明を用いることで、理論上は一部を抽出して検査するのではなく、あらゆる可能な経路を網羅できる。
現在のイーサリアムエコシステムで一般的に使われている形式的検証ツールには、Certora Prover（専用のCVL仕様記述言語を使用）、Solidity組み込みのSMTChecker、そして定理証明やモデル検査に基づく各種の学術的ツールなどがあり、それぞれ自動化の度合いや対応できるコントラクトの複雑さに違いがある。
形式的検証がスマートコントラクト業界で重視される根本的な理由は、ブロックチェーンアプリケーションが一度デプロイされ資産がコントラクトにロックされると、コードのバグは従来のソフトウェアのように後から簡単にパッチを当てて修正することができないことが多い点にある。多くのコントラクトは意図的に改変不可能に設計されており、従来のテストがカバーしていなかった極めて稀な実行経路に潜む一つの脆弱性が、数千万ドル、時には数億ドル規模の資産損失を引き起こしうる。「一度誤りが起きればコストが極めて高く、かつ事後の修復が難しい」というこの特性こそが、形式的検証のような数学レベルの保証を提供する手法がスマートコントラクト分野に特に適している理由だ。
イーサリアム仮想マシン（EVM）の実行環境は決定論的（deterministic）かつ有界（bounded）という特性を持つ——同じ入力は常に同じ出力を生み、実行過程には従来のソフトウェアによく見られる無限ループや不確定な外部状態が関与しない。この特性は形式的な数学的手法をスマートコントラクトに比較的適用しやすくしており、汎用のソフトウェアシステムと比べて、むしろスマートコントラクトは形式的検証が効果を発揮しやすい環境だと言える。
形式的検証の実際のプロセスは、通常コントラクトのコードとEVMの実行状態を数学モデルに変換することから始まる。このモデルはシステム全体を状態機械（state machine）として表現し、各取引が一つの状態遷移に対応する。次に開発者や監査担当者は仕様を記述する必要がある。これはシステムがどのような状況下でも維持しなければならない不変条件を明確に定義するもので（例えば「コントラクト内のトークン総供給量は、常にすべてのアカウント残高の合計に等しい」といった条件）、この仕様記述の質が検証全体の有効範囲を直接左右する。最後に定理証明器（theorem prover）またはモデル検査器（model checker）がこの数学モデルと仕様に対して推論を行い、仕様に違反する入力や取引の連続を一つでも発見すれば、ツールは具体的な「反例」（counterexample）を生成し、どの取引の組み合わせが違反を引き起こすかを正確に特定する。推論に成功すれば、その仕様が記述する性質があらゆる条件下で成立することが数学的に証明されたことを意味する。
業界では現在、形式的検証と人手による監査は互いに代替するものではなく補完し合う関係にあると広く認識されている。人手による監査は仕様に欠けているルールを明確化したり補完したりすることや、ビジネスロジックそのものの設計が妥当かどうかを判断することに長けており、形式的検証は人手による監査が見落としがちな境界ケース（corner case）を見つけ出すことに長けている。特にコードが継続的に修正されるプロジェクトでは特に有効だ。しかし逆に言えば、定理証明のような手法は通常完全には自動化されておらず、複雑なロジックに直面すると人間の専門家が介入し証明器を導いて推論を完了させる必要があることが多い。これが形式的検証の実行コストと時間的投資が、一般的なテストツールに比べてかなり高くなりがちな理由でもある。
一般ユーザーにとって、あるプロジェクトが自分たちのコントラクトは「形式的検証を受けている」と主張しているのを見た際、最も重要な理解は次の点だ——それはコントラクトの中核となるロジックが、ある特定の仕様を満たすことが数学的に証明されたことを意味するが、その保証の有効範囲は、その仕様そのものがどれだけ完全に記述されているかに完全に依存する。もし開発者が仕様を書く際に、本来存在すべきルールを一つ見落としていたり、仕様そのものに論理的な誤りがあったりすれば、形式的検証ツールはその仕様に書かれていないルールを一切検査しない。これは、あるコントラクトが数学的には完全に「仕様を満たしている」と証明されながら、同時に深刻な脆弱性が依然として存在しうることを意味する——ただしその脆弱性は、たまたま仕様がカバーしていない範囲に落ちているだけなのだ。
Bybit事件は、まさにこの原則を最も鮮明に示す実例だ。Bybitが利用していたSafeマルチシグコントラクトは、その中核ロジックが確かに業界で高く評価される厳格な形式的検証を経ており、長年の運用の中でプロトコルレベルの侵害は一度もなかった。しかし攻撃者はコントラクトのロジック自体を完全に迂回し、署名者が取引内容を「理解する」ために依拠していたインターフェース層を狙った——この層はいかなる形式的検証の仕様範囲にも一度も含まれたことがなかった。なぜなら形式的検証は、そもそも「ユーザーに表示される画面が真実であること」を証明するために存在するものではないからだ。したがって「形式的検証済み」という言葉を目にしたら、それは「コントラクトの中核ロジックが厳格な数学的検査を経ている」という意味だと理解すべきであり、「このプロジェクトにはセキュリティリスクが一切ない」という意味ではない——この二つは別のことであり、前者は後者の必要条件の一つであって、十分条件ではない。
Bybit事件で使われたSafeマルチシグコントラクトの中核ロジックは、セキュリティ企業CertoraがそのCertora Proverツールを用いて形式的検証を実施しており、これは署名しきい値の仕組みが正しく機能することなど、特定の不変条件をコントラクトのロジックが満たしていることを数学的に証明するものだった。Safeのコントラクトは長年の運用の中でプロトコルレベルでの侵害は一度もなく、この検証実績自体はコントラクトロジックの高い信頼性を確かに反映していた。しかし2025年2月の実際の攻撃では、攻撃者はコントラクトロジック自体を破ろうとは一度も試みず、代わりにサプライチェーン攻撃を用いて署名者が取引内容を確認するために依拠していたインターフェースソフトウェアを改ざんし、署名者に偽造された「明瞭な」取引説明に対して署名を完了させた。この事件は、形式的検証が保証する範囲と、システム全体が実際に直面するリスクの範囲との間に生じうる乖離を明確に示している。
形式的検証の利点は、数学レベルの正確性保証を提供でき、理論上はあらゆる可能な実行経路を網羅できることであり、デプロイ後に修正が難しく誤りのコストが極めて高いスマートコントラクトのようなシステムに特に適している。欠点は実行コストと時間的投資が概して高く、複雑なロジックにはしばしば人間の専門家による証明プロセスへの介入が必要であり、保証の有効範囲は仕様記述の完全性に完全に制約されるという点だ——本記事で触れたインターフェース層攻撃のような、仕様の外にあるリスクは検証範囲に一切含まれない。したがって形式的検証だけに単独で依存すべきではなく、包括的なセキュリティ戦略の一要素として扱うべきである。