Vitalik Buterin 表示，artificial intelligence could reshape how crypto systems are attacked 的進展，將改變加密系統遭受攻擊與防禦的方式，並推動基礎設施走向以數學方式驗證的軟體。
Buterin 論文概述 AI 威脅
這位以太坊共同創辦人主張，increasingly powerful AI models 將使發現與利用複雜軟體中的漏洞變得容易得多。
Buterin 指出，一旦 AI 工具開始自動化漏洞發掘，加密基礎設施中的錯誤將變得更加令人憂心，這一點也在資安研究社群中引起共鳴。
他特別點名 Ethereum (ETH) 的基礎設施、共識機制與後量子密碼學，認為這些都是必須優先加強防禦的目標。
Buterin 指出，開發者不應再僅依賴傳統稽核，而應採用形式化驗證這種方法，透過數學方式證明程式碼在既定條件下會如預期運作。said
延伸閱讀： Crypto Funds Bleed $1.07B As Iran Tensions End Six-Week Inflow Run
形式化驗證作為防禦手段
「AI 讓你能以犧牲準確性的代價，撰寫大量程式碼，而形式化驗證則把準確性還給你。」Buterin 如此寫道。
他反駁了一些研究者的觀點，這些人認為 AI 產生的軟體已無法被完全信任；相反地，他提出一種較為樂觀的看法。
Buterin 認為，AI 輔助程式設計搭配驗證工具，最終可能產出比人類單獨撰寫更強韌的軟體。
他同時提到 Arklib 與 evm-asm 等活躍專案，這些專案專注於保護密碼學基礎設施與以太坊虛擬機（EVM）軟體的安全。
不過，該篇文章也警告，形式化驗證並非萬靈丹。即便是經過數學證明的系統，當開發者驗證了錯誤的前提，或攻擊利用點位於驗證範圍之外時，仍然可能失效。
Buterin 的安全紀錄與願景
Buterin 描繪了一個未來：關鍵的數位基礎設施將集中於較小的「安全核心」系統中，這些核心被隔離且高度驗證，而重要性較低的應用程式則在受限權限下運作。
今年以來，這位以太坊共同創辦人多次重申 AI 資安這一主題。2 月時，他曾建議應在 AI 帶來的生產力提升之間，於速度與安全性之間做分配；到了 5 月，他又支持 Lean 等形式化驗證工具，用於高保證開發。他最新的文章則進一步延伸這些論點，提出更廣泛的主張：將數學證明視為應對 AI 驅動攻擊工具，在區塊鏈與傳統網路系統中最具說服力的解方。
下一篇閱讀： Iran Settles Hormuz Shipping Cover In Bitcoin, Eyes $10B Haul