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

以太坊创始人反驳“AI黑客将使网络安全无解”论调：验证工具将赋予防御方结构性优势

9月17日，以太坊创始人维塔利克·布特林（Vitalik Buterin）公开驳斥了“随着AI黑客能力不断增强，网络安全将变得无法防守”的观点。他指出，先进的验证工具有望最终为防御者带来结构性的优势。

根据布特林于9月17日发布的声明，其个人净资产的约90%仍持有加密货币。这一事实本身也侧面印证了他的观点：持续持有加密货币的人，实际上是在押注安全的数字系统能够抵御日益强大的自动化攻击。

核心论点：形式化验证与数学证明

布特林的论证核心在于“形式化验证”（Formal Verification）。这是一种利用数学规范和证明来确定软件是否按照预定义属性运行的技术。他将此比作高级数学定理证明，认为具备足够能力的AI可以帮助证明“该程序是安全的”，即使软件本身的逻辑非常复杂。

他批评了那种认为“AI黑客意味着网络安全已死”的普遍看法。相反，他认为一旦人们理顺技术体系，网络安全本质上是偏向防御方的。任何继续持有加密货币的人（包括他自己），都在隐含地支持这一信念。

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

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

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

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

基金会的安全团队表示，发现漏洞并非AI工作流程中最困难的部分。研究人员发现，AI代理经常生成看似令人信服的报告，但这些报告可能涉及不可达的执行路径、仅在调试时出现的故障，或者技术上通过了验证但实际证明的属性弱于预期。因此，独立复现仍是团队接受发现的必要条件。自动化检查和人工审查不可或缺，因为代理可能会产生一个看似有效的证明，却未能约束研究人员真正想要测试的软件行为。这种经验被描述为一种“分诊”问题：AI可以生成大量候选漏洞，但研究人员仍需确定每个问题在生产环境中是否可达且具有意义。

形式化验证进入以太坊协议路线图

以太坊基金会已将形式化验证纳入其当前的协议研究计划。在9月7日的协议优先级更新中，基金会宣布形式化验证将成为跨越多项多年研究领域的通用工具。这些领域涵盖隐私、状态管理、zkEVM开发、后量子安全以及其他协议组件，相关工作将持续至2029年。

路线图指出，L1 zkEVM的开发有望推动形式化验证工具、工作流和经过验证的密码学组件的发展。以太坊研究人员正致力于构建一个系统，使验证者最终能够验证简洁的执行证明，而不是独立重新执行每一个区块。

此外，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驱动的安全风险会严重损害对比特币的信心。他表示，网络层问题通常可以通过软件和挖矿基础设施升级来解决，而比特币哈希值或工作量证明机制的实际突破被认为极不可能发生。