以太坊联合创始人 Vitalik Buterin 于 5 月 18 日表示，人工智能可能通过形式化验证工具提升加密系统安全性，重点涉及以太坊基础设施、共识系统、密码学和零知识技术。按他的说法，AI 辅助的证明系统能让开发者用数学方法验证软件行为，而不是只依赖审计和测试。
用数学证明代码行为，而不只看测试结果
Buterin提到，形式化验证的核心，是让计算机自动检查数学证明，确认程序在预设条件下按预期运行。与常规软件测试相比，这种方法试图直接缩小“设计目标”和“实际执行”之间的不确定性。问题也很现实：这类证明过去通常需要人工编写，速度慢，门槛高，落地成本不低。
他认为，AI 可以减轻这部分负担。具体包括同时生成代码、证明以及额外测试结构，从而让开发流程更快，也让验证覆盖面更大。研究员 Yoichi Hirai 曾将这种路径称为软件开发的“最终形态”，但 Buterin也强调，人类仍需判断规格说明本身是否正确，这一步不能交给机器替代。
以太坊相关项目已在推进验证型基础设施
Buterin列举称，以太坊相关项目已在多个方向采用这类方法，包括抗量子签名、STARK 证明系统、拜占庭容错共识协议，以及 ZK-EVM 基础设施。其中，Arklib 正在推进经过形式化验证的 STARK 实现；evm-asm 项目则在使用 RISC-V assembly 构建一个经过数��验证的以太坊虚拟机。
这些案例说明，形式化验证不再只是理论讨论，已经进入具体工程环节。尤其在共识机制、密码学组件和虚拟机层面，一旦出现漏洞，影响往往会沿着基础设施向上扩散，波及更大范围的链上应用和资金安全。
形式化验证并非万能，错误规格仍会带来风险
Buterin同时承认，形式化验证存在边界。即便软件已经过验证，只要规格说明写错，或者漏洞出现在验证范围之外，系统仍可能失效。也就是说，验证能证明“代码符合设计”，却不能自动证明“设计本身没有问题”。短板依然存在。
即便如此，他仍认为数学验证能减少关键系统中的不确定性。随着 AI 生成软件的范围扩大，共识机制和密码学基础设施这类关键模块，可能需要更深入的验证。Buterin还描述了一种分层结构：把软件拆分为安全层和非安全层，由更小的安全核心处理敏感基础设施，权限受限的低风险系统则放在外层运行。
AI攻防同步升级，防守方希望拿到更强工具
Buterin将这场讨论与自动化攻击能力提升直接联系起来��他认为，在 AI 辅助攻击越来越复杂的情况下，防守方终于可能获得更强的工具。他还提到 Mozilla 在内部加固系统、应对自动化漏洞发现工具方面的经验。
这番表态出现之际，DeFi（去中心化金融）平台仍持续遭遇与智能合约漏洞和基础设施薄弱环节相关的攻击。对以太坊生态而言，AI 是否能把形式化验证从高门槛方法推向更广泛的工程实践，已成为安全讨论中的一个核心问题。