深潮 TechFlow 消息，5 月 18 日，Vitalik 發佈文章《 A shallow dive into formal verification 》，介紹形式化驗證在以太坊前沿研發中的應用進展。文章指出，開發者可使用 Lean、EVM 字節碼或彙編語言編寫代碼，並通過可自動檢查的數學證明驗證其正確性，以同時提升代碼效率與安全性。

他表示，形式化驗證特別適用於 STARK、拜占庭容錯共識、ZK-EVM、抗量子簽名等複雜但安全目標相對清晰的系統，並提及 Arklib、VCV-io、evm-asm 等相關項目。文章同時強調，形式化驗證並非萬能，仍可能受限於規格定義錯誤、未覆蓋代碼、硬件邊界與側信道攻擊等問題。