Vitalik：AI輔助形式化驗證有望同時提升代碼效率與安全性

ChainCatcher 消息，Vitalik Buterin 發文探討形式化驗證（Formal Verification）在區塊鏈安全領域的應用前景。

文章指出，以太坊前沿研發中正興起一種新範式，直接使用 EVM 位元碼、匯編或 Lean 編寫程式碼，並用 Lean 中可自動檢查的數學證明驗證其正確性，研究者 Yoichi Hirai 將這一範式稱為"軟體開發的最終形態"。

Vitalik 認為，AI 輔助形式化驗證有望同時提升程式碼效率與安全性，尤其適用於 STARK、ZK-EVM、抗量子簽名和共識演算法等安全核心模組。

文章同時強調，形式化驗證並非萬能，仍可能因證明範圍不完整、規格錯誤、硬體側信道等問題失效；未來軟體或將分化為"安全核心"與"非安全邊緣"，以太坊將成為重要安全核心之一。