Vitalik最新长文：AI时代，代码如何变得更安全？

编者按：AI时代的代码安全悖论

随着 AI 编程能力的快速提升，软件安全正面临一个新的悖论：AI 可以更高效地生成代码，也可以更高效地发现漏洞。对加密行业而言，这一问题尤其关键。智能合约、ZK 证明、共识算法和链上资产系统一旦出现缺陷，后果往往不是普通软件报错，而是不可逆的资金损失和信任崩塌。

Vitalik 在本文中讨论的，正是 AI 时代代码安全的另一条路径：形式化验证。简单来说，它不是依赖人类审计员逐行检查代码，而是把程序应当满足的性质写成数学命题，再用机器可检查的证明去验证这些性质是否成立。

什么是形式化验证？

过去，形式化验证因门槛高、过程繁琐，一直停留在相对小众的研究和工程领域；但随着 AI 能够辅助编写代码和证明，这套方法正在重新获得现实意义。

文章的核心判断并不是「形式化验证可以解决一切安全问题」。相反，Vitalik 反复提醒，所谓「可证明安全」并不等于绝对安全：证明可能遗漏关键假设，规范本身可能写错，未被验证的代码、硬件边界和侧信道攻击也可能成为新的风险来源。但它依然提供了一种更可靠的安全范式：用多种方式表达开发者的意图，再让系统自动检查这些表达是否彼此兼容。

形式化验证在以太坊中的重要性

这对以太坊尤为重要。未来的以太坊将越来越依赖复杂底层组件，包括 STARK、ZK-EVM、抗量子签名、共识算法和高性能 EVM 实现。这些系统的实现极其复杂，但其核心安全目标往往可以被相对清晰地形式化。

也正是在这类场景中，AI 辅助形式化验证有可能发挥最大价值：让 AI 负责编写高效代码和证明，让人类负责检查最终被证明的命题是否真的对应自己想要的安全目标。

从宏观角度看网络安全

从更宏观的角度看，这篇文章也是 Vitalik 对 AI 时代网络安全的一次回应。面对更强的 AI 攻击者，答案不是放弃开源、放弃智能合约，或重新依赖少数中心化机构，而是把关键系统压缩成更小、更可验证、更可信的「安全核心」。

AI 会让粗糙代码大量增加，但也可能让真正重要的代码变得比过去更安全。

形式化验证的基本逻辑与案例

特别感谢 Yoichi Hirai、Justin Drake、Nadim Kobeissi 和 Alex Hicks 对本文提供反馈与审阅。

过去几个月里，一种新的编程范式正在以太坊前沿研发圈以及计算领域的许多其他角落迅速兴起：开发者直接使用非常底层的语言编写代码，例如 EVM 字节码、汇编语言，或使用 Lean 编写代码，并通过在 Lean 中撰写可自动检查的数学证明来验证其正确性。

如果运用得当，这种方式既有可能生成极其高效的代码，也可能比过去的软件开发方式安全得多。Yoichi Hirai 将其称为「软件开发的最终形态」。

形式化验证的实际应用

为了给出一个相对简单、但仍然有意思的例子，我们可以看一个关于斐波那契数列的基本定理：每三个数中就有一个偶数，其余两个则是奇数。

这个论证对人类来说是有说服力的。但如果你想证明的东西复杂一百倍，而且你真的非常想确认自己没有犯错，该怎么办？这时，你就可以构造一个能让计算机也信服的证明。

形式化验证的局限性

形式化验证不是万能药。但在某些场景下，它尤其适用：也就是目标远比具体实现更简单的时候。这一点在以太坊下一次重大迭代中需要部署的一些最棘手技术里尤为明显，例如抗量子签名、STARK、共识算法和 ZK-EVM。

以下是 Leanstral 对这一定理含义的总结：passive_secrecy_le_ddh 定理是一个紧致归约，表明在随机预言机模型（Random Oracle Model）下，X3DH 的被动消息保密性至少和 DDH 假设一样难以攻破。

形式化验证的未来展望

强大的 AI 漏洞发现能力带来的挑战确实严峻，但它是一种过渡性挑战。等尘埃落定、我们进入新的均衡之后，我们将抵达一个比过去更有利于防守方的状态。

形式化验证不会解决我们所有问题。但如果我们希望建立一种互联网安全模型，而不是让所有人都去信任少数强大组织，那么我们就需要能够转而信任代码——包括在面对强大 AI 对手时，依然能够信任代码。