币圈界报道：

AI威胁未颠覆网络安全根基：Vitalik提出定义优先新范式

面对公众对人工智能引发新型网络攻击的广泛忧虑，以太坊联合创始人Vitalik Buterin明确表示，此类悲观情绪并不成立。他认为，只要建立合理的系统架构并引入更高效的验证机制，安全防线依然具备压倒性优势。

以数学为基石：安全可被形式化证明

Buterin以数学领域为例说明可能性：若人工智能能攻克纳维-斯托克斯方程或费马大定理，同样有能力将“该程序无漏洞”这一断言转化为可严格证明的数学命题，即便其结构极为复杂。

安全定义的精细化挑战与突破路径

他指出，“安全”的内涵远比表面复杂，需涵盖攻击者行为模式、数据泄露路径及软硬件故障场景等多重维度。因此，如何将这些抽象要求转化为人类可理解的高级语言，成为当前最关键的议题。尽管定义可能极其细致，但其覆盖范围通常远小于实际代码体量。

相较于直接扫描源码，验证定义的完整性更具可控性。随着工具进步，这一方法正变得日益可行。更关键的是，当多个团队采用不同安全标准时，程序若同时满足两者，则增强可信度；若存在冲突，则暴露核心风险点，推动系统优化。

全程序验证并非万能：差异存在于关键组件

Buterin承认，并非所有软件模块都适合采用高阶定义。例如用户界面部分，其定义规模往往接近实现代码本身。然而，在消息传递协议、沙箱隔离机制以及SNARKs、全同态加密等密码学构造中，定义与实现之间存在显著差距。

过去开发者常仅对自认为关键的部分进行验证，其余则放任不管。但在当今AI辅助验证能力大幅提升的背景下，这种局限已不再合理。他强调，真正的出路不是依赖“好人先发现漏洞”，而是从根本上提升代码的抗脆弱性。否则，专注于可扩展性与隐私保护的区块链系统将难以为继。