維塔利克：以太坊將成為「安全核心」重要組成部分，AI輔助形式化驗證可提升程式碼安全性

BlockBeats 消息，5 月 19 日，以太坊联合创始人 Vitalik Buterin 發文深度解析形式化驗證（Formal Verification）技術的現狀與前景，認為結合 AI 的形式化驗證將成為「軟體開發的終極形態」，也是在強大 AI 對手面前守住網路安全底線的關鍵路徑。Vitalik 指出，形式化驗證的核心是將程式碼的正確性轉化為可被電腦自動檢驗的數學定理，從而以數學證明的方式保障軟體安全，而非依賴傳統測試或人工審計。他認為這一範式尤其適用於「目標遠比實現簡單」的場景——例如量子抗性簽名、STARK 證明系統、拜占庭容錯共識算法和 ZK-EVM，這些恰恰是以太坊下一階段升級的核心技術組件。

然而，Vitalik 也坦承形式化驗證並非萬能。常見失效模式包括：僅對部分程式碼進行驗證而遺漏關鍵缺陷、安全規範本身存在疏漏，以及軟硬體邊界處的旁路攻擊難以被現有證明模型捕捉。他強調，「可證明的正確性」在本質上驗證的是不同意圖表達之間的內在一致性，而非對照人類真實意圖的絕對正確。

對於 AI 帶來的網路安全挑戰，Vitalik 持審慎樂觀態度。他認為，AI 輔助的形式化驗證將推動軟體架構向「安全核心與不安全邊緣」的模式演進：邊緣組件在沙箱中運行，被授予最小權限；安全核心則通過形式化方法持續強化，承載社會數位化過程中最高級別的信任負擔。以太坊將成為這一安全核心的重要組成部分。