Vitalik驳斥AI黑客无敌论：形式化验证将赋予防御方结构性优势

9月17日，以太坊联合创始人维塔利克·布特林针对“人工智能驱动的黑客将使网络安全彻底失效”的观点作出回应。他明确表示，随着验证技术的发展，防御方正逐步获得结构性优势，而非被动受制于攻击者的自动化能力。

核心观点：形式化验证是破局关键

布特林的核心主张聚焦于形式化验证——一种基于数学规范来严格证明程序行为符合预设属性的技术。他将其类比为高等数学中的定理推导，认为具备足够智能的AI系统能够协助完成复杂系统的安全性论证，即使面对高度复杂的代码逻辑。

他批评了“AI崛起即意味着安全终结”的普遍误解。相反，他认为只要构建合理的验证框架，网络安全本质上更有利于防御方。而所有持续持有加密资产的人，包括他自己，实际上都在用实际行动支持这一信念。

局限性提醒：规范定义决定验证有效性

尽管前景乐观，以太坊基金会的技术文档也指出，形式化验证仅能确认软件是否满足所设定的规范，无法自动保证这些规范本身涵盖全部安全需求。若安全边界设定过窄，遗漏协议、网络层或数据库等环节，仍可能产生未被覆盖的风险。

因此，布特林强调应推动对完整系统而非局部模块进行验证，避免因过度聚焦单一组件而忽略整体架构中的潜在攻击路径。

实践进展：AI已助力发现真实漏洞

尽管全面自动化验证尚在发展中，以太坊团队已在实际项目中引入AI辅助安全检测。今年7月，其协议安全团队报告称，协同运作的AI代理成功识别出Rust libp2p库中Gossipsub实现的一个远程可触发崩溃漏洞。

该漏洞被编号为CVE-2026-34219，影响0.49.4版本之前的代码。攻击者可通过构造特定的PRUNE消息引发算术溢出，导致服务中断。版本0.49.4已修复此问题。

然而，研究人员发现，AI生成的报告常包含不可达路径、调试专属错误或形式上正确但实质意义有限的结论。因此，独立复现仍是接受发现的前提条件。这反映出当前阶段的挑战在于“分诊”——如何从大量候选结果中筛选出真正具有威胁性的缺陷。

路线图布局：形式化验证纳入长期规划

以太坊基金会已将形式化验证列为未来多年的关键研究方向。根据9月7日发布的协议优先级更新，该技术将成为跨领域通用工具，覆盖隐私保护、状态管理、zkEVM开发、后量子安全等多个核心模块，预计将持续至2029年。

在L1 zkEVM建设过程中，形式化验证有望推动简洁执行证明的普及，使验证节点无需重新执行全部区块即可确认结果，显著提升效率与可信度。

此外，8月启动的“better.codes”项目正探索将AI代理与机器检查相结合，引导其在Lean语言环境中解决密码学健全性问题，由内核自动校验提交的证明是否满足既定定理。

第二季度资金报告显示，基金会还正在推进多项融合大型语言模型与形式化方法的项目，包括ETHeorem（用于客户端合规性检查）、SPECA、LeanAgent（自动化协议验证）以及RISC-V zkVM基础设施的形式化验证工作。

现实双面：AI同时增强攻防两端

近期网络安全研究揭示，AI确实在提升攻击效率方面发挥重要作用。Anthropic在其9月威胁情报报告中指出，部分恶意行为者已建立可自动运行的漏洞挖掘与利用流程，覆盖研究、开发到多目标攻击的全链条。

截至8月26日，该公司通过AI发现并披露了392个开源项目中的2,300个漏洞，其中421个已被上游修复。这表明技术进步正被双刃剑式使用。

尽管如此，Anthropic也承认该技术可用于防御。其Project Glasswing倡议已与多家安全厂商合作，在攻击者利用前主动定位高危漏洞，形成前置防护机制。

然而，攻击侧的影响依然明显。6月至2026年3月期间的调查显示，832个恶意账户在多个操作阶段使用了AI技术，部分组织甚至构建了可在测试环境验证的未知漏洞管道，指向有组织、可持续的高级威胁活动。

此前，布特林也曾回应关于AI削弱比特币信心的担忧，指出网络层问题可通过软件和挖矿基础设施迭代解决，而比特币工作量证明机制本身突破的可能性极低。