イーサリアム共同創設者のヴィタリック・ブテリン氏は18日、自身のブログで「A shallow dive into formal verification（形式検証への浅い入門）」と題した記事を公開した。ソフトウェアの正しさを数学的な証明によって保証する「形式検証」が、イーサリアムの研究・開発において急速に普及しつつある現状を解説している。

「ソフトウェア開発の最終形態」──AIが形式検証を現実にした

形式検証とは、プログラムの挙動が仕様通りであることをコンピュータが自動的に検証できる数学的証明として記述する手法だ。概念自体は約60年前から存在するが、証明を書く作業が極めて煩雑だったため、長らくニッチな分野にとどまっていた。

ブテリン氏によると、この状況を変えつつあるのがAIの進歩だ。証明支援言語「Lean（リーン）」を使ったコード記述と検証が、AIの支援により格段に効率化されている。現在、イーサリアムの最先端の研究・開発グループでは、EVMバイトコードやアセンブリ言語などの低レベル言語で直接コードを書き、Leanで正しさを証明するアプローチが急速に広がっている。Yoichi Hirai氏はこの手法を「ソフトウェア開発の最終形態」と呼んでいる。

たとえばフィボナッチ数列の性質（3つごとに偶数が現れる）のような数学的定理を、人間が理解できる証明ではなく、コンピュータが自動検証できる形式で記述する。人間にとっての直感的な証明と、コンピュータにとって検証しやすい証明は大きく異なるが、Leanの「omega」タクティクスなどの機能により、複雑な数式展開を一行で処理できるようになっている。

暗号資産業界で「なぜ重要か」──3つの具体的応用

ブテリン氏は、形式検証が暗号資産業界にとって特に重要である理由を3段階のリスクで説明している。

第一に、スマートコントラクトのバグだ。不変のオンチェーンコントラクトにバグがあれば、北朝鮮のような攻撃者が自動的に全資金を引き出せてしまう。第二に、これがゼロ知識証明（ZKP）で包まれると、攻撃が成功しても「何が」起きたのか、さらには「いつ」問題が発生したのかすら判別できなくなる。第三に、AIモデルの進歩により、ゼロデイ脆弱性の自動発見が加速しており、防御側も同等の速度で安全性を担保する手段が必要になっている。

具体的な応用例として、ブテリン氏は3つのプロジェクトを挙げた。まず、暗号化メッセンジャーSignalのX3DHプロトコルの安全性を形式検証で証明する取り組みだ。DDH（決定的ディフィー・ヘルマン）仮定のもとで、受動的攻撃者がセッション鍵をランダムな値と区別できないことを数学的に証明している。次に、TLSやブラウザ内暗号の安全な実装を証明する「Project Everest」。さらに、EVMバイトコードレベルでスマートコントラクトの正しさを証明する取り組みも進行中だ。

形式検証の限界──「安全」の定義自体が間違っている可能性

一方でブテリン氏は、形式検証の限界についても率直に言及している。最大のリスクは「安全」の定義そのものが不完全な場合だ。証明すべきクレーム（主張）を見落とすことは容易であり、クレームがコード自体と同じくらい複雑になるケースもある。

また、システムの一部だけを形式検証しても、検証されていない部分やハードウェアのバグで攻撃を受ける可能性は残る。さらに、証明の前提に組み込まれた仮定が実際には成立しないケースや、Lean自体の実装バグも理論上は存在し得る。

ブテリン氏はこうした限界を認めつつも、形式検証がセキュリティを大幅に向上させるツールであることは間違いないとの立場を示している。エンドツーエンドで形式検証を行えば、ユーザーはコード全体を読む必要がなくなり、証明された「主張」だけを確認すればよい。これは暗号資産における「トラストレスネス」の実現に直結する概念だ。

先日のBybitハッキング（約15億ドル被害）やEIP-7702の委任悪用など、コードの脆弱性が巨額の被害を生む事例が後を絶たない中、形式検証はこうした構造的リスクに対する根本的な対策として注目を集めている。ブテリン氏のブログ投稿は、イーサリアムのセキュリティ哲学が「テスト・監査」から「数学的証明」へと移行しつつある潮流を象徴するものだ。

関連：イーサリアム財団「署名内容を見える化」──Bybit級ハッキング防止へ新規格
関連：ヴィタリック氏、イーサリアム100年計画発表──量子耐性を最優先

関連銘柄：ETH