イーサリアム（ ETH ）の共同創設者ヴィタリック・ブテリン氏（Vitalik Buterin）は17日、AIによるハッキングの増加でサイバーセキュリティは崩壊するとの見方が広がっていることについて、X（旧Twitter）で反論した。
同氏は「人々がきちんと取り組みさえすれば、サイバーセキュリティは本質的に防御側が有利になる」と主張し、自身の純資産の約9割を仮想通貨で保有し続けていること自体が、この見立てに賭けている証だと説明した。
形式検証とは、プログラムが特定の性質を満たすことを数学的に証明する手法を指す。テストで個々の動作を確認するのとは異なり、あらゆる入力パターンに対して不具合が起きないことを理論的に保証できる点が特徴だ。
ヴィタリック氏は「AIがナビエ・ストークス方程式やフェルマーの最終定理のような数学の難問を証明できるなら、プログラムがどれほど複雑であっても『このプログラムは安全である』という命題を数学的定理として証明できるはずだ」と述べた。
同氏によると、暗号化メッセージアプリ「Signal」の安全性を例に挙げても、鍵の漏えい経路や送受信者の特定可能性まで含めると、定義そのものが1000行を超える規模になり得る。それでも実装コード全体を検証するより、定義を検証するほうがはるかに扱いやすいと指摘した。
定義には複数の要件を組み合わせられる利点もある。異なる2つの定義を同時に満たすことは、コードの一部にバグがあれば全体が破綻するのとは対照的に、証明として積み上げられるという。
過去の形式検証プロジェクトの多くは、開発者が自ら「安全性に関わる」と判断した一部分しか検証しておらず、それ以外の箇所に脆弱性が潜んでいたと同氏は振り返った。データベースやネットワーク層を含むプログラム全体を検証する必要があるとし、AIの進歩によりそれが現実的になったとの見方を示した。
ヴィタリック氏はこの方向性について、イーサリアムが数年単位で進める取り組みだと位置づけた。スケーラビリティとプライバシーを両立させるブロックチェーンには、この手法を避けて通る未来はないと言い切った。
同氏は2026年5月、自身のブログで形式検証に関する解説記事を公開しており、今回の投稿はその内容を踏まえたものだ。
