ブテリン氏、AIによる形式的検証が暗号通貨のセキュリティを強化すると発言

ブテリン氏、AIとコードの安全性に関する新しい投稿を公開

イーサリアム共同創設者のヴィタリック・ブテリン氏は、2026年5月18日にvitalik.eth.limoでブログ記事を公開しました。その中で、AI支援の形式的検証がサイバーセキュリティの最も重要なツールの一つになると主張しています。形式的検証は、ソフトウェアが意図した通りに正確に動作することを確認するために数学的証明を使用する方法です。ブテリン氏は、AIと形式的検証を組み合わせることで、開発者が攻撃者に先んじて脆弱性を見つけるのに役立つと述べています。

AIの力の例としてクロード・ミトスを挙げる

ブテリン氏は、アンソロピックによって開発されたAIモデルクロード・ミトスを、ますます強力なAIシステムの例として挙げています。彼は、そのようなシステムが脆弱性の発見と悪用を加速できると主張しています。クロード・ミトスは実在のモデルであり、アンソロピックは2026年3月の偶発的なデータ漏洩後にその存在を確認しました。このモデルのプレビューは2026年4月に選ばれたパートナーに公開されました。

ブテリン氏、形式的検証の限界を列挙

ブテリン氏は、形式的検証がすべてのリスクを排除するわけではないと強調しています。証明システムは重要な仮定を見逃したり、ハードウェアの脆弱性や隣接する攻撃面をカバーできなかったりする可能性があります。また、AIが大量のソフトウェアを生成するための障壁を下げることに警告を発しています。これにより、安全でない、または理解が不十分なコードが生産システムに入るリスクが高まります。これらの限界にもかかわらず、ブテリン氏はこのアプローチが従来のソフトウェア開発と比較して壊滅的なリスクを減少させると主張しています。

Arklibプロジェクトが検証されたSTARK実装を目指す

ブテリン氏は、イーサリアムに適用された形式的手法の具体例としてArklibを強調しています。Arklibは、STARK証明システムの完全に形式的に検証された実装を構築することを目指すオープンソースプロジェクトです。STARKは、イーサリアムのスケーリングインフラストラクチャで使用される暗号証明の一種です。イーサリアム財団は、NethermindにFRIプロトコルの形式化をLean証明アシスタントで拡張するための資金を提供しました。ブテリン氏は、RISC-Vアセンブリで直接書かれたイーサリアム仮想マシンの形式的に検証された実装にも言及しています。