維塔利克·布特林分析人工智能時代形式驗證的進展與限制

Odaily 星球日報訊 以太坊聯創 Vitalik Buterin 發布文章《A shallow dive into formal verification》，系統梳理了形式化驗證（Formal Verification）在以太坊及更廣泛計算領域中的最新發展與局限。文章指出，近幾個月在以太坊前沿研究圈中，一種新編程範式正在快速興起：開發者直接使用極低級語言（如 EVM 字節碼、彙編）或 Lean，並通過可自動驗證的數學證明來驗證代碼正確性。這種方法理論上既能提升代碼效率，也能顯著提高安全性，被部分研究者稱為「軟體開發的終極形態」。

Vitalik 表示，形式化驗證的核心是透過機器可檢查的數學證明來驗證程式性質，其價值在於能夠將「安全性」從經驗測試轉向可證明的邏輯體系。在加密通信、密碼協議以及區塊鏈系統（如零知識證明與共識機制）中，這一方法已開始被用於端到端驗證關鍵系統行為。

文章同時指出，以太坊生態系統正在探索包括 EVM 實現、STARK 證明系統及抗量子簽名等關鍵基礎設施的形式化驗證項目，以提升協議級安全性與可靠性。不過，Vitalik 也強調形式化驗證並非「銀彈」。其局限包括：安全性定義依賴人為建模、部分系統難以完整形式化，以及硬體或非驗證模組仍可能成為攻擊面。此外，即便在形式化證明存在的情況下，規格錯誤或未覆蓋的假設仍可能導致漏洞。

Vitalik 最後提出，更現實的路徑是將形式化驗證與 AI 輔助編程、類型系統、測試框架等多種方法結合，在「冗餘表達意圖並自動驗證一致性」的框架下逐步提升軟體安全性。在 AI 大規模生成代碼的趨勢下，軟體系統將逐步分化為「易受攻擊的邊緣模組」與「高度可信的安全核心」。未來應將形式化驗證集中應用於核心系統（如區塊鏈協議、作業系統核心等），以構建可驗證安全性的數位基礎設施。