Vitalik Buterin 表示，人工智能可能重塑加密系统被攻击和防御的方式 的进展，将推动基础设施迈向经数学验证的软件。
布特林在文章中勾勒 AI 威胁
这位以太坊联合创始人指出，愈发强大的 AI 模型 将大幅降低在复杂软件中发现并利用漏洞的门槛。
布特林称，一旦 AI 工具开始将漏洞发现过程自动化，加密基础设施中的缺陷就更加令人担忧，这一观点也在安全研究社区中广泛被认同。
他特别提到 Ethereum (ETH) 的基础设施、共识机制以及后量子密码学，是需要优先加强防御的重点目标。
布特林表示，开发者不应再只依赖传统审计，而应采用形式化验证这一方法，在既定条件下以数学方式证明代码按预期运行。
延伸阅读： Crypto Funds Bleed $1.07B As Iran Tensions End Six-Week Inflow Run
形式化验证作为防御手段
“AI 让你可以以牺牲准确性为代价，写出海量代码，而形式化验证可以把准确性找回来。”布特林写道。
他反驳了一些研究者的观点，这些人认为 AI 生成的软件已经变得无法完全信任；布特林则给出了更为乐观的看法。
布特林认为，把 AI 辅助编程与验证工具结合，最终可能生成比人类单独编写更为稳健的软件。
他还点名了一些正在进行的项目，比如 Arklib 和 evm-asm，它们专注于保护密码学基础设施和以太坊虚拟机软件。
不过，这篇文章也警告，形式化验证并非万能。即便是经数学证明的系统，也可能因为开发者验证了错误的前提假设，或攻击路径落在验证范围之外而发生失败。
布特林的安全实践记录
布特林描绘了一个未来：关键数字基础设施会被收缩并集中到更小的“安全核心”系统中，这些系统被隔离并进行高强度验证，而不那么关键的应用则在受限权限下运行。
在今年，布特林多次回到 AI 安全这一主题。2 月，他建议将 AI 带来的生产力提升在“速度”和“安全性”之间进行分配；5 月，他又公开支持 Lean 等形式化验证工具，用于高保障开发。他最新的文章在此前论点基础上进一步延展，提出一个更广泛的主张：在区块链和传统互联网系统中，数学证明是应对 AI 驱动攻击工具的最可信答案。
下一篇阅读： Iran Settles Hormuz Shipping Cover In Bitcoin, Eyes $10B Haul