Vitalik Buterin：AI不會終結加密安全

以太坊聯合創始人Vitalik Buterin發文反駁“ai黑客將使網絡安全必敗”的說法，稱網絡安全在認真做防禦後天然偏向防守方，ai不會讓加密安全崩盤。

他給出的核心路徑是形式化驗證：用數學證明軟件滿足事先寫死的安全性質，而不是靠人工翻代碼賭沒漏。他的類比是，若ai能證明納維-斯托克斯方程與費馬大定理，就能把“這段程序是安全的”也證成定理，哪怕程序本身很複雜。他同時承認“安全”的定義極易寫窄，漏掉協議、服務器、數據庫、網絡層、緩存和依賴供應鏈後，證明本身會變成假安全感。

他把自己的倉位綁進這個判斷：約90%淨資產仍在加密資產裏，並稱繼續持有加密本身就是在賭防禦能跟上更強的自動化攻擊。早前他已否定ai會在兩年內把比特幣砸掉50%的預測，認爲哈希與工作量證明被ai從根上擊穿的概率極低，客戶端、礦池等無需社會共識即可修補的層纔是過渡難點，同一邏輯也適用於以太坊。

落地項目已在鋪：arklib推進stark的全驗證實現，evm-asm用匯編重寫整套evm並配正確性證明，vyper與verity兩條智能合約語言都在做形式化驗證。以太坊基金會協議安全組已用ai智能體掃協議代碼並獨立復現漏洞，確認過rust libp2p gossipsub裏可遠程觸發的崩潰，編號cve-2026-34219，由特製prune消息觸發退避計算溢出，0.49.4版本已修。

研究側把驗證做成橫切工具而不是單點審計。基金會9月協議優先級把形式化驗證鋪到隱私、狀態、zkevm、後量子等持續到2029年的軌道上；8月啓動的better.codes讓研究者把密碼學健全性問題寫進lean，由lean內核檢查證明是否命中固定定理；資金報告裏還有etheorem對照客戶端與規範、speca與leanagent做協議合規，以及riscv zkvm相關驗證。他強調可擴展與隱私鏈沒有這條路就沒有未來，驗證必須覆蓋整棧，不能只圈“關鍵模塊”。

攻防兩邊同時加速。anthropic披露前沿模型已在加速漏洞研究、利用開發和多目標戰役，到8月26日已向392個開源項目披露2300個ai發現的漏洞，其中421個已上游修補；其威脅情報還記錄到針對安全設備和政府目標的ai利用流水線。防守側同一套模型也被用來做披露前排查。他另舉2026年一例：某後量子密碼庫自稱“已驗證”仍被打穿，原因通常是驗證覆蓋不全或規範漏寫關鍵性質。形式化驗證、測試與類型系統必須疊用，單一工具給不出全覆蓋保證。

市場機制上，這是事件驅動的敘事交易而非即時資金搬家：繼續持幣的一方等於做多“防禦成本下降快於攻擊成本下降”，以太坊l1研究、zkevm、stark工具鏈和驗證語言受益；未驗證合約、依賴供應鏈和用戶意圖層（釣魚、誤授權、agent亂簽名）承壓。進攻方買的是更便宜的漏洞流水線，防守方買的是可機器檢查的規範與證明；資金不會因爲一篇帖子立刻改道，但安全溢價會從“審計報告頁數”轉向“整棧是否可證”。鏈上未見與該發言直接對應的異常大額 eth 流向，價格反應主要停在敘事層。

來源：公開信息