Vitalik Buterin 表示，人工智能可能重塑加密系統被攻擊與防禦的方式，並推動基礎設施走向以數學方式嚴格驗證的軟件。
Buterin 文章勾勒 AI 威脅
這位以太坊聯合創辦人指出，愈來愈強大的 AI 模型將大幅降低在複雜軟件中尋找及利用漏洞的門檻。
Buterin 認為，一旦 AI 工具開始自動化發現漏洞，加密基建中的漏洞將變得格外可怕，這點在資安研究社群中亦被廣泛關注。
他特別點名 以太坊 (ETH) 基礎設施、共識機制以及後量子密碼學，認為這些都是需要優先加強防禦的關鍵目標。
Buterin 表示，開發者不應再只依賴傳統審計，而應採用「形式化驗證」——一種透過數學方法證明程式碼在特定條件下必然按預期運作的做法。他表示，這將成為更可靠的安全基礎。
延伸閱讀： Crypto Funds Bleed $1.07B As Iran Tensions End Six-Week Inflow Run
以形式化驗證作為防線
「AI 讓你可以用精準度為代價，快速產出大量程式碼，而形式化驗證則把精準度還給你。」Buterin 如此寫道。
他反駁了部分研究人員的悲觀看法——這些人認為 AI 產生的軟件根本無法完全信任。Buterin 則提出較為樂觀的觀點。
Buterin 相信，AI 協助編碼結合驗證工具，最終能產出比人類單獨開發更強韌的軟件。
他同時提到一些現正活躍的專案，例如 Arklib 和 evm-asm，專注於強化密碼學基礎設施與以太坊虛擬機（EVM）軟件的安全性。
不過，這篇文章亦警告，形式化驗證並非萬靈丹。即使是經過數學證明的系統，也可能因為開發者驗證了錯誤的前提，或是攻擊手法發生在驗證範圍之外的程式路徑，而出現失誤。
Buterin 的安全布局與紀錄
Buterin 描繪了一個可能的未來：關鍵數碼基建將逐步集中在較小、經嚴格隔離與高度驗證的「安全核心」系統之中，而重要性較低的應用則在權限受限的環境下運行。
今年以來，這位以太坊聯合創辦人多次回到 AI 與安全的主題。二月時，他建議應將 AI 帶來的生產力提升，在「速度」與「安全」兩方面作折衷分配；到了五月，他又公開支持如 Lean 等形式化驗證工具，作為高保障開發的基石。他最新的文章進一步延伸上述論點，提出更廣泛的主張：在鏈上世界與傳統互聯網系統中，數學證明將是對抗 AI 驅動攻擊工具最具說服力的答案之一。
下一篇閱讀： Iran Settles Hormuz Shipping Cover In Bitcoin, Eyes $10B Haul