导语：以太坊联合创始人 Vitalik Buterin 在其 5 月 18 日发布的博客文章中提出，人工智能尽管存在“幻觉”和生成漏洞代码的问题，但如果与形式化验证结合，可能成为软件行业迄今最强大的防黑客工具。
AI 的速度代价
Buterin 认为，AI 可以快速生成大量代码，但其可靠性低于人类开发者精心编写的代码。在管理数十亿美元的智能合约中，此类错误可能带来生存性风险。他披露自己约 90% 的净资产持有在 ETH 中，这使他对加固以太坊生态的兴趣兼具个人与技术维度。
用数学证明替代部分测试
形式化验证通过数学证明表明代码在所有可能场景下行为正确，而不是仅依赖针对特定案例的测试。Buterin 指出，Lean 定理证明器是关键工具，它允许开发者编写可被机械检查的证明，形成传统代码审查难以匹敌的数学确定性。对于“攻击者也能用 AI 更快找漏洞”的反对意见，他称这一担忧是“短暂的”：经过确认的证明具有永久性，而攻击者找到漏洞是一次性事件。
以太坊的高风险应用
Buterin 强调，后量子密码是形式化验证可发挥作用的领域。随着量子计算机逐步逼近破解现有加密方案，以太坊和其他区块链需要抗量子签名，形式化验证能提供仅靠测试无法提供的信心。零知识证明是另一优先事项。ZK 技术通过 ZK-EVM 和 rollups 支撑以太坊扩容战略，而这些高度复杂的密码学构造中，一个细微漏洞就可能危及整个 Layer 2 网络的完整性。他提到两个进行中的项目：Arklib，一个经过形式化验证的 STARKs 实现；以及 evm-asm，一个旨在让以太坊虚拟机更易于形式化分析的 EVM 抽象。
信任模式转变与两大限制
Buterin 还指出，形式化验证不仅提升安全性，也改变用户需要信任的对象。用户不必逐行审计整个代码库，而可以验证关于代码行为的高层断言。不过，他提出两个主要限制：其一是规范风险，形式化验证只能证明代码符合规范，如果规范本身错误，证明便毫无价值；其二是硬件，软件可以形式化验证，但运行它的物理芯片无法以同等严格程度验证，受感染的处理器可能破坏即使经过完美验证的代码。
从航空国防走向更广泛软件
尽管存在这些限制，Buterin 仍将 AI 辅助的形式化验证描述为软件开发潜在的“最终形态”。形式化验证的根源可追溯至 20 世纪 50 至 60 年代，但实际应用长期局限于航空航天、国防等安全关键行业，因为这些领域失败成本足以证明数学证明成本合理。如今变化在于经济性：AI 大幅降低编写代码和证明所需的人力，可能使形式化验证对更广泛软件变得可行，并为以太坊提供更持久的防黑客屏障。