币圈界报道：

布特林力挺形式化验证：防御者有望赢得技术代差

9月17日，以太坊创始人维塔利克·布特林公开回应关于“人工智能将使网络安全彻底失效”的担忧。他指出，随着验证技术的演进，尤其是基于数学逻辑的形式化方法，防御方正逐步获得系统性优势。

持有加密资产即在押注系统韧性

布特林披露其个人财富约九成仍以加密货币形式持有。这一举动被解读为对数字资产底层安全性的坚定信任，也间接反映其核心立场：持续持有者本质上是在支持一个能够抵御智能攻击的可信系统。

用数学定理思维重构软件安全性

布特林的核心主张聚焦于“形式化验证”——一种通过精确数学规范来证明程序行为符合预期属性的技术。他将其类比为高等数学中的定理推导，认为具备足够算力的AI可协助完成复杂系统的安全证明。

他反对“一旦出现智能攻击，网络便无从防守”的悲观预测，认为只要技术架构清晰，防御始终具备内在优势。任何坚持持有加密资产的行为，都是对这一信念的实践投票。

规范定义不当可能埋下隐藏风险

尽管前景乐观，以太坊基金会的技术文档警示：形式化验证仅能确认程序是否满足预设规范，无法保证这些规范本身涵盖所有潜在威胁。若安全边界设定过窄，诸如协议、数据库、网络栈或缓存机制等非核心模块中的漏洞仍可能被遗漏。

因此，布特林呼吁验证范围应向更完整的系统架构扩展，而非仅聚焦少数关键组件。唯有如此，才能避免因局部验证而产生的虚假安全感。

AI已介入真实漏洞挖掘实战

以太坊研究团队近期报告称，部署的协作式AI代理已在生产环境中识别出实质性缺陷。其中一项成果是发现Rust libp2p库中Gossipsub实现的一个远程触发崩溃漏洞，编号CVE-2026-34219。

该漏洞存在于0.49.4版本之前的代码中，可通过构造特定PRUNE消息引发算术溢出，导致服务中断。该问题已在后续版本中修复。

然而，团队指出，AI生成的报告常包含不可达路径、调试专用异常或形式上成立但语义弱化的证明。因此，人工复现仍是接受发现的必要门槛。整个流程本质上是一种“筛选分诊”：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个开源项目中的2300个漏洞，其中421个已完成修复。这些成果部分归功于其Project Glasswing计划，该计划与供应商合作，在攻击者利用前定位高危漏洞。

然而，进攻端影响同样显著。6月至2026年3月期间，调查显示832个账户涉及多阶段AI驱动的恶意活动。部分攻击者甚至构建了可在测试环境验证未知漏洞的攻击管道，目标包括安全设备与政府机构。

此前布特林也曾否认AI会动摇比特币根基，认为网络层问题可通过升级解决，而工作量证明机制本身极难被突破。