深潮 TechFlow 消息，5 月 19 日，Vitalik Buterin 個人博客發文，形式化驗證（Formal Verification）正在以太坊研發圈及更廣泛的計算領域迅速興起。該技術通過在 Lean 等數學證明工具中編寫可自動檢驗的數學證明，來驗證代碼的正確性，被研究者稱為"軟件開發的終極形態"。文章指出，形式化驗證尤其適用於目標簡單但實現複雜的場景，包括量子抗性簽名、STARKs、共識算法及 ZK-EVM 等以太坊核心技術。V 神同時強調，形式化驗證並非萬能，其侷限性在於無法完全捕捉人類意圖，且存在規範遺漏、部分代碼未被覆蓋等風險。

對此，他提出樂觀展望：AI 與形式化驗證的結合將形成互補——AI 負責高效生成大量代碼，形式化驗證則確保其準確性，未來軟件安全將形成"安全核心+不安全邊緣沙盒"的架構模型，以太坊將成為其中重要的安全核心之一。