作者： Vitalik Buterin
编译：佳欢，ChainCatcher
特别感谢 Yoichi Hirai、Justin Drake、Nadim Kobeissi 和 Alex Hicks 提供的反馈和审阅。
过去几个月里，一种新的编程范式在以太坊的前沿研发圈以及计算领域的许多其他角落迅速获得青睐：直接用非常底层的语言（例如 EVM 字节码、汇编语言）或 Lean 编写代码，并使用自动可校验的、用 Lean 编写的数学证明来验证其正确性。
如果操作得当，这不仅有可能输出极其高效的代码，而且比以往的编程方式要安全得多。Yoichi Hirai 将此称为"软件开发的终极形态"。
这篇文章将试图揭开其中的基本原理，探讨软件的形式化验证能做什么，以及在以太坊及其他领域中，它的弱点和局限性在哪里。
形式化验证是指以能够被自动检查的方式，为数学定理编写证明。为了给出一个相对简单但仍然有趣的例子，让我们来看看关于斐波那契数列的一个基本定理：每第三个数字是偶数，其余的是奇数。
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+2 + F3k+3 = 奇数 + 偶数 = 奇数 F3k+5 = F3k+3 + F3k+4 = 偶数 + 奇数 = 奇数 F3k+6 = F3k+4 + F3k+5 = 奇数 + 奇数 = 偶数
因此，我们从知道该陈述在 3k+3 前成立，推导出了该陈述在 3k+6 前成立。我们可以反复应用这个推论，从而确信该规则对所有整数都成立。
这个论点足以让人类信服。但是，如果你想证明复杂一百倍的东西，而且你想非常非常确定自己没有犯错呢？好吧，你可以给计算机提供一个它能信服的证明。
以下是它的具体呈现方式：
这是同样的推理逻辑，但用 Lean 表达出来。Lean 是一种常用于编写和验证数学证明的编程语言。
这看起来与上面给出的"人类"证明不同，原因很充分：对计算机直观的东西（在"计算机"的传统意义上，即由 if/then 语句组成的"确定性"程序，而不是大型语言模型）与对人类直观的东西截然不同。
在上面的证明中，你没有强调 fib(3k+4) = fib(3k+3) + fib(3k+2) 这个事实，而是强调了 fib(3k+3) + fib(3k+2) 是奇数，而 Lean 中名字相当宏大、叫做 omega 的策略会自动将其与它对 fib(3k+4) 定义的知识结合起来。
在更复杂的证明中，你有时候必须在每一步明确指定是哪条数学定律允许你采取当前这一步，有时还要用到像 Prod.mk.inj 这样晦涩的名字。
但另一方面，你可以在一步之内展开巨大的多项式表达式，并且只需通过像 "omega" 或 "ring" 这样的单行表达式来证明它是合理的。
这种不直观和繁琐很大程度上解释了为什么尽管机器可验证的证明已经存在了近 60 年，该领域却依然小众。但另一方面，由于人工智能的快速发展，许多以前不可能的事情现在正迅速成为可能。
到目前为止，你可能会想：好吧，计算机能够验证数学定理的证明了，所以我们终于能确定关于质数之类的疯狂新结论里哪些是真的，哪些只是百页 pdf 论文里的错误。
也许我们甚至能弄清楚望月新一关于 ABC 猜想的观点是否正确！
但抛开猎奇心不谈，那又怎样？
有很多可能的答案。但对我来说非常重要的一个答案是，验证计算机程序的正确性，特别是那些执行密码学或与安全相关任务的程序。
毕竟，计算机程序是一个数学对象，因此证明计算机程序以某种方式运行本身就是一个数学定理。
例如，假设你想证明像 Signal 这样的加密通信软件是否真的安全。你可以写下在这种背景下"安全"在数学上的含义。
从高层次来看，你要证明的是，假设某些密码学假设成立，只有拥有私钥的人才能了解有关消息内容的任何信息。在现实中，有许多不同的安全属性都非常关键。
事实证明，真的有一个团队在试图弄清楚正是这个问题！他们的一个安全定理看起来是这样的：
以下是 Leanstral 对其含义的总结：
如果你将其与 AES 加密实现正确的证明结合起来，你就得到了 Signal 协议的加密对被动攻击者是安全的证明。
类似的项目也证明了 TLS 和浏览器内密码学其他部分的实现是安全的。
如果你进行端到端的完全形式化验证，你证明的就不只是协议的某种理论描述是安全的，而是用户运行的具体代码在实际中也是安全的。
从用户的角度来看，这极大地提升了免信任性：为了完全信任代码，你不需要检查整个代码库，你只需检查关于它被证明的那些声明。
现在，有一些重要的大前提需要牢记，尤其是关于"安全"这个至关重要的词到底意味着什么。
人们很容易忘记证明那些真正重要的声明。很容易发现，有时候要证明的声明并没有比代码本身更简单的描述方式。
很容易在证明中偷偷引入最终并不成立的假设。也很容易决定系统中只有一个部分真正需要被形式化证明，结果却被其他部分（甚至硬件）中的严重漏洞击中。
就连 Lean 实现本身也可能有 bug。但在我们讨论所有这些恼人的细节之前，让我们首先深入探讨一下，正确且理想地完成形式化验证可能带来的乌托邦。
计算机代码中的 bug 很可怕。
当你把加密货币放入不可变的链上智能合约，而朝鲜可以在代码出现 bug 时自动抽干你的所有资金且你无法申诉时，代码中的 bug 就变得更加可怕。
当这一切被包装在零知识证明中时，bug 就变得越发可怕，因为如果有人设法黑入零知识证明系统，他们可以提取所有的钱，而我们完全不知道出了什么问题（更糟糕的是，甚至不知道何时出了问题）。
当我们拥有强大的AI模型，比如再迭代两年后的Claude Mythos，可以自动化地发现这些 bug 时，代码中的 bug 就更加更加可怕了。
有些人对这种现实的反应是主张放弃智能合约的基本理念，甚至认为网络领域根本无法成为防御者能够对攻击者拥有不对称优势的领域。
一些引言：
以及：
更糟糕的是，一些人认为唯一的解决方案是放弃开源。
对网络安全而言，这将是一个黯淡的未来。尤其是对于我们这些关心互联网去中心化和自由的人来说，这是极其悲观的前景。
整个密码朋克精神从根本上建立在这样一个理念上：在互联网上，防御者具有优势，建立一座数字"城堡"（无论是加密、签名还是证明）要比摧毁一座容易得多。
如果我们失去了这一点，那么互联网安全就只能来自规模经济，来自在全世界追捕潜在的攻击者，并且从更广泛的意义上说，只能在统治与毁灭之间做二选一。
我不同意，我对网络安全的未来有着更加乐观的愿景。
我认为强大的 AI 漏洞寻找能力带来的挑战是严峻的，但它是一个过渡性的挑战。一旦尘埃落定，我们进入新的平衡点，我们将获得比过去更加有利于防御者的环境。
Mozilla 同意我的观点。引用他们的话：
现在，如果你在 Mozilla 的帖子中使用 Ctrl+F 搜索"形式化"和"验证"这两个词，你将会发现零个匹配项。网络安全的积极未来并不完全依赖于形式化验证，或者任何其他单一技术。
它取决于什么？基本上是这张图表：
CVE漏洞数量随时间的下降趋势
几十年来，许多技术促成了漏洞数量的下降：
在人工智能辅助下的形式化验证不应该被视为一种全新的范式，而应该被看作是已经在向前发展的趋势和范式的强大加速器。
形式化验证不是万能的。但它特别适合目标比实现简单得多的情况。这在我们将需要在以太坊的下一个主要迭代中部署的一些极其复杂的棘手技术中尤为真实：抗量子签名、STARKs、共识算法以及 ZK-EVMs。
STARK 是一款非常复杂的软件。但它实现的核心安全属性很容易理解和形式化：如果你看到一个指向程序 P 的哈希 H、输入 x 和输出 y 的证明，那么要么 (i) STARK 中使用的哈希算法被攻破了，要么 (ii) P(x) = y。
因此我们有了 Arklib 项目，它正试图创建一个完全经过形式化验证的 STARK 实现（参见 VCV-io，它提供了基础的预言机计算基础设施，可用于形式化验证各种其他加密协议，其中许多是 STARK 的依赖项）。
更具野心的是 evm-asm：一个构建完全经过形式化验证的整个 EVM 实现的项目。
这里的安全属性就没那么简单明了了：基本上，目标是证明其等效于用 Lean 编写的另一个 EVM 实现，不过那个实现可以为了最大化直观性和可读性而编写，完全不用考虑具体的运行效率。
有可能我们会得到十个 EVM 实现，都可证明地互为等价，且它们碰巧都包含同一个致命缺陷，能让攻击者抽干他们没有权限动用的地址里的所有 ETH。
但这比现今某个 EVM 实现存在这类缺陷的可能性要小得多。而另一个我们在经历了痛苦教训后才明白其重要性的安全属性，即抗DoS攻击能力，就很容易规范。
另外两个重要领域是：
在所有这些情况中，形式化验证带来的巨大附加值之一在于这些证明真正是端到端的。通常，最讨厌的 bug 都是交互 bug，它们潜伏在两个被独立考虑的子系统的交界处。
对于人类来说，端到端地推理整个系统太困难了。但自动化的规则检查系统能够做到。
让我们再看看 evm-asm。这是一个 EVM 实现。但它是直接用 RISC-V 汇编编写的 EVM 实现。
货真价实地。
这是 ADD 操作码：
之所以选择 RISC-V，是因为正在构建的 ZK-EVM 证明器通常通过证明 RISC-V 并将以太坊客户端编译为 RISC-V 来运作。因此，如果你有一个直接用 RISC-V 编写的 EVM 实现，这应该是你能得到的最快实现。
RISC-V 也可以在普通计算机内非常高效地被模拟（且市面上也有 RISC-V 笔记本电脑）。
当然，为了真正实现端到端，你必须形式化验证 RISC-V 的实现（或证明器的算术化）本身，但别担心，这方面的工作也已经存在了。
直接用汇编编写代码是我们在五十年前常做的事情。从那时起，我们已经放弃了这种做法，转而使用高级语言编写代码。
高级语言在效率上有所妥协，但作为交换，它们编写代码的速度快得多，更重要的是，理解他人代码的速度也快得多，这对于安全来说是必不可少的。
借助形式化验证和人工智能的结合，我们有机会"回到未来"。
具体来说，我们可以让人工智能编写汇编代码，然后编写一个形式化证明来验证该汇编代码具有所需属性。
至少，所需属性可以仅仅是与那些为提高可读性而优化、且用某种人类友好的高级语言编写的实现完美等价。
我们不再需要单一的代码对象在可读性和效率之间进行平衡，而是拥有两个独立的对象：一个（汇编实现）仅优化效率，同时考虑到其执行的特定环境的需求；另一个（安全声明，或高级语言实现）仅优化可读性，然后我们通过数学证明来证明两者之间的等价性。
用户可以（自动地）验证一次该证明，从那时起，他们只需运行快速版本。
这种方法非常强大，Yoichi Hirai 称之为"软件开发的终极形态"是有原因的。
在密码学和计算机科学领域，有一个传统几乎与形式化方法本身的历史一样悠久：那就是批评形式化方法（或更广泛地批评对"证明"的依赖）的传统。
这些文献充满了实际案例。让我们从早期简单密码学时代手写的证明说起，此处引用了 Menezes 和 Koblitz 在 2004 年的批评：
Menezes 和 Koblitz 接着给出了更多例子。常见的规律是：围绕着使加密协议更加"可证明"而进行的设计，往往会使它们变得更不"自然"，这使得它们更有可能在设计者甚至没有考虑过的情况下发生崩溃。
现在，让我们回到机器可验证的证明和代码。这是一篇 2011 年发现经过形式化验证的 C 编译器中存在漏洞的 论文 ：
还有一篇 2022 年的 论文 ：
而今天，在 2026 年，以下是 Nadim Kobeissi 描述 Cryspen 中经过形式化验证的软件的漏洞：
以及：
以上四个问题都属于以下两种类型之一：
Nadim 的文章包含了对形式化验证失败模式的分类；他也给出了其他类型的失败模式（比如，另一个主要的情况是"形式化规范本身就是错的，或者证明中包含了被构建系统默默接受的虚假声明"）。
最后，我们可以看看软件和硬件边界上的形式化验证失败。这里的一个常见问题是验证抗侧信道攻击的能力。
即使你有完美安全的加密形式来保护你的消息，如果几米外的人能够捕捉到电信号波动并在几十万次加密后提取出你的私钥，你仍然是不安全的。
这是一篇关于"差分功率分析"的 文章 ，这是一个目前已经被充分理解的此类技术例子。
差分功率分析是侧信道攻击的一种常见类型。来源：维基百科
一直有人试图证明能抵御此类攻击者的安全性。然而，任何这样的证明都需要某种攻击者的数学模型，让你能够针对其证明安全性。
有时会使用"d 探测模型"：我们假设攻击者在电路中可以查询的位置数量有一个已知的限制。但是，有些泄漏形式是这种模型无法捕捉的。
正如这篇文章中所观察到的，一个常见问题是过渡性泄漏：如果你能观察到一个不仅取决于某个位置的值，还取决于该值变化的信号，那么这通常足以让你从两个值（新旧值）而不是仅仅一个值中恢复你所需的信息。
这篇文章给出了其他形式泄漏的分类。
几十年来，对形式化验证的这些批评帮助形式化验证变得更好。相比过去，我们现在更善于提防此类问题。但即使在今天，它也不完美。
纵观全局，这里有一条主线索。形式化验证很强大。
但无论营销术语如何让形式化验证听起来像是给了你"可证明的正确性"，所谓的"可证明的正确性"从根本上并不能证明软件（或硬件）是"正确的"。
按照大多数人类的理解，"正确"的意思类似于："事物的行为符合用户对开发者意图的理解"。
而"安全"的意思类似于："事物的行为没有违背用户的期望，做出对用户利益不利的事情"。
在这两种情况下，正确性和安全性都归结为数学对象与人类意图或期望之间的比较。
人类的意图和期望在技术上也是数学对象，毕竟人类的大脑也是宇宙的一部分，它遵循着如果你有足够的算力就可以模拟的物理定律。
但它们是令人难以置信的复杂数学对象，计算机和我们自己都无法理解甚至无法读取。
就所有实际意图和目的而言，它们都是黑匣子；我们之所以对自己的意图和期望有任何了解，仅仅是因为我们每个人都有多年观察自己想法和推断他人想法的经验。
并且由于我们无法将原始的人类意图塞进计算机，形式化验证就无法证明与人类意图的比较。
因此，"可证明的正确性"和"可证明的安全性"实际上并没有证明我们人类所理解的"正确性"和"安全性"。除非我们能完全模拟人类大脑，否则任何东西都做不到。
我倾向于将测试套件、类型系统和形式化验证都看作是对编程语言安全性同一底层方法的不同实现方式（这可能也是唯一合理的方法）。
它们都是关于用不同方式冗余地规范我们的意图，然后自动检查这些不同规范之间是否相互兼容。
以这段 Python 代码为例：
在这里，你用三种不同的方式表达你的意图：
运行文件会将公式与示例进行核对。类型检查器可以验证类型是否兼容：将两个整数相加是合规操作，并会产生另一个整数。
类型系统往往是在物理学中检查作业的好方法：如果你在计算加速度，却得出了一个单位是米/秒而不是米/秒²的答案，你就知道你做错了。
而测试用例就是"样例包"定义的一个实例，对于人类来说，处理概念时这种方式往往比直接显式的定义自然得多。
你能用越多不同的方式来规范你的意图，理想情况下是那些要求你以不同思维方式来解决问题的截然不同的方式，一旦所有这些表达形式都被证明是相互兼容的，你就越有可能实际上表达出了你真正想要的东西。
安全编程在于用多种不同的方式表达你的意图，然后自动验证这些表达式是否全都相互兼容。
形式化验证使你能将这种方法进一步延伸。通过形式化验证，你可以用几乎无限数量的不同冗余方式来规范你的意图，程序只有在它们全部兼容时才能验证通过。
你可以规范一个高度优化的实现以及一个效率极低但易于人类阅读的实现，并验证它们是否匹配。你可以请你的十个朋友提供他们认为你的程序应具备的数学属性列表，然后检查它是否全部通过。
如果没通过，找出到底是程序错了还是数学属性定错了。而且，你可以使用人工智能极度高效地完成所有这些操作。
现实一点讲，你不会自己编写证明的。形式化方法一直没有流行起来的原因，就是大多数人无法弄明白怎么写这些晦涩的内容。你能告诉我下面这段代码的意思吗？
（如果你想知道，这是针对一种 SPHINCS 签名变体的一项特定安全声明的证明中的许多子引理之一。
具体来说，该声明是：除非发生哈希碰撞，否则某条消息的签名将至少在一条哈希阶梯上的某处需要比任何其他消息的签名更高的值，因此它包含了无法从那另一个签名中计算出来的信息）
无需手动编写代码和证明，你只需让人工智能为你编写程序（无论是直接用 Lean 写，还是为了速度用汇编语言写），并在过程中证明任何期望的属性即可。
这项任务有个好处是它本身就是自我验证的，因此你不需要去监督，你只要让人工智能自己连续运行好几个小时就行。
最糟糕的结果也就是它在原地打转而毫无进展（或者，就像我的 leanstral 曾做过的那样，它为了减轻自己的工作负担，擅自替换掉了被要求证明的声明）。
你在最后唯一需要检查的，就是它证明的声明是否符合你的要求。
在 SPHINCS 签名变体中，这是最终声明：
这实际上处于勉强能读懂的边缘：
如果从一个哈希摘要（dig1）生成的数字不等于从另一个哈希摘要（dig2）生成的数字
那么以下两种情况都不成立：
在通过添加校验和生成的"扩展数字"（wotsFullDigits）中也是如此。也就是说，在 dig1 的扩展中，不可避免地有些地方的数字会更高，而在另一些地方，dig2 的扩展中的数字会更高。
在使用大型语言模型编写证明方面，我发现 Claude 和 Deepseek 4 Pro 都能胜任。Leanstral 是一款经过专门微调以编写 Lean 的较小开源权重模型，它是一个很有前景的替代方案。
它拥有 119B 的参数量，每个 token 激活 6B，你可以在本地运行它，尽管速度较慢（在我的笔记本电脑上速度约为 15 tok/sec）。根据基准测试，Leanstral 优于大得多的通用模型：
根据我目前的个人经验，它比 Deepseek 4 Pro 稍差一些，但仍然很有效。
形式化验证无法解决我们所有的问题。
但是，如果我们希望互联网安全的模型不再建立在人人都信任少数几个强大组织的基础上，我们就有必要转而去信任代码，这包括在面对强大的人工智能对手时也能信任代码。
AI 辅助下的形式化验证让我们在实现这一目标的道路上迈出了坚实的大步。
就像区块链和 ZK-SNARKs 一样，人工智能和形式化验证也是非常互补的技术。
区块链以隐私和可扩展性为代价赋予你开放的可验证性和抗审查性，而 ZK-SNARKs 又把隐私和可扩展性还给了你（实际上甚至比你之前的还要多）。
人工智能以准确性为代价赋予了你编写大量代码的能力，而形式化验证又把准确性还给了你（实际上甚至比你之前的还要高）。
在默认情况下，人工智能将催生大量极为草率的代码，bug 的数量将会增加。
事实上，在某些情况下，容忍 bug 的增加才是正确的权衡：如果 bug 是轻微的，那么即使是存在 bug 的软件，也比没有该软件要好。
但在这里，网络安全有着乐观的未来：软件将（继续）分裂成围绕"安全核心"的"不安全边缘部分"。
不安全的边缘部分将在沙箱中运行，只被赋予完成工作所需的最低权限。
安全核心将管理一切。如果安全核心崩溃，一切都会崩溃，包括你的个人数据、你的金钱等等。但是如果某个不安全的边缘部分崩溃了，安全核心依然能保护你。
当涉及到安全核心时，我们不能让存在 bug 的代码泛滥。我们会采取激进的行动来保持安全核心规模的小巧，甚至进一步缩小它。
相反，我们将人工智能带来的所有额外性能完全投入到使安全核心更安全的任务中，从而使其能够承受我们在高度数字化的社会中赋予它的极高的信任重任。
操作系统的内核（或者至少是其中一部分）将成为这样的一个安全核心。
以太坊将是另一个。
希望至少对于所有非性能密集型的计算，你所使用的硬件会成为第三个。
与物联网相关的系统将是第四个。
至少在这些安全核心之中，那句古老的格言"bug 是不可避免的，你只能在攻击者之前尽力去找到它们"将被证伪，取而代之的是一个更加充满希望的世界，在那里你将获得真正的安全。
但如果你心甘情愿将你的资产和数据交给那些编写拙劣、可能意外将它们吞噬进黑洞的软件，好吧，你当然也拥有那个自由。
