TechFlowより、5月18日、Vitalik氏が「形式的検証への浅い探訪（A shallow dive into formal verification）」という記事を公開し、形式的検証がイーサリアムの最先端研究開発においてどのように活用されているかを紹介しました。同記事では、開発者がLean、EVMバイトコード、またはアセンブリ言語を用いてコードを記述し、自動的に検証可能な数学的証明によってその正しさを検証することで、コードの効率性と安全性の両方を向上させられると述べられています。
また、Vitalik氏は、STARK、ビザンチン耐性合意（BFT）、ZK-EVM、耐量子署名など、複雑ではあるもののセキュリティ目標が比較的明確なシステムにおいて、形式的検証が特に有効であると指摘しています。さらに、Arklib、VCV-io、evm-asmなどの関連プロジェクトにも言及しています。ただし、記事では形式的検証が万能ではないことも強調されており、仕様定義の誤り、未カバーのコード領域、ハードウェアの制約、サイドチャネル攻撃などの課題により、依然として限界があると述べられています。
お気に入りに追加
SNSで共有
