Vitalik：AI 輔助形式化驗證是「軟體開發終極形態」，以太坊成安全核心

以太坊聯合創始人 Vitalik Buterin 於 5 月 18 日發表深度分析，探討形式化驗證（Formal Verification）技術的現狀與前景，認為 AI 輔助的形式化驗證將成為「軟體開發的最終形態」，並指出以太坊將成為未來「安全核心」架構的重要組成部分。

形式化驗證的核心原理與適用場景

根據 Vitalik 文章確認，形式化驗證特別適用於「目標遠比實現簡單」的場景，他明確列出以太坊下一階段升級的四類核心技術組件：

量子抗性簽名：已有 SPHINCS 簽名變體的形式化驗證工作

STARK 證明系統：Arklib 項目致力於創建完全形式化驗證的 STARK 實現

拜占庭容錯共識算法：目前正致力於正式規定和證明 Lean 共識的安全屬性

ZK-EVM：evm-asm 項目旨在建立完整的形式化驗證 EVM 實現（直接用 RISC-V 彙編語言編寫）

Vitalik 引用平井洋一的說法，將此方法稱為「軟體開發的最終形態」。

Vitalik 描述的「安全核心」架構演進方向

根據 Vitalik 文章確認，他描述了未來軟體架構的演進模式：

安全核心：通過形式化方法持續強化，承載最高信任；Vitalik 明確表示以太坊、作業系統核心和物聯網相關應用將成為安全核心。

不安全邊緣：邊緣組件在沙箱環境中運行，被授予完成工作所需的最低權限；若邊緣組件故障，安全核心提供保護。

形式化驗證的確認限制與失敗模式

Vitalik 坦承形式化驗證並非萬能，援引 Nadim Kobeissi（Cryspen）等研究者的工作，確認的三類主要失敗模式：部分驗證遺漏（僅驗證部分程式碼，而未驗證的部分存在關鍵缺陷）；規範疏漏（安全規範本身錯誤或證明中包含錯誤假設）；旁路攻擊（軟硬體邊界處的側通道攻擊難以被現有模型捕捉）。

Vitalik 強調，「可證明的正確性」在本質上驗證的是不同意圖表達之間的內在一致性，而非與人類真實意圖的絕對對應。

AI 輔助形式化驗證的確認工具

根據 Vitalik 文章確認的可用工具：Lean（數學證明語言，可自動驗證定理）；Claude 和 Deepseek 4 Pro（Vitalik 確認足以用於編寫 Lean 證明）；Leanstral（1190 億參數開放權重模型，專門針對 Lean 編寫微調，可在本地運行，基準測試表現優於許多規模更大的通用模型）。

常見問題

Vitalik 為何認為以太坊應成為「安全核心」？

根據 Vitalik 的文章，以太坊與作業系統核心類似，承載著社會數位化過程中最高級別的信任。他指出，安全核心的設計目標是讓其安全性達到不允許漏洞程式碼氾濫的標準，並將所有 AI 帶來的額外算力投入到提升安全核心的安全性上。

形式化驗證為何特別適合 STARK、ZK-EVM 等技術？

根據 Vitalik 的分析，這些技術的共同特點是「目標遠比實現簡單」——其安全屬性可用數學語言清晰定義，但具體實現極為複雜，恰恰是形式化驗證最能發揮作用的場景。

Vitalik 如何建議開發者實際使用 AI 輔助形式化驗證？

根據 Vitalik 的文章，他建議讓 AI 編寫 Lean 程式碼和數學證明，用戶最終只需核查被證明的語句是否符合預期，而無需自行編寫繁瑣的底層證明代碼。他確認 Claude、Deepseek 4 Pro 和 Leanstral 是目前可用的主要工具。