Vitalik Buterin 駁斥了日益強大的人工智慧駭客將使網路安全實際上無法取勝的說法，並於 9 月 17 日主張，先進的驗證工具最終可能為防禦方帶來結構性優勢。
摘要
- 根據 Buterin 本人 9 月 17 日的聲明，他淨資產的 90% 仍留在加密貨幣中。
- 根據 Buterin 的論點，AI 輔助的形式驗證可以幫助證明軟體滿足既定的安全屬性。
- 以太坊的安全團隊已經使用 AI 代理來檢查協議程式碼並獨立重現漏洞。
- 以太坊研究人員現在將形式驗證視為跨越多個長期協議研究軌道的跨領域工具。
- Anthropic 表示，前沿 AI 可以加速攻擊，而其模型已識別出數千個漏洞。
Buterin 在 9 月 17 日於 X 上的貼文中寫道，他不同意日益普遍的觀點，即「AI 駭客意味著網路安全注定失敗」。他表示，繼續持有加密貨幣的人隱含地押注安全的數位系統能夠在更強大的自動化攻擊下存活，並補充說他自己約 90% 的淨資產仍留在加密貨幣中。
他的論點核心是形式驗證，這是一種使用數學規格和證明來確定軟體行為是否符合預定義屬性的技術。Buterin 以高階數學定理證明作為類比，表示足夠強大的 AI 可以幫助證明「此程式是安全的」，即使軟體本身很複雜。
Buterin 表示形式驗證可以有利於防禦方
Buterin 的論點並不將 AI 安全視為一場防禦研究人員只需在攻擊者之前找到漏洞的競賽。他的貼文反而描述了一種模型，其中開發人員定義系統必須滿足的屬性，然後使用自動化證明工具來確立實作遵守這些屬性。
以太坊自己的形式驗證文件以更狹義的術語描述了該技術。它表示形式驗證可以用數學證明智慧合約符合形式規格，對該規格中包含的屬性提供比普通測試更強的保證。
同一份以太坊文件指出了 Buterin 評論背後的一個重要限制。證明確立了軟體滿足被檢查的規格；它並不自動證明開發人員正確定義了每一個安全屬性。選擇不當或不完整的規格可能使行為落在證明之外。
Buterin 在他的貼文中也做出了同樣的區分。他主張，將「安全」定義得太狹隘可能會遺漏涉及協議、伺服器、資料庫、網路層、快取或其他支援元件等領域的攻擊路徑。因此，他提出的方向是驗證更多完整系統，而不是將一小組模組標記為安全關鍵。
Buterin 已經將 AI 輔助的形式驗證描述為軟體開發可能的「最終形式」。他早先的評論將該方法應用於以太坊共識、零知識系統和抗量子密碼學等領域。
以太坊已在測試 AI 輔助安全
以太坊研究人員已經在安全工作中使用 AI，儘管當前系統距離自動證明全系統安全仍很遙遠。
以太坊基金會協議安全團隊在 7 月報告稱，協調的 AI 代理已在以太坊使用的系統中發現了真實缺陷。其中一個已確認的發現涉及 Rust libp2p 的 Gossipsub 網路實作中可遠端觸及的崩潰。
這個漏洞被編號為 CVE-2026-34219。美國國家漏洞資料庫的記錄指出，0.49.4 之前的版本可透過精心構造的 PRUNE 訊息遠端導致崩潰，該訊息會在 Gossipsub 退避處理期間觸發算術溢位。版本 0.49.4 修復了此問題。
基金會的安全團隊表示，漏洞發現並不是 AI 工作流程中最困難的部分。研究人員發現，AI 代理經常生成看似可信的報告，涉及無法到達的執行路徑、僅限除錯的失敗，或是在技術上通過、卻證明了比預期更弱性質的形式化證明。
在團隊接受一項發現之前，獨立重現仍然是必要條件。基金會表示，需要自動化檢查與人工審查，因為代理可能產生看似有效的證明，卻未能約束研究人員真正想要測試的軟體行為。
基金會的經驗被描述為一個分類問題：AI 可以生成大量候選漏洞，但研究人員仍必須判斷每個問題在生產環境中是否可達且有意義。
形式化驗證正進入以太坊的協議路線圖
以太坊基金會已另行將形式化驗證納入其當前的協議研究計畫。在其9 月 7 日的協議優先事項更新中，基金會表示形式化驗證將作為橫跨其剩餘多年研究領域的通用工具。該文件涵蓋了到 2029 年為止在隱私、狀態、zkEVM 開發、後量子安全及其他協議元件方面的工作。
同一份路線圖指出，L1 zkEVM 的開發預計將推進形式化驗證工具、工作流程及經過驗證的密碼學元件。以太坊研究人員正朝著一個系統努力，讓驗證者最終驗證簡潔的執行證明，而不是獨立重新執行每個區塊。
另一個於八月啟動的以太坊基金會專案已經將 AI 代理與機器檢查的證明結合起來。better.codes 專案讓研究人員將 AI 系統導向一個以 Lean 形式化的密碼學健全性問題，而 Lean 核心則檢查提交的證明是否滿足固定的定理陳述。
基金會的第二季度資助報告列出了更多結合大型語言模型與形式化方法的工作。專案包括用於檢查以太坊客戶端實作是否符合規範的 ETHeorem、用於自動化協議合規工作的 SPECA 與 LeanAgent，以及涉及 RISC-V zkVM 基礎設施的形式化驗證。
以太坊更新後的技術路線圖賦予形式化驗證與隱私、零知識證明及後量子保護並列的角色。因此，Buterin 在 9 月 17 日的評論是延續既有的研究方向，而非宣布新的升級或預定的分叉。他的貼文並未指名新的 EIP、部署日期，或要求每個以太坊程式都必須接受形式化驗證的強制規則。
當前 AI 證據也顯示出更強的攻擊能力
近期的網路安全研究支持了這樣一種擔憂：即使防禦性用途不斷擴大，AI 正讓攻擊者變得更有能力。Anthropic 在其九月威脅情報報告中表示，它觀察到惡意行為者利用 AI 來自動化漏洞研究、漏洞利用開發及多目標攻擊行動。該公司表示，部分操作者維持著可持續進行漏洞研究的自動化工作流程。
Anthropic 早前的研究在大規模上發現了類似證據。其協調披露儀表板指出，截至 8 月 26 日，該公司已在 392 個開源專案中披露了 2,300 個由 AI 發現的漏洞，其中 421 個已在上游修補。
Anthropic 也將同一技術描述為對防禦有用。其 Project Glasswing 計畫報告稱，與安全公司及軟體供應商合作使用前沿模型，在惡意行為者能夠利用之前定位高風險與嚴重漏洞。
攻擊面依然可被量化。Anthropic 六月的研究檢視了 2025 年 3 月至 2026 年 3 月期間與惡意網路活動相關的 832 個帳號，發現威脅行為者在網路行動的多個階段中使用 AI。Buterin 早已駁斥了另一種論點，即 AI 驅動的安全風險可能嚴重損害人們對比特幣的信心。他表示，網路層問題通常可以透過軟體與挖礦基礎設施升級來解決，同時稱比特幣雜湊或工作量證明機制真正被破解的可能性極低。
Anthropic 九月的報告指出，其調查人員已識別出操作者利用 AI 建構的漏洞利用管道，針對安全設備與政府目標發動攻擊，其中一些行動產生了先前未知的漏洞，攻擊者並在自己的測試環境中加以驗證。
