以太坊Vitalik：AI輔助形式化驗證有望提升安全性

香港文匯報訊（記者 黎梓田）以太坊創辦人Vitalik Buterin（V神）發文探討形式化驗證（Formal Verification）在區塊鏈安全領域的應用前景。文章指出，以太坊前沿研發中正興起一種新範式，直接使用EVM位元碼、匯編或Lean編寫程式碼，並用Lean中可自動檢查的數學證明驗證其正確性，研究者Yoichi Hirai將這一範式稱為「軟體開發的最終形態」。

Vitalik認為，AI輔助形式化驗證有望同時提升程式碼效率與安全性，尤其適用於STARK、ZK-EVM、抗量子簽名和共識演算法等安全核心模組。文章同時強調，形式化驗證並非萬能，仍可能因證明範圍不完整、規格錯誤、硬體側信道等問題失效；未來軟體或將分化為「安全核心」與「非安全邊緣」，以太坊將成為重要安全核心之一。

形式化驗證（Formal Verification）是一種利用嚴格的數學與邏輯方法，去「證明」系統（如軟體、硬體或智慧合約）是否符合特定規格的技術。簡而言之，一般的測試是「找 Bug」，而形式化驗證則是「數學證明完全沒有 Bug」。