TechFlowの報道によると、5月19日、ヴィタリク・ブテリン氏が個人ブログで「形式的検証（Formal Verification）」に関する記事を公開しました。この技術は、イーサリアムの研究開発コミュニティおよびより広範なコンピューティング分野において急速に注目を集めています。形式的検証は、Leanなどの数学的証明ツールを用いて、自動的に検証可能な数学的証明を記述し、コードの正しさを保証する手法であり、研究者からは「ソフトウェア開発の究極の形態」とも称されています。記事では、形式的検証が特に「目標は単純だが実装は複雑」なシナリオにおいて有効であると指摘されており、その例として、耐量子署名（quantum-resistant signatures）、STARKs、合意アルゴリズム、ZK-EVMなど、イーサリアムのコア技術が挙げられています。また、ブテリン氏は、形式的検証には万能ではないという限界があることも強調しています。具体的には、人間の意図を完全に捉えることができず、仕様の抜け漏れや一部コードの検証未実施といったリスクが存在します。
こうした課題に対して、ブテリン氏は楽観的な展望を示しています。すなわち、AIと形式的検証の融合により、両者は互いに補完し合う関係を築くことができるというものです。つまり、AIは大量のコードを効率的に生成し、形式的検証はその正確性を保証する——このような協働によって、将来的なソフトウェアセキュリティは「セキュアなコア＋セキュアでないエッジのサンドボックス」というアーキテクチャモデルへと進化すると予測されています。そして、イーサリアムはその中で重要なセキュア・コアの一つとなるでしょう。
お気に入りに追加
SNSで共有
