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

Foresight News 消息，Vitalik Buterin 發文探討形式化驗證在區塊鏈安全領域的應用前景。文章指出，以太坊前沿研發中正興起一種新範式，直接使用 EVM 位元組碼、組合語言或 Lean 撰寫程式碼，並用 Lean 中可自動檢查的數學證明驗證其正確性，研究者 Yoichi Hirai 將這一範式稱為「軟體開發的最終形態」。Vitalik 認為，AI 輔助形式化驗證有望同時提升程式碼效率與安全性，尤其適用於 STARK、ZK-EVM、抗量子簽名和共識演算法等安全核心模組。文章同時強調形式化驗證並非萬能，仍可能因證明範圍不完整、規格錯誤、硬體側通道等問題失效；未來軟體或將分化為「安全核心」與「非安全邊緣」，以太坊將成為重要安全核心之一。