Vitalik：以太坊下一阶段的关键是什么？

By: rootdata|2026/05/20 19:45:03

设为Google首选来源

Drake

作者：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 前成立。我们可以反复应用这个推论，从而确信该规则对所有整数都成立。

这个论点足以让人类信服。但是，如果你想证明复杂一百倍的东西，而且你想非常非常确定自己没有犯错呢？好吧，你可以给计算机提供一个它能信服的证明。

以下是它的具体呈现方式：

-- Fibonacci with fib 0 = 0, fib 1 = 1, fib 2 = 1 (indices offset by 1)
def fib : Nat → Nat
  | 0     => 0
  | 1     => 1
  | n + 2 => fib (n + 1) + fib n

-- Claim: fib (3k+1) is odd, fib (3k+2) is odd, fib (3k+3) is even.
-- Equivalently: every third Fibonacci number starting from fib 3 is even.
-- We prove all three at once by induction on k, since each case
-- of the next block is built from the previous block.
theorem fib_triple (k : Nat) :
    fib (3 * k + 1) % 2 = 1 ∧
    fib (3 * k + 2) % 2 = 1 ∧
    fib (3 * k + 3) % 2 = 0 := by
  induction k with
  | zero => decide
  | succ k ih =>
    -- Rewrite the new indices into the form (something) + 2 so fib unfolds.
    refine ⟨?_, ?_, ?_⟩
    · show (fib (3 * k + 3) + fib (3 * k + 2)) % 2 = 1
      omega
    · show (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)) % 2 = 1
      omega
    · show (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)
      + (fib (3 * k + 3) + fib (3 * k + 2))) % 2 = 0
      omega

这是同样的推理逻辑，但用 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 这样的加密通信软件是否真的安全。你可以写下在这种背景下"安全"在数学上的含义。

从高层次来看，你要证明的是，假设某些密码学假设成立，只有拥有私钥的人才能了解有关消息内容的任何信息。在现实中，有许多不同的安全属性都非常关键。

事实证明，真的有一个团队在试图弄清楚正是这个问题！他们的一个安全定理看起来是这样的：

theorem passive_secrecy_le_ddh
    (g : G)
    (adv : PassiveAdversary G SK) :
    passiveSecrecyAdvantage (F := F) g adv ≤
    ProbComp.boolDistAdvantage
      (DiffieHellman.ddhExpReal (F := F) g (ddhReduction adv))
      (DiffieHellman.ddhExpRand (F := F) g (ddhReduction adv))

以下是 Leanstral 对其含义的总结：

passive_secrecy_le_ddh 定理是一个紧凑归约，表明 X3DH 的被动消息保密性至少与随机预言模型下的 DDH 假设一样难。如果对手能够破解 X3DH 的被动消息保密性，那么他们也能破解 DDH。

由于我们假设 DDH 很难破解，因此 X3DH 对被动攻击也是安全的。该定理证明了，如果对手可以被动观察 Signal 的密钥交换消息，他们无法以优于可忽略的概率将其产生的会话密钥与随机密钥区分开来。

如果你将其与 AES 加密实现正确的证明结合起来，你就得到了 Signal 协议的加密对被动攻击者是安全的证明。

类似的项目也证明了 TLS 和浏览器内密码学其他部分的实现是安全的。

如果你进行端到端的完全形式化验证，你证明的就不只是协议的某种理论描述是安全的，而是用户运行的具体代码在实际中也是安全的。

从用户的角度来看，这极大地提升了免信任性：为了完全信任代码，你不需要检查整个代码库，你只需检查关于它被证明的那些声明。

现在，有一些重要的大前提需要牢记，尤其是关于"安全"这个至关重要的词到底意味着什么。

人们很容易忘记证明那些真正重要的声明。很容易发现，有时候要证明的声明并没有比代码本身更简单的描述方式。

很容易在证明中偷偷引入最终并不成立的假设。也很容易决定系统中只有一个部分真正需要被形式化证明，结果却被其他部分（甚至硬件）中的严重漏洞击中。

就连 Lean 实现本身也可能有 bug。但在我们讨论所有这些恼人的细节之前，让我们首先深入探讨一下，正确且理想地完成形式化验证可能带来的乌托邦。

为安全而生的形式化验证

计算机代码中的 bug 很可怕。

当你把加密货币放入不可变的链上智能合约，而朝鲜可以在代码出现 bug 时自动抽干你的所有资金且你无法申诉时，代码中的 bug 就变得更加可怕。

当这一切被包装在零知识证明中时，bug 就变得越发可怕，因为如果有人设法黑入零知识证明系统，他们可以提取所有的钱，而我们完全不知道出了什么问题（更糟糕的是，甚至不知道何时出了问题）。

当我们拥有强大的AI模型，比如再迭代两年后的Claude Mythos，可以自动化地发现这些 bug 时，代码中的 bug 就更加更加可怕了。

有些人对这种现实的反应是主张放弃智能合约的基本理念，甚至认为网络领域根本无法成为防御者能够对攻击者拥有不对称优势的领域。

一些引言：

要加固一个系统，你需要花费比攻击者用于利用漏洞更多的代币来发现这些漏洞。

以及：

我们这个行业是建立在确定性代码的基础上的。编写它、测试它、发布它、确信它能运行，但在我的经验中，这种契约正在破裂。

在真正AI原生公司的顶尖运营者中，代码库已经变成了你"相信"它能运行的东西，而你不再能精确说明它的成功概率。

更糟糕的是，一些人认为唯一的解决方案是放弃开源。

对网络安全而言，这将是一个黯淡的未来。尤其是对于我们这些关心互联网去中心化和自由的人来说，这是极其悲观的前景。

整个密码朋克精神从根本上建立在这样一个理念上：在互联网上，防御者具有优势，建立一座数字"城堡"（无论是加密、签名还是证明）要比摧毁一座容易得多。

如果我们失去了这一点，那么互联网安全就只能来自规模经济，来自在全世界追捕潜在的攻击者，并且从更广泛的意义上说，只能在统治与毁灭之间做二选一。

我不同意，我对网络安全的未来有着更加乐观的愿景。

我认为强大的 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 曾经如此普遍，还是值得一试的。因此我们在 Lean 中有进行中的共识协议的 Lean 实现及证明。
智能合约编程语言：参见 Vyper 和 Verity 中的形式化验证。

在所有这些情况中，形式化验证带来的巨大附加值之一在于这些证明真正是端到端的。通常，最讨厌的 bug 都是交互 bug，它们潜伏在两个被独立考虑的子系统的交界处。

对于人类来说，端到端地推理整个系统太困难了。但自动化的规则检查系统能够做到。

为效率而生的形式化验证

让我们再看看 evm-asm。这是一个 EVM 实现。但它是直接用 RISC-V 汇编编写的 EVM 实现。

货真价实地。

这是 ADD 操作码：

import EvmAsm.Rv64.Program
namespace EvmAsm.Evm64
open EvmAsm.Rv64

/-- 256-bit EVM ADD: binary, pops 2, pushes 1.
    Limb 0: LD, LD, ADD, SLTU (carry), SD (5 instructions).
    Limbs 1-3: LD, LD, ADD, SLTU (carry1), ADD (carryIn), SLTU (carry2), OR (carryOut), SD (8 each).
    Then ADDI sp, sp, 32.
    Registers: x12=sp, x7=acc, x6=operand, x5=carry, x11=carry1. -/
def evm_add : Program :=
  -- Limb 0 (5 instructions)
  LD .x7 .x12 0 ;; LD .x6 .x12 32 ;;
  ADD .x7 .x7 .x6 ;; SLTU .x5 .x7 .x6 ;; SD .x12 .x7 32 ;;
  
  -- Limb 1 (8 instructions)
  LD .x7 .x12 8 ;; LD .x6 .x12 40 ;;
  ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;
  ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;
  OR' .x5 .x11 .x6 ;; SD .x12 .x7 40 ;;
  
  -- Limb 2 (8 instructions)
  LD .x7 .x12 16 ;; LD .x6 .x12 48 ;;
  ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;
  ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;
  OR' .x5 .x11 .x6 ;; SD .x12 .x7 48 ;;
  
  -- Limb 3 (8 instructions)
  LD .x7 .x12 24 ;; LD .x6 .x12 56 ;;
  ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;
  ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;
  OR' .x5 .x11 .x6 ;; SD .x12 .x7 56 ;;
  
  -- sp adjustment
  ADDI .x12 .x12 32
end EvmAsm.Evm64

之所以选择 RISC-V，是因为正在构建的 ZK-EVM 证明器通常通过证明 RISC-V 并将以太坊客户端编译为 RISC-V 来运作。因此，如果你有一个直接用 RISC-V 编写的 EVM 实现，这应该是你能得到的最快实现。

RISC-V 也可以在普通计算机内非常高效地被模拟（且市面上也有 RISC-V 笔记本电脑）。

当然，为了真正实现端到端，你必须形式化验证 RISC-V 的实现（或证明器的算术化）本身，但别担心，这方面的工作也已经存在了。

直接用汇编编写代码是我们在五十年前常做的事情。从那时起，我们已经放弃了这种做法，转而使用高级语言编写代码。

高级语言在效率上有所妥协，但作为交换，它们编写代码的速度快得多，更重要的是，理解他人代码的速度也快得多，这对于安全来说是必不可少的。

借助形式化验证和人工智能的结合，我们有机会"回到未来"。

具体来说，我们可以让人工智能编写汇编代码，然后编写一个形式化证明来验证该汇编代码具有所需属性。

至少，所需属性可以仅仅是与那些为提高可读性而优化、且用某种人类友好的高级语言编写的实现完美等价。

我们不再需要单一的代码对象在可读性和效率之间进行平衡，而是拥有两个独立的对象：一个（汇编实现）仅优化效率，同时考虑到其执行的特定环境的需求；另一个（安全声明，或高级语言实现）仅优化可读性，然后我们通过数学证明来证明两者之间的等价性。

用户可以（自动地）验证一次该证明，从那时起，他们只需运行快速版本。

这种方法非常强大，Yoichi Hirai 称之为"软件开发的终极形态"是有原因的。

形式化验证不是灵丹妙药

在密码学和计算机科学领域，有一个传统几乎与形式化方法本身的历史一样悠久：那就是批评形式化方法（或更广泛地批评对"证明"的依赖）的传统。

这些文献充满了实际案例。让我们从早期简单密码学时代手写的证明说起，此处引用了 Menezes 和 Koblitz 在 2004 年的批评：

1979 年，Rabin 提出了一种加密函数，该函数在某种意义上是"可证明"安全的，也就是说，它具有一种归约主义的安全属性。

归约主义安全声明指出，能够从密文 y 中找出消息 m 的人，也必须能够分解 n。 ... 在 Rabin 提出其加密方案后不久，Rivest 指出，具有讽刺意味的是，正是赋予其额外安全性的这一特性，如果它面临另一种名为"选择密文"的攻击者时，会导致全线崩溃。

也就是说，假设攻击者可以以某种方式欺骗 Alice 解密其选择的密文，那么攻击者就可以遵循 Sam 在上一段中用来分解 n 的相同步骤。

Menezes 和 Koblitz 接着给出了更多例子。常见的规律是：围绕着使加密协议更加"可证明"而进行的设计，往往会使它们变得更不"自然"，这使得它们更有可能在设计者甚至没有考虑过的情况下发生崩溃。

现在，让我们回到机器可验证的证明和代码。这是一篇 2011 年发现经过形式化验证的 C 编译器中存在漏洞的论文：

我们发现的第二个 CompCert 问题体现在两个导致生成如下代码的 bug 中： stwu r1, -44432(r1) 此处正在分配一个大型的 PowerPC 堆栈帧。

问题在于 16 位的位移字段溢出了。CompCert 的 PPC 语义没有规定对此立即数宽度的限制，他们假设汇编器会捕获超出范围的值。

还有一篇 2022 年的论文：

在 CompCert-KVX 中，提交 e2618b31 修复了一个 bug："nand"指令会被打印为"and"；"nand"仅被用于极少见的 ~(a & b) 模式。该 bug 是通过编译随机生成的程序发现的。

而今天，在 2026 年，以下是 Nadim Kobeissi 描述 Cryspen 中经过形式化验证的软件的漏洞：

在 2025 年 11 月，Filippo Valsorda 独立报告了 libcrux-ml-dsa v0.0.3 在给定相同确定性输入的情况下，在不同平台上产生了不同的公钥和签名。

该 bug 存在于 _vxarq_u64 内部包裹函数中，该函数实现了 SHA-3 的 Keccak-f 置换中使用的 XAR 操作。后备机制向移位操作传递了不正确的参数，在没有硬件 SHA-3 支持的 ARM64 平台上损坏了 SHA-3 摘要。

这属于类型 I 故障：该内部函数被标记了，而整个 NEON 后端都没有完成对运行时安全性或正确性的证明。

以及：

libcrux-psq 库实现了一个后量子预共享密钥协议。在 decrypt_out 方法中，AES-GCM 128 解密路径对解密结果调用了 .unwrap() 而不是传播错误。一个格式错误的密文就能让进程崩溃。

以上四个问题都属于以下两种类型之一：

只验证了部分代码的情况（因为验证其余部分太难了），结果发现未验证的代码比作者想象的漏洞更多（且方式更致命）。
作者忘记规定需要证明的关键属性的情况。

Nadim 的文章包含了对形式化验证失败模式的分类；他也给出了其他类型的失败模式（比如，另一个主要的情况是"形式化规范本身就是错的，或者证明中包含了被构建系统默默接受的虚假声明"）。

最后，我们可以看看软件和硬件边界上的形式化验证失败。这里的一个常见问题是验证抗侧信道攻击的能力。

即使你有完美安全的加密形式来保护你的消息，如果几米外的人能够捕捉到电信号波动并在几十万次加密后提取出你的私钥，你仍然是不安全的。

这是一篇关于"差分功率分析"的文章，这是一个目前已经被充分理解的此类技术例子。

差分功率分析是侧信道攻击的一种常见类型。来源：维基百科

一直有人试图证明能抵御此类攻击者的安全性。然而，任何这样的证明都需要某种攻击者的数学模型，让你能够针对其证明安全性。

有时会使用"d 探测模型"：我们假设攻击者在电路中可以查询的位置数量有一个已知的限制。但是，有些泄漏形式是这种模型无法捕捉的。

正如这篇文章中所观察到的，一个常见问题是过渡性泄漏：如果你能观察到一个不仅取决于某个位置的值，还取决于该值变化的信号，那么这通常足以让你从两个值（新旧值）而不是仅仅一个值中恢复你所需的信息。

这篇文章给出了其他形式泄漏的分类。

几十年来，对形式化验证的这些批评帮助形式化验证变得更好。相比过去，我们现在更善于提防此类问题。但即使在今天，它也不完美。

纵观全局，这里有一条主线索。形式化验证很强大。

但无论营销术语如何让形式化验证听起来像是给了你"可证明的正确性"，所谓的"可证明的正确性"从根本上并不能证明软件（或硬件）是"正确的"。

按照大多数人类的理解，"正确"的意思类似于："事物的行为符合用户对开发者意图的理解"。

而"安全"的意思类似于："事物的行为没有违背用户的期望，做出对用户利益不利的事情"。

在这两种情况下，正确性和安全性都归结为数学对象与人类意图或期望之间的比较。

人类的意图和期望在技术上也是数学对象，毕竟人类的大脑也是宇宙的一部分，它遵循着如果你有足够的算力就可以模拟的物理定律。

但它们是令人难以置信的复杂数学对象，计算机和我们自己都无法理解甚至无法读取。

就所有实际意图和目的而言，它们都是黑匣子；我们之所以对自己的意图和期望有任何了解，仅仅是因为我们每个人都有多年观察自己想法和推断他人想法的经验。

并且由于我们无法将原始的人类意图塞进计算机，形式化验证就无法证明与人类意图的比较。

因此，"可证明的正确性"和"可证明的安全性"实际上并没有证明我们人类所理解的"正确性"和"安全性"。除非我们能完全模拟人类大脑，否则任何东西都做不到。

那它到底有什么用?

我倾向于将测试套件、类型系统和形式化验证都看作是对编程语言安全性同一底层方法的不同实现方式（这可能也是唯一合理的方法）。

它们都是关于用不同方式冗余地规范我们的意图，然后自动检查这些不同规范之间是否相互兼容。

以这段 Python 代码为例：

def fib(n: int) -> int:
    if n < 0:
        raise Exception("Negative values not supported")
    elif 0 <= n < 2:
        return n
    else:
        return fib(n-1) + fib(n-2)

if __name__ == '__main__':
    assert [fib(i) for i in range(10)] == [0, 1, 1, 2, 3, 5, 8, 13, 21, 34]
    assert fib(15) == 610

在这里，你用三种不同的方式表达你的意图：

显式地，通过在代码中实现斐波那契公式
隐式地，通过类型系统（指定输入、输出和递归中间步骤均为整数）
通过"样例包"方法：测试用例

运行文件会将公式与示例进行核对。类型检查器可以验证类型是否兼容：将两个整数相加是合规操作，并会产生另一个整数。

类型系统往往是在物理学中检查作业的好方法：如果你在计算加速度，却得出了一个单位是米/秒而不是米/秒²的答案，你就知道你做错了。

而测试用例就是"样例包"定义的一个实例，对于人类来说，处理概念时这种方式往往比直接显式的定义自然得多。

你能用越多不同的方式来规范你的意图，理想情况下是那些要求你以不同思维方式来解决问题的截然不同的方式，一旦所有这些表达形式都被证明是相互兼容的，你就越有可能实际上表达出了你真正想要的东西。

安全编程在于用多种不同的方式表达你的意图，然后自动验证这些表达式是否全都相互兼容。

形式化验证使你能将这种方法进一步延伸。通过形式化验证，你可以用几乎无限数量的不同冗余方式来规范你的意图，程序只有在它们全部兼容时才能验证通过。

你可以规范一个高度优化的实现以及一个效率极低但易于人类阅读的实现，并验证它们是否匹配。你可以请你的十个朋友提供他们认为你的程序应具备的数学属性列表，然后检查它是否全部通过。

如果没通过，找出到底是程序错了还是数学属性定错了。而且，你可以使用人工智能极度高效地完成所有这些操作。

那么我该如何开始？

现实一点讲，你不会自己编写证明的。形式化方法一直没有流行起来的原因，就是大多数人无法弄明白怎么写这些晦涩的内容。你能告诉我下面这段代码的意思吗？

  /-- Helper: pointwise ≤ at the foldl level with an accumulator. -/
private theorem foldl_acc_le (ds1 ds2 : List Nat) (w : Nat) (a b : Nat) (hAcc : a ≤ b)
    (hLE : Forall₂ (· ≤ ·) ds1 ds2) :
    List.foldl (λ acc d => acc * w + d) a ds1 ≤
    List.foldl (λ acc d => acc * w + d) b ds2 := by
  match ds1, ds2, hLE with
  | [], [], .nil => exact hAcc
  | d1::ds1', d2::ds2', .cons hd htl =>
    simp [List.foldl]
    refine foldl_acc_le ds1' ds2' w (a * w + d1) (b * w + d2) ?_ htl
    exact Nat.add_le_add (Nat.mul_le_mul hAcc (Nat.le_refl _)) hd

（如果你想知道，这是针对一种 SPHINCS 签名变体的一项特定安全声明的证明中的许多子引理之一。

具体来说，该声明是：除非发生哈希碰撞，否则某条消息的签名将至少在一条哈希阶梯上的某处需要比任何其他消息的签名更高的值，因此它包含了无法从那另一个签名中计算出来的信息）

无需手动编写代码和证明，你只需让人工智能为你编写程序（无论是直接用 Lean 写，还是为了速度用汇编语言写），并在过程中证明任何期望的属性即可。

这项任务有个好处是它本身就是自我验证的，因此你不需要去监督，你只要让人工智能自己连续运行好几个小时就行。

最糟糕的结果也就是它在原地打转而毫无进展（或者，就像我的 leanstral 曾做过的那样，它为了减轻自己的工作负担，擅自替换掉了被要求证明的声明）。

你在最后唯一需要检查的，就是它证明的声明是否符合你的要求。

在 SPHINCS 签名变体中，这是最终声明：

theorem wots_fullDigits_incomparable
    {dig1 dig2 : List Nat} {w l1 l2 : Nat}
    (hw : 0 < w)
    (hLen1 : dig1.length = l1) (hLen2 : dig2.length = l1)
    (hBound1 : ∀ d ∈ dig1, d < w) (hBound2 : ∀ d ∈ dig2, d < w)
    (hL2suff : l1 * (w - 1) < w ^ l2)
    (hNeq : dig1 ≠ dig2) :
    ¬ Forall₂ (· ≤ ·) (wotsFullDigits dig1 w l1 l2) (wotsFullDigits dig2 w l1 l2) ∧
    ¬ Forall₂ (· ≤ ·) (wotsFullDigits dig2 w l1 l2) (wotsFullDigits dig1 w l1 l2)

这实际上处于勉强能读懂的边缘：

如果从一个哈希摘要（dig1）生成的数字不等于从另一个哈希摘要（dig2）生成的数字

那么以下两种情况都不成立：