Vitalik：不认同「AI 黑客将使网络安全无解」，以太坊将推进形式化验证所有程序

Foresight News 消息，Vitalik Buterin 发推表示，其不认同「AI 黑客意味着网络安全注定失败」的观点。一旦方法到位，网络安全天然偏向防守方；继续持有加密资产（其称约占自身净资产 90%）本身就是在押注这一判断。其给出的简化表述是：若 AI 能证明纳维–斯托克斯方程与费马大定理，也能把「该程序是安全的」证明为数学定理，即使程序很复杂。

Vitalik 强调难点在于「安全」极易被定义得过窄，从而漏掉大量攻击面，定义必须可读、可叠加；对消息协议、沙箱、SNARK、FHE 等关键组件，验证定义是否充分通常比直接扫代码更可行。过去形式化验证常只覆盖自认的关键模块，其余代码仍可能成为突破口；其主张应验证所有程序，包括数据库、网络与缓存等，并认为现代 AI 已使这一路径更现实。其称这不是「好人抢在坏人之前找漏洞」，而是让代码先天更抗攻击；没有这条路径，尤其带扩容与隐私的区块链将没有未来，以太坊未来几年将朝此方向推进。