Vitalik分析:以太坊（ETH）下一阶段,这些关键点将引领变革

“代码即法律”——这是区块链世界最初的信念之一。但如果代码本身存在bug呢？如果AI的介入让bug变得无处不在，又该怎么办？这是Vitalik最新长文试图回答的核心问题。先说说几个关键判断：以太坊的下一阶段，焦点在于安全与去中心化的平衡，推进扩容、零知识验证和抗量子技术；实现账户抽象以提升用户体验；强化隐私保护；借助AI增强协议证明能力；最终让手机、IoT设备都能完成链上验证，打造一个最安全、可靠、值得长期依赖的全球计算基础设施。

过去几个月里，一种新的编程范式正在以太坊的前沿研发圈以及更广泛的计算机科学领域迅速获得青睐：直接用非常底层的语言——比如EVM字节码、汇编语言，或者Lean——来编写代码，并使用自动可校验的、同样用Lean编写的数学证明来验证其正确性。如果操作得当，这种方式不仅能产出极其高效的代码，而且安全性远超以往的编程方法。有人将之称为“软件开发的终极形态”。

这篇文章就是要揭开这背后的原理，探讨形式化验证能做什么，以及在以太坊及其他领域中，它的弱点和局限性到底在哪里。

什么是形式化验证？

简单说，形式化验证就是用一种能被自动检查的方式，为数学定理编写证明。为了让你有个直观感受，我们来看一个关于斐波那契数列的基本定理：每第三个数字是偶数，其余的都是奇数。

1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377, 610, 987, 1597, 2584 ...

证明方法并不复杂，用数学归纳法，每次向前推进三步。先看基本情况：设F1=F2=1，F3=2，通过观察，这个命题（“Fi在3的倍数时为偶数，否则为奇数”）在x=3之前成立。然后是归纳情况：假设命题在3k+3之前成立，即已知F3k+1、F3k+2、F3k+3的奇偶性分别是奇数、奇数、偶数。接下来计算下一组三个数的奇偶性：从F3k+4到F3k+6，最终可以推导出命题对3k+6也成立。反复应用这个推论，就能确信规则对所有整数成立。

这个论证足以让人类信服。但如果要证明的东西复杂一百倍，而且你希望确保自己万无一失呢？这时，你就要给计算机提供一个它能信服的证明。

用Lean来表达相同的推理逻辑，看起来会和人类的证明有些不同。原因很简单：对计算机（传统意义上由if/then语句组成的确定性程序）来说直观的东西，与对人类直观的东西往往截然不同。在更复杂的证明里，你有时必须在每一步明确指定是哪条数学定律允许你这么做，甚至要用到一些晦涩的名字。但另一方面，你可以在一步之内展开庞大的多项式表达式，然后用类似“omega”或“ring”这样一行代码就完成证明。这种不直观和繁琐，解释了为什么尽管机器可验证的证明已存在近60年，这个领域依然小众。但另一方面，随着人工智能的快速发展，许多以前不可能的事情正在迅速成为可能。

当数学证明开始守护代码

读到这儿，你可能会想：好吧，计算机能验证数学定理的证明了，所以我们终于能搞清楚那些关于质数的疯狂新结论中，哪些是真的，哪些只是百页论文里的错误。

但抛开猎奇心理，这又能怎样呢？

答案很多。但对以太坊来说，最重要的一个应用是：验证计算机程序的正确性，尤其是那些执行密码学或与安全相关任务的程序。毕竟，计算机程序本质上是一个数学对象，证明其按某种方式运行，本身就是一个数学定理。

比如说，你想证明Signal这样的加密通信软件是否真的安全。你需要写下“安全”在数学上的具体含义。从高层次上看，你要证明的是，假设某些密码学假设成立，只有拥有私钥的人才能了解消息内容的任何信息。事实上，真的有一个团队在专门研究这个问题。他们提出了一个安全定理，其核心意思是：X3DH的被动消息保密性至少与随机预言模型下的DDH假设一样难。如果你将这个定理与AES加密实现正确的证明结合起来，就得到了Signal协议加密部分对被动攻击者是安全的完整证明。

类似的项目也证明了TLS和浏览器内其他密码学实现的安全性。如果你进行端到端的完全形式化验证，你证明的就不只是某种理论描述是安全的，而是用户运行的具体代码在实际中也是安全的。对用户来说，这极大地提升了免信任性——你不再需要检查整个代码库，只需验证关于它的那些声明是否成立。

当然，有几个重要的大前提需要牢记。尤其是关于“安全”这个词究竟意味着什么。人们很容易忘记去证明那些真正重要的声明；有时，要证明的声明并没有比代码本身更简单的描述方式；很容易在证明中偷偷引入最终并不成立的假设；也很容易决定系统中只有一个部分需要被形式化证明，结果却被其他部分甚至硬件中的严重漏洞击中。就连Lean实现本身也可能有bug。但在深入讨论这些细节之前，先看看正确完成形式化验证可能带来的理想状态。

为安全而生的形式化验证

计算机代码中的bug很可怕。当你把加密货币放入不可变的链上智能合约，而朝鲜可以在代码出现bug时自动抽干你的所有资金且你无法申诉时，这种可怕程度就翻倍了。当这一切被包装在零知识证明中时，bug就更可怕了——如果有人黑入零知识证明系统，他们可以提取所有资金，而我们完全不知道出了什么问题。

更可怕的是，当我们拥有强大的AI模型（比如再迭代两年后的Claude Mythos）可以自动化地发现这些bug时，情况会变得更加严峻。有些人对这种现实的反应是主张放弃智能合约的基本理念，甚至认为网络领域根本无法成为防御者对攻击者有不对称优势的领域。更糟糕的是，一些人认为唯一的解决方案是放弃开源。这对网络安全而言，将是一个黯淡的未来，尤其是对那些关心互联网去中心化和自由的人来说。

但我不这么认为。强大的AI漏洞寻找能力带来的挑战虽然严峻，但这是一个过渡性的挑战。一旦尘埃落定，我们进入新的平衡点，将获得一个比过去更有利于防御者的环境。Mozilla也同意这个观点：他们相信防御者终于有机会决定性地赢得胜利，因为缺陷是有限的，我们正在进入一个终于可以把它们全部找出来的世界。

网络安全的积极未来并不能完全依赖形式化验证或任何其他单一技术。它取决于什么？基本上可以看这张图：

几十年来，许多技术促成了漏洞数量的下降：类型系统、内存安全语言、软件架构的改进（沙盒化、权限控制，以及明确区分“可信计算基础”与“其他代码”）、更好的测试方法，还有不断丰富的安全编码知识库和经过审计的软件库。形式化验证在AI的辅助下，不是要成为全新的范式，而是这些既有趋势的强大翻跟斗。

形式化验证不是万能的。但它特别适合那些目标比实现简单得多的情况。这在以太坊下一个主要迭代中需要部署的一系列极其复杂的技术中尤为真实：抗量子签名、STARKs、共识算法以及ZK-EVMs。

STARK是一款极其复杂的软件，但它实现的核心安全属性却很容易理解和形式化：如果你看到一个指向程序P的哈希H、输入x和输出y的证明，那么要么STARK中使用的哈希算法被攻破了，要么P(x)=y。因此有了Arklib项目，它正试图创建一个完全经过形式化验证的STARK实现。更具野心的是evm-asm：一个构建完全经过形式化验证的整个EVM实现的项目。这里的安全属性没那么简单——目标是证明其等效于用Lean编写的另一个EVM实现。虽然有可能十个EVM实现都可证明地互为等价，却碰巧包含同一个致命缺陷，但这种可能性比现在单个实现存在这类缺陷要小得多。

另外两个重要领域是拜占庭容错共识——要形式化规范所有期望的安全属性同样困难，但考虑到bug曾经如此普遍，还是值得一试；以及智能合约编程语言——Vyper和Verity已经在进行形式化验证。在这些情况下，形式化验证的巨大价值之一在于这些证明真正是端到端的。最讨厌的bug往往是交互bug，潜伏在两个子系统交界处。对人类来说，端到端地推理整个系统太困难，但自动化的规则检查系统可以做到。

为效率而生的形式化验证

让我们再回到evm-asm。这是一个直接用RISC-V汇编编写的EVM实现。之所以选择RISC-V，是因为正在构建的ZK-EVM证明器通常通过证明RISC-V并将以太坊客户端编译为RISC-V来运作。因此，直接用RISC-V编写的EVM实现，理论上应该是你能得到的最快的实现。当然，为了真正实现端到端，你必须形式化验证RISC-V的实现本身——别担心，这方面的工作也已经存在了。

直接用汇编编写代码是五十年前的事。之后我们放弃了这一做法，转向高级语言，因为它编写和理解起来更快，对安全至关重要。借助形式化验证和AI的结合，我们有机会“回到未来”。具体来说，我们可以让AI编写汇编代码，然后编写一个形式化证明来验证该汇编代码具有所需属性。起码，所需属性可以仅仅是与那些为提高可读性而优化、用人类友好的高级语言编写的实现完美等价。用户只需验证一次证明，从那时起，他们就可以运行快速版本。这种方法极其强大，被称为“软件开发的终极形态”是有道理的。

形式化验证不是灵丹妙药

在密码学和计算机科学领域，有一个与形式化方法本身历史几乎一样悠久的传统：批评形式化方法（或更广泛地说，批评对“证明”的依赖）。这些文献中充满了实际案例。

从早期密码学手写的证明说起：Rabin曾提出一种加密函数，具有“可证明”的安全性——能从中找出消息的人也必须能分解n。然而Rivest很快指出，正是这一特性，在面对选择密文攻击时会导致全线崩溃。常见的规律是：围绕使加密协议更“可证明”而进行的设计，往往使它们变得更不“自然”，更容易在设计者未曾考虑的情况下崩溃。

回到机器可验证的证明和代码。2011年的一篇论文发现，经过形式化验证的C编译器中存在漏洞——一个PowerPC堆栈帧的16位位移字段溢出了，而语义没有规定对立即数宽度的限制。2022年的论文又发现了另一个bug。到了2026年，即使像Cryspen这样经过形式化验证的软件，依然出现了问题：在同一确定性输入下，不同平台产生了不同的公钥和签名；一个格式错误的密文就能让进程崩溃。

这些案例提醒我们：形式化验证并非万能。你可能会证明一切，却偏偏遗漏了真正重要的东西；也可能在证明中引入不成立的假设；还可能依赖了有bug的底层系统。但即便如此，形式化验证仍然是让防御者在这场不对称战争中重新占据优势的最有力武器之一。它不会解决所有问题，但它会让那些最关键的路径变得足够可靠——这对于以太坊的下一阶段来说，已经足够了。