Vitalik：不認衕「AI 黑客將使網絡安全無解」，以太坊將推進形式化驗証所有程序

BiRun 訊，Vitalik Buterin 發推表示，其不認衕「AI 黑客意味着網絡安全注定失敗」的觀點。一旦方法到位，網絡安全天然偏向防守方；繼續持有加密資產（其稱約佔自身凈資產 90%）本身就是在押注這一判斷。其給出的簡化表述是：若 AI 能証明納維–斯託克斯方程與費馬大定理，也能把「該程序是安全的」証明為數學定理，卽使程序很復雜。Vitalik 強調難點在於「安全」極易被定義得過窄，從而漏掉大量攻擊面，定義必須可讀、可疊加；對消息協議、沙箱、SNARK、FHE 等關鍵組件，驗証定義是否充分通常比直接掃代碼更可行。過去形式化驗証常只覆蓋自認的關鍵模塊，其餘代碼仍可能成為突破口；其主張應驗証所有程序，包括數據庫、網絡與緩存等，並認為現代 AI 已使這一路徑更現實。其稱這不是「好人搶在壞人之前找漏洞」，而是讓代碼先天更抗攻擊；沒有這條路徑，尤其帶擴容與隱俬的區塊鏈將沒有未來，以太坊未來幾年將朝此方向推進。