Vitalik 發布一篇關於形式化驗證的文章，強調其在以太坊安全性與效率中的角色

根據 ChainCatcher，Vitalik 今天發表了一篇標題為「對形式化驗證的淺層探討」的文章，討論形式化驗證如何同時提升以太坊開發的安全性與效率。開發者可以使用 Lean、以太坊虛擬機（EVM）位元組碼，或組合語言來撰寫程式，並透過可自動檢查的數學證明來驗證其正確性。Vitalik 指出，形式化驗證特別適用於像 STARKs、拜占庭容錯共識、ZK-EVM 與後量子簽名等複雜系統，儘管它也存在限制，包括規格錯誤、程式碼覆蓋不完整，以及硬體層級的攻擊。