PANewsは5月18日、ヴィタリック・ブテリン氏がブログ記事を公開し、イーサリアムコミュニティがLeanのような形式検証ツールを使用して、基盤となる言語（EVMバイトコードやRISC-Vアセンブリなど）で直接コードを記述し、機械検証可能な数学的証明によって正当性とセキュリティを確保する実験を行っていると報じた。ヴィタリック氏は、形式検証はSignal、TLS、STARK、ZK-EVM、コンセンサスアルゴリズム、EVM実装などの暗号化通信プロトコルのエンドツーエンドのセキュリティと等価性を検証するために使用でき、AIが自動的にバグを発見する新しい環境において防御側の優位性を大幅に高めることができると指摘した。しかし、形式検証は万能薬ではなく、モデル化されていない仮定、サイドチャネル、未カバーのモジュールなどのリスクを見落とす可能性があることも強調した。ヴィタリック氏は、将来のソフトウェアは少数の「セキュリティコア」を中心に構築され、AIがコード生成の大部分を処理し、形式検証が重要インフラのセキュリティを確保する責任を負うようになると考えている。