维塔利克·布特林驳斥AI网络安全末日论

Ethereum founder refutes the argument that "AI hackers will make cybersecurity unsolvable": verification tools will give defenders structural advantages

On September 17, Ethereum founder Vitalik Buterin publicly refuted the view that "as AI hacking capabilities continue to increase, cybersecurity will become undefensible." He pointed out that advanced verification tools are expected to ultimately provide structural advantages to defenders.

According to a statement issued by Butrin on September 17, approximately 90% of his personal net worth still holds cryptocurrencies. This fact itself confirms his view: people who continue to hold cryptocurrencies are actually betting that secure digital systems can withstand increasingly powerful automated attacks.

Core Argument: Formal Verification and Mathematical Proof

The core of Butrin's argument lies in "Formal Verification." This is a technique that uses mathematical specifications and proofs to determine whether software is operating in accordance with predefined attributes. He likened this to high-level mathematical theorem proof, arguing that AI with sufficient capabilities could help prove that "the program is safe," even if the logic of the software itself is very complex.

He criticized the common view that "AI hacking means cybersecurity is dead." On the contrary, he believes that once people straighten out the technical system, cybersecurity is inherently biased towards the defender. Anyone who continues to hold cryptocurrencies, including himself, implicitly supports this belief.

然而，以太坊基金会关于形式化验证的技术文档指出了一种重要的局限性：证明只能确立软件满足所检查的规范，并不能自动保证开发者正确定义了所有安全属性。如果规范选择不当或不完整，未被证明覆盖的行为可能会导致安全隐患。布特林在帖子中也强调了这一点，指出如果将“安全性”定义得过于狭隘，可能会遗漏涉及协议、服务器、数据库、网络层、缓存或其他支持组件的攻击路径。因此，他的建议方向是验证更完整的系统，而不是仅将一小部分模块标记为关键安全模块。

以太坊已在实践中测试AI辅助安全

尽管目前系统距离实现全系统安全的自动证明仍有距离，但以太坊研究人员已经在安全工作中使用AI。今年7月，以太坊基金会协议安全团队报告称，协调运作的AI代理在以太坊使用的系统中发现了真实缺陷。其中一项确认的发现涉及Rust libp2p的Gossipsub网络实现中存在的一个可远程触发的崩溃漏洞。

该漏洞被记录为CVE-2026-34219。美国国家漏洞数据库记录显示，0.49.4之前的版本可能通过精心构造的PRUNE消息导致算术溢出，从而在Gossipsub退避处理期间引发远程崩溃。版本0.49.4修复了此问题。

The foundation's security team said discovering vulnerabilities is not the most difficult part of the AI workflow. Researchers have found that AI agents often generate seemingly convincing reports, but these reports may involve unreachable execution paths, failures that occur only during debugging, or technically verified properties that are weaker than expected. Therefore, independent reproduction remains a prerequisite for the team to accept discoveries. Automated inspections and manual reviews are indispensable because agents can produce a seemingly valid certificate but fail to constrain the software behavior that researchers really want to test. This experience is described as a "triage" problem: AI can generate a large number of candidate vulnerabilities, but researchers still need to determine whether each problem is reachable and meaningful in a production environment.

Formal verification enters the Ethereum protocol roadmap

The Ethereum Foundation has incorporated formal verification into its current protocol research program. In a September 7 protocol priority update, the foundation announced that formal verification will become a common tool across multiple years of research areas. These areas cover privacy, state management, zkEVM development, post-quantum security and other protocol components, and work will continue into 2029.

roadmap states that the development of L1zkEVM is expected to drive the development of formal verification tools, workflows, and verified cryptographic components. Ethereum researchers are working to build a system that allows verifiers to ultimately verify concise proof of execution rather than independently re-executing each block.

此外，8月启动的一项以太坊基金会项目“better.codes”正在结合AI代理与机器检查的证明。该项目允许研究人员将AI系统引导至在Lean语言中形式化的密码学健全性问题，而Lean内核则检查提交的证明是否满足固定的定理陈述。

基金会的第二季度资金报告还列出了进一步将大型语言模型与形式化方法相结合的工作，包括ETHeorem（用于检查以太坊客户端实现是否符合规范）、SPECA和LeanAgent（用于自动化协议合规性工作），以及涉及RISC-V zkVM基础设施的形式化验证项目。

布特林9月17日的评论延续了现有的研究方向，而非宣布新的升级或计划中的硬分叉。他的帖子并未提及新的EIP（以太坊改进提案）、部署日期或要求所有以太坊程序必须经过形式化验证的强制规则。

当前证据显示AI同样增强了进攻能力

最近的网络安全研究支持了AI使攻击者能力增强的担忧，尽管防御性应用也在扩展。Anthropic在其9月的威胁情报报告中表示，观察到恶意行为者利用AI自动化漏洞研究、漏洞开发和多目标活动。该公司指出，一些操作者维持着可以持续进行漏洞研究的自动化工作流。

Anthropic早前的研究也在大规模上发现了类似证据。其协调披露仪表板显示，截至8月26日，该公司已披露了392个开源项目中由AI发现的2,300个漏洞，其中421个已在上游得到修补。

Anthropic也将该技术描述为对防御有用的工具。其Project Glasswing倡议报告称，与安全和软件供应商合作，使用前沿模型在恶意行为者利用之前定位高危及严重级别的漏洞。

然而，进攻侧的影响依然可测量。Anthropic在6月的一项研究考察了2025年3月至2026年3月期间与恶意网络活动相关的832个账户，发现威胁行为者在网络操作的多个阶段使用AI。Anthropic的9月报告还表示，调查人员确定了针对安全设备和政府目标的AI构建漏洞管道的操作者，其中一些活动产生了攻击者在自己的测试环境中验证过的未知漏洞。

此前，布特林也曾反驳过另一种观点，即AI驱动的安全风险会严重损害对比特币的信心。他表示，网络层问题通常可以通过软件和挖矿基础设施升级来解决，而比特币哈希值或工作量证明机制的实际突破被认为极不可能发生。