Vitalik：AI支援による形式的検証は、コードの効率とセキュリティの両方を向上させる可能性がある

Foresight Newsの報道によると、Vitalik Buterinが形式的検証のブロックチェーンセキュリティ分野における応用の展望について投稿しました。記事では、Ethereumの先端開発において新たなパラダイムが生まれており、EVMバイトコード、アセンブリ、またはLeanを直接用いてコードを作成し、その正当性をLeanで自動検証可能な数学的証明で確認する方法が紹介されています。研究者のYoichi Hiraiはこのパラダイムを「ソフトウェア開発の究極の形態」と名付けています。Vitalikは、AI支援による形式的検証がコード効率とセキュリティの両方を高める可能性があり、特にSTARK、ZK-EVM、耐量子署名、コンセンサスアルゴリズムなどのセキュリティコアモジュールに適していると考えています。同時に、記事は形式的検証が万能ではなく、証明範囲の不完全さ、仕様ミス、ハードウェアのサイドチャネルなどによって無効になる場合があることも強調しています。将来的にはソフトウェアが「セキュリティコア」と「非セキュリティエッジ」に分化し、Ethereumが重要なセキュリティコアの一つになるとしています。