暗号資産（仮想通貨）イーサリアム（ ETH ）の共同創設者のヴィタリック・ブテリン氏は18日、形式的検証（formal verification）に関するブログを公開した。
形式的検証とは一般的に、ソフトウェアなどのシステムの正しさを数学的に証明する手法のこと。ブテリン氏は、形式的検証とAI（人工知能）を組み合わせてイーサリアムなどの安全性や開発の効率性を高めることができると分析している。
ブテリン氏は冒頭で、この数カ月の間にイーサリアムの最先端の研究開発コミュニティやコンピューティングに関する他の多くの領域で、プログラミングの新しい手法が急速に普及しつつあると指摘した。
そして、具体的に新しい手法とは、機械語に近いプログラミング言語（EVMバイトコードなどの低級言語）かLeanで直接コードを書き、Leanで書いた自動チェックが可能な数学的証明でコードの正しさを検証するという方法だとしている。
この手法が正しく行えれば、非常に効率的なコードを出力したり、以前のプログラミングよりもはるかに高い安全性を確保したりできる可能性があると主張。ブテリン氏は「この手法はソフトウェア開発の最終形態である」との言葉を引用している。
その上で、今回のブログは、イーサリアムなどにおいて現在何が起きているか、ソフトウェアの形式的検証は何ができるのか、どのような弱点や制限があるかの基礎をわかりやすく説明することを目指すものだと説明した。
ブテリン氏は、現在はAIの発展によって形式的検証が行いやすくなっていると指摘。形式的検証の定義については「数学的な定理の証明を、それらの定理が自動的にチェックされることが可能な方法で記述することを指す」と説明した。
今回のブログは最初のパートのタイトルである「形式的検証とは」や次の「コンピュータープログラムの検証」などと順に展開する、非常に長くて一般の人々には難解な内容である。
その中でブテリン氏は今回、「セキュリティのための形式検証」というパートで、最近注視されている北朝鮮に関連する攻撃やAIモデル「クロード・ミュトス（Claude Mythos）に言及した。
ブテリン氏は、コンピューターのコードに潜むバグについて、変更不可能なブロックチェーンのスマートコントラクトに仮想通貨を預け、そこから北朝鮮の関連組織が自動的に資産を引き出すことが可能で、なおかつバグが原因であるために救済手段がない時に恐怖が増すと指摘している。
また、クロード・ミュトスのような強力なAIモデルが登場し、さらに改良が重ねられて自動的にバグを発見できるようになれば、さらに恐怖感が高まるとも指摘。他にも、ゼロ知識証明にバグが含まれている場合の恐ろしさにも触れた。
このような恐怖に対し「唯一の解決策はオープンソースという特徴自体を手放すことだ」などの悲観的な意見もあるが、ブテリン氏は将来的なサイバーセキュリティについて、もっと楽観的な見方をしていると述べている。
強力なAIによるバグの発見という課題は深刻だが、これは過度期の課題であると考えていると説明。事態が落ち着き、新たな安定局面に入れば、以前よりも防御側に有利な状況が生まれるとの見方を示した。
ブテリン氏は、形式的検証は万能薬ではないが、「目的が実装よりもシンプルな場合」に特に有効であると指摘。イーサリアムがこれから実装しようとしている量子耐性のある署名やZK-EVMなどの、展開が極めて困難な技術にも有効性が当てはまるとした。
今回ブテリン氏は形式的検証について、イーサリアムなどの効率性向上につながる活用方法も説明した。具体的には、プログラミング言語を使う開発での活用である。
形式的検証とAIを組み合わせて使うことで、効率性を重視した低級言語を安全に使いやすくなると指摘。ブテリン氏は、この低級言語と人間が理解しやすい高級言語が同じであるかを検証・証明できるようになると説明した。
ブテリン氏が指摘しているように、一般的に機械が理解しやすい低級言語を使った方が開発が相対的に速く効率的に行える。一方、高級言語には人間が理解しやすいというメリットがあり、安全性を高めることが可能だ。
今回ブテリン氏は、形式的検証とAIを活用し、低級言語の効率性と高級言語の読みやすさ・安全性を両立することができうると説明している。
ブテリン氏は最後の段落で、イーサリアムなどのコアな部分においてはバグは避けられないものという従来の常識を覆し、形式的検証によって実際に安全な世界を実現すべきだと主張した。
