【翻译】V神博客-浅探形式化验证

作者：Vitalik Buterin
原文：https://vitalik.eth.limo/general/2026/05/18/fv.html
发表时间：2026-05-18
译者：AI 辅助翻译，加有译者注解

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

---

过去几个月，一种新的编程范式正在以太坊前沿研究和开发圈子，以及计算机领域的诸多角落中迅速崛起：直接用极低层级的语言（如 EVM 字节码、汇编语言）或 Lean 编写代码，并用 Lean 书写可自动检验的数学证明来验证其正确性。

若做到位，这既有望产出极高效的代码，安全性也将远超以往的编程方式。Yoichi Hirai 称之为”软件开发的终极形态”。本文将尝试揭开这一切的神秘面纱——形式化验证究竟是什么，软件的形式化验证能做到什么，以及它在以太坊乃至更广泛领域内的局限与弱点。

[译注] Lean 是一种交互式定理证明辅助语言，最初由微软研究院开发，现由 Lean 社区维护。它既是一门函数式编程语言，也是一个数学证明系统，越来越多地被用于编写可机器检验的数学证明。

---

什么是形式化验证？

形式化验证，是指以可自动检验的方式书写数学定理的证明。举一个不算太简单、但还算直观的例子：斐波那契数列中，每第三个数是偶数，其余为奇数。

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

一种简单的证明方式是数学归纳法，每次往前走三步。

基础情形：令 F₁ = F₂ = 1，F₃ = 2。通过直接检查，命题（”3 的倍数处的 Fᵢ 为偶数，其余为奇数”）在 x = 3 时成立。

归纳步骤：假设命题对 3k+3 以内均成立，即已知 F₃ₖ₊₁、F₃ₖ₊₂、F₃ₖ₊₃ 分别为奇、奇、偶。可以计算下一组三个数的奇偶性：

F₃ₖ₊₄ = F₃ₖ₊₂ + F₃ₖ₊₃ = 奇 + 偶 = 奇
F₃ₖ₊₅ = F₃ₖ₊₃ + F₃ₖ₊₄ = 偶 + 奇 = 奇
F₃ₖ₊₆ = F₃ₖ₊₄ + F₃ₖ₊₅ = 奇 + 奇 = 偶

这样，我们从”命题对 3k+3 以内成立”推出了”命题对 3k+6 以内成立”。反复应用此推导，便可确信规律对所有整数都成立。

这个论证对人类来说颇具说服力。但如果你要证明复杂一百倍的东西，并且想非常非常确信自己没有犯错呢？那你可以构造一个能说服计算机的证明。

下面是它的样子：

-- 斐波那契数列，fib 0 = 0, fib 1 = 1, fib 2 = 1（索引偏移 1）
def fib : Nat → Nat
  | 0     => 0
  | 1     => 1
  | n + 2 => fib (n + 1) + fib n

-- 命题：fib (3k+1) 为奇，fib (3k+2) 为奇，fib (3k+3) 为偶。
-- 等价地：从 fib 3 开始，每第三个斐波那契数为偶数。
-- 我们对 k 进行归纳，同时证明三个部分，
-- 因为下一块的每个情况都由上一块构建。

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 =>
    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 语句组成的”确定性”程序，而非 LLM）的直觉与人类的直觉截然不同。在上面的证明中，你不需要强调 fib(3k+4) = fib(3k+3) + fib(3k+2) 这个事实，而是强调 fib(3k+3) + fib(3k+2) 为奇数，然后 Lean 那个名字有些夸张的 omega 策略会自动将此与它对 fib(3k+4) 定义的认知结合起来。

[译注] omega 是 Lean 中一种自动化证明策略，能处理线性整数算术（Linear Integer Arithmetic）的问题。它的名字来源于”omega 测试”算法。类似地，ring 策略能自动证明环论中的等式。Prod.mk.inj 是一个关于有序对（product type）的引理名，意为”如果两个有序对相等，则它们的分量分别相等”。

在更复杂的证明中，你有时需要在每个步骤显式指定是哪条数学定律允许你做这一步，有时会遇到 Prod.mk.inj 这样晦涩的名字。但另一方面，你可以一步展开巨大的多项式表达式，只需写一行 “omega” 或 “ring” 便可证明它。

这里的反直觉性和繁琐性，是尽管机器可验证证明已存在近 60 年，这一领域却仍属小众的重要原因之一。但另一方面，随着 AI 的快速进步，很多以前不可能的事情正在迅速变为可能。

---

验证计算机程序

到目前为止，你可能在想：好吧，计算机可以验证关于数学定理的证明，这样我们终于能确认那些关于素数或别的什么的疯狂新结论哪些是真的，哪些只是百页 PDF 论文里的错误。也许我们甚至能搞清楚望月新一关于 ABC 猜想的证明是否正确！但除了满足好奇心，这又怎样？

[译注] ABC 猜想（abc conjecture）是数论中的一个重要未解猜想，由 Oesterlé 和 Masser 于 1985 年提出。日本数学家望月新一（Shinichi Mochizuki）于 2012 年声称给出了证明，但其证明方法（宇宙际 Teichmüller 理论，IUT）极其晦涩，数学界至今未能形成定论。

这个问题有很多可能的答案。但其中一个对我而言最为重要的答案是：验证计算机程序的正确性，尤其是涉及密码学或安全的程序。毕竟，计算机程序是一个数学对象，因此证明一个程序以某种方式运行，就是在证明一个数学定理。

举例来说，假设你想证明像 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 的密钥交换消息，他无法以超过可忽略的概率将得到的会话密钥与随机密钥区分开来。

[译注] DDH（Decisional Diffie-Hellman，判定性 Diffie-Hellman）假设是密码学中的基础假设之一，其大意是在循环群中，给定 g、gᵃ、gᵇ，难以区分 gᵃᵇ 与随机群元素。X3DH 是 Signal 协议使用的扩展三重 Diffie-Hellman 密钥协商协议，用于在双方没有实时在线时建立加密通信。”随机预言模型”（Random Oracle Model）是密码学证明中常用的理想化假设，将哈希函数视为一个完全随机的函数。如果对端到端加密感兴趣的可以看看我的这篇博客：https://bdwms.site/e2ee/

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

类似的验证项目也存在，用于证明 TLS 和其他浏览器端密码学的安全实现。

如果你端到端地进行形式化验证，你证明的就不仅仅是某个协议描述在理论上是安全的，而是用户实际运行的那段具体代码在实践中是安全的。从用户角度看，这极大地改善了”无信任性”：为了完全信任代码，你不需要检查所有代码，你只需检查关于它所证明的命题。

当然，这里有几个重要的星号需要牢记，特别是关于”安全”这个最重要的词究竟意味着什么。忘记证明真正重要的命题很容易发生。找不到比代码本身更简单的方式来描述需要证明的命题也很常见。往证明中悄悄塞入实际上并不成立的假设也很容易做到。决定系统的某一部分才真的需要形式化证明，然后仍被另一部分（甚至硬件）中的严重缺陷所击中，这种事也不少见。即使是 Lean 的实现本身也可能有 bug。但在讨论所有这些恼人的细节之前，让我们先深入探索形式化验证在理想情况下正确执行所能带来的那种”乌托邦”。

---

形式化验证与安全

代码里的 bug 很可怕。

当你把加密货币放进不可篡改的链上智能合约，而代码里存在 bug 时，朝鲜就能自动把你的钱全部抽走、且毫无追索可能——bug 就更可怕了。

当这一切又被包裹进零知识证明系统，一旦有人攻破了零知识证明系统，他们就能抽走所有资金，而我们完全不知道出了什么问题——甚至不知道何时出了问题——那就更更可怕了。

当我们拥有了像 Claude Mythos（再经过两年的进化）那样能自动发现漏洞的强大 AI 模型时，代码里的 bug 就变得更更更可怕了。

[译注] Vitalik 此处提到”Claude Mythos”是一个假设性的未来 AI 模型名称，用来指代 2028 年前后可能出现的、能自动大规模发现零日漏洞的 AI 系统。这是一种对 AI 安全威胁的具体化比喻，而非实际存在的产品。原文链接的新闻标题为”AI 在 FreeBSD 中发现数千个零日漏洞”，说明这种威胁已初现端倪。

面对这一现实，一些人的回应是主张放弃智能合约的根本理念，甚至认为网络空间根本不可能成为一个防御方具有非对称优势的领域。

一些引言如下：

要加固一个系统，你需要花费比攻击者利用漏洞更多的算力来发现漏洞。

以及：

我们的职业建立在确定性代码的基础上——写好、测试、发布、知道它能运行。但在我的经验中，这份契约正在瓦解。在真正 AI 原生公司的顶尖运营者中，代码库已经开始变成一种你”相信”它能运行的东西，而这个概率你已经无法精确描述了。

更有甚者，一些人认为唯一的解决方案是放弃开源。

这对网络安全来说将是一个黯淡的未来。对于我们这些关心互联网去中心化与自由的人来说，这尤其是一个极其黯淡的未来。整个密码朋克精神的根基，正是互联网上防御者具有优势这一信念：构建一座数字”城堡”（无论是加密、签名还是证明）远比摧毁它容易得多。一旦失去这一点，互联网安全就只能依赖规模经济，依赖在全球追捕可能的攻击者，归根结底是在”统治”与”毁灭”之间做二选一。

[译注] “密码朋克”（cypherpunk）是 20 世纪 80-90 年代兴起的一种思想运动，倡导通过密码技术和隐私保护来推动社会变革，强调个人自由和去中心化。以太坊和比特币等加密货币项目在精神上都与这一传统紧密相连。

我不同意这种悲观看法，我对网络安全的未来持有更乐观的愿景。

我认为强大 AI 漏洞挖掘带来的挑战是严峻的，但它是一个过渡性的挑战。一旦尘埃落定、进入新的均衡，我们将到达一个比以前更有利于防御的位置。

Mozilla 与我的看法一致。引用他们的话：

你可能需要把其他一切重新排列优先级，将毫不动摇的专注全部投入这项任务，但隧道尽头是有光的。我们为团队应对这一挑战的方式感到无比自豪，其他人也将如此。我们的工作还未完成，但我们已经转过了那个弯，可以瞥见一个远比”仅仅跟上”更美好的未来。防御者终于有机会决定性地胜出。

……

缺陷是有限的，我们正在进入一个终于可以把它们全部找出来的世界。

值得一提的是，如果你在 Mozilla 的帖子里搜索”formal”和”verification”两个词，你会发现一个也找不到。网络安全的积极未来并不严格依赖于形式化验证，也不依赖于任何单一技术。

那它依赖于什么？基本上，就是这张图：

这些年来，已有多种技术对漏洞数量的下降做出了贡献：

• 类型系统
• 内存安全语言
• 软件架构的改进（包括沙箱化、权限控制，以及更一般意义上的明确区分”可信计算基”与”其他代码”）
• 更好的测试方法论
• 关于安全与不安全编码模式的知识积累
• 预先编写和经过审计的软件库的积累

[译注] “可信计算基”（Trusted Computing Base，TCB）是指系统中需要被信任的最小软硬件集合。TCB 越小，需要审计和保护的范围就越小，安全性也就越高。这一概念是现代安全架构设计的核心思想之一。内存安全语言的代表有 Rust、Go 等，相比 C/C++ 能消除大量缓冲区溢出等漏洞。

在 AI 的辅助下，形式化验证不应被视为一个全新的范式，而应被视为一个已经在向前推进的趋势与范式的强力加速剂。

形式化验证不是灵丹妙药。但它特别适合于目标远比实现简单的场景。在以太坊下一个重大迭代中需要部署的一些最棘手的技术里，这一点尤为突出：抗量子签名、STARK、共识算法和 ZK-EVM。

[译注] STARK（Scalable Transparent ARgument of Knowledge）是一种零知识证明技术，无需可信设置，具有后量子安全性。ZK-EVM 是使用零知识证明来验证以太坊虚拟机执行的系统，是以太坊 L2 扩容方案的核心技术。抗量子签名（如 SPHINCS+）旨在抵御量子计算机的攻击。

STARK 是一个极其复杂的软件。但它所实现的核心安全属性简单易懂、便于形式化描述：如果你看到一个证明，它指向程序 P、输入 x 和输出 y 的哈希 H，那么要么（i）STARK 中使用的哈希算法被破解了，要么（ii）P(x) = y。因此我们有了 Arklib 项目，致力于创建 STARK 的完全形式化验证实现（另见 VCV-io，它提供了基础性的预言机计算基础设施，可用于形式化验证各种密码学协议，其中许多是 STARK 的依赖项）。

[译注·展开解释] 这段话的核心逻辑是：STARK 的内部实现很复杂，但它对外承诺的事情很简单，因此很适合用形式化验证来检验这个承诺。

用大白话说，STARK 是一种”计算验证器”：你拿着一段程序 P、一个输入 x 和一个声称的输出 y，STARK 能生成一张”证明书”，让别人不重新跑一遍程序就能相信”P 在输入 x 下确实输出了 y”。这张证明书里含有一个哈希值 H，把程序、输入、输出都”锁住”了。

那它的安全性保证是什么？非常简洁：要么哈希函数本身被破解了（极不可能），要么这张证明书就是真的——P(x) 确实等于 y。没有第三种可能。这个保证就是 STARK 的”核心安全属性”，用数学语言写下来很短，远比 STARK 的内部实现简单得多。

这正是形式化验证的用武之地：**我们只需要证明”这段代码真的满足上述那个简洁的保证”**，而不需要证明代码的每一行都”直觉上正确”。Arklib 和 VCV-io 就是在做这件事——用形式化证明来担保 STARK 实现的安全性边界。

更雄心勃勃的是 evm-asm：一个构建完全形式化验证的完整 EVM 实现的项目。在这里，安全属性并不那么清晰：基本目标是证明与另一个用 Lean 编写的 EVM 实现的等价性——而那个实现可以在完全不考虑具体效率的情况下，被编写得尽量直观易读。我们可能会有十个 EVM 实现，它们彼此都被证明等价，却全都有同样的致命缺陷，让攻击者能从他们没有权限的地址提走所有 ETH。但这比今天任何一个 EVM 实现存在这种缺陷的可能性要小得多。还有另一个安全属性——DoS 抗性——我们只有在经历了痛苦的教训后才认识到它的重要性，但它很容易形式化描述。

另外两个重要领域是：

• 拜占庭容错共识。在这里，形式化描述所有期望的安全属性同样困难，但考虑到 bug 出现的频率之高，值得一试——于是我们有了 Lean 共识的进行中的实现和证明工作。

[译注] 拜占庭容错（Byzantine Fault Tolerance，BFT）是指在分布式系统中，即使部分节点存在恶意行为或任意错误，整个系统仍能达成共识的能力。这一概念得名于”拜占庭将军问题”，是区块链共识机制设计的理论基础。

• 智能合约编程语言：参见 Vyper 的形式化验证和 Verity 项目。

[译注] Vyper 是以太坊的一种智能合约语言，设计目标是比 Solidity 更安全、更易于审计。

在所有这些情况下，证明真正端到端带来了巨大的附加价值。通常，最棘手的 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

[译注] 这段代码实现了以太坊 EVM 的 256 位整数加法。由于 RISC-V 寄存器是 64 位的，一个 256 位整数需要被拆成 4 段来处理，代码中称为 limb（直译”肢”，更准确的理解是”分段”或”分组”）。Limb 0 处理最低 64 位，Limb 1~`Limb 3` 依次处理更高位。

每一段加法的流程是：LD（加载操作数）→ ADD（相加）→ SLTU（检测是否进位，Set Less Than Unsigned）→ SD（存回结果）。比 Limb 0 多出来的步骤，是要把上一段产生的进位（carry）也加进来，并把新进位传给下一段——这就是多步 ADD + SLTU + OR 的由来。最后的 ADDI sp, sp, 32 是弹出栈顶两个操作数、压入一个结果后对栈指针的调整。

之所以选择 RISC-V，是因为正在构建的 ZK-EVM 证明器（prover）通常通过证明 RISC-V 来工作，并将以太坊客户端编译到 RISC-V。因此，如果你有一个直接用 RISC-V 编写的 EVM 实现，它应该是你能得到的最快实现。RISC-V 也可以在普通计算机内部非常高效地模拟运行（RISC-V 笔记本电脑已经存在）。当然，要真正做到端到端，你还必须形式化验证 RISC-V 实现（或证明器的算术化）本身，但别担心——这也已经存在了。

[译注] 这段话需要先理解”证明器”（prover）是什么。

回到前面说的 STARK：STARK 能生成一张”证明书”，证明某个计算被正确执行了。生成这张证明书的程序就叫”证明器”（prover）。验证这张证明书的程序叫”验证器”（verifier）。

ZK-EVM 的工作方式就是：用证明器给以太坊上发生的每一笔交易、每一个区块的执行过程生成一张证明书，这样其他节点只需验证证明书，而不必自己重新执行一遍所有计算——这是以太坊 L2 扩容的核心原理。

那证明器为什么要和 RISC-V 扯上关系？因为证明器要”描述”一段计算，必须把它翻译成一种固定的数学形式（算术电路）。如果每种语言都要单独翻译一次，工作量巨大。但如果统一先把代码编译成 RISC-V 指令，再让证明器只针对 RISC-V 做一次通用的翻译，就能证明任意程序——就像有了 JVM，任何语言编译成字节码就能运行一样。

所以，直接用 RISC-V 汇编实现 EVM，省去了”先编译到 RISC-V 再证明”的中间损耗，是理论上最快的路径。

五十年前，我们经常直接用汇编写代码。从那以后，我们逐渐转向用高级语言写代码。高级语言在效率上有所损失，但换来了更快的编码速度，以及——对于安全来说同样重要的——更快地理解他人代码的能力。

有了形式化验证与 AI 的结合，我们有机会”回到未来”。具体来说，我们让 AI 写汇编，然后写一个形式化证明来验证该汇编具有期望的属性。至少，期望的属性可以直接就是：与某个针对可读性优化的高级语言实现完全等价。

不再需要一个单一的代码对象在可读性与效率之间做权衡，而是有两个独立的对象：一个（汇编实现）只优化效率，充分考虑其执行环境的具体需求；另一个（安全声明，或高级语言实现）只优化可读性；然后有一个数学证明来证明这两者之间的等价性。用户可以（自动地）一次性验证这个证明，此后就只运行快速版本。

这很强大，这就是为什么 Yoichi Hirai 将其称为”软件开发的终极形态“。

---

形式化验证不是灵丹妙药

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

让我们从密码学更古老、更简单的年代里手写证明开始，Menezes 和 Koblitz 在 2004 年的批评如下：

1979 年，Rabin 提出了一种加密函数……在某种意义上是”可证明”安全的，即它具有归约安全属性。

归约安全声明：能从密文 y 中找到消息 m 的人，必然也能分解 n。

……

就在 Rabin 提出他的加密方案后不久，Rivest（见 [63]）指出，具有讽刺意味的是，赋予它额外一层安全性的那个特性，如果面对一种不同类型的攻击者——“选择密文攻击者”——就会导致完全崩溃。换言之，假设攻击者能设法让 Alice 解密一段由他自己选择的密文，他就可以按照 Sam 在前一段中使用的同样方法来分解 n。

[译注] Rabin 密码系统（1979）基于整数分解难题，具有”可证明安全”的特性——破解它等价于分解大整数。然而 Rivest 指出，在”选择密文攻击”（CCA）模型下，攻击者可以通过让解密预言机帮助自己，从而分解密钥。这个例子深刻说明了密码学证明的脆弱性：安全性高度依赖于威胁模型的准确性，忽略一类攻击者可能导致”可证明安全”的方案在实践中完全不安全。

Menezes 和 Koblitz 接着给出了更多例子。共同模式是：为了让密码学协议更”可证明”而进行的设计，往往使其变得不那么”自然”，从而更容易在设计者甚至没有考虑到的某些情形下崩溃。

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

我们发现的第二个 CompCert 问题，由生成如下代码的两个 bug 来说明：

stwu r1, -44432(r1)

这里正在分配一个大的 PowerPC 栈帧。问题是 16 位位移字段溢出了。CompCert 的 PPC 语义未能指定此立即值宽度的约束，其假设是汇编器会捕获超出范围的值。

以及 2022 年的一篇论文：

在 CompCert-KVX 中，commit e2618b31 修复了一个 bug——“nand”指令会被打印成”and”；”nand”仅在罕见的 ~(a & b) 模式下被选择。该 bug 是通过编译随机生成的程序发现的。

[译注] CompCert 是一个经过形式化验证的 C 编译器，用 Coq 证明助手编写。它的核心目标是保证编译器不会引入错误——即如果源代码正确，编译出的机器码也会正确。然而这些例子表明：即便是形式化验证过的编译器，其验证范围的边界（如与汇编器的接口、指令打印层）仍可能存在未被覆盖的 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 摘要。这是一类 Type I 失败：该内部函数被标记了，整个 NEON 后端没有完成运行时安全性或正确性的证明。

以及：

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

[译注] 这两个例子分别代表了形式化验证中的常见失效模式：第一个是”部分验证陷阱”——汇编内部函数被标记为”已验证”但实际上没有完成证明；第二个是”规范遗漏”——忘记对错误处理逻辑（.unwrap() 会在 None 时 panic）添加相应的安全属性证明。在 Rust 中，.unwrap() 是一种粗暴的错误处理方式，生产代码中不应对外部输入使用它。

上述四个问题都属于两种类型：

• 部分验证陷阱：只有部分代码被验证（因为验证其余部分太困难），而未被验证的代码比作者预想的更容易出现 bug（且以更关键的方式）
• 规范遗漏：作者忘记指定需要被证明的关键属性

Nadim 的文章包含了形式化验证失效模式的分类；他还给出了其他类型的失效模式（例如，另一个主要的失效模式是”形式规范本身是错误的，或者证明包含被构建系统静默接受的虚假声明”）。

最后，我们可以看看软件与硬件边界处的形式化验证失效。这里的一个常见问题是验证旁路攻击抗性。即使你有一种完美安全的加密来保护你的消息，如果几米外的人能捕捉到电气波动，并在几十万次加密后提取你的私钥，你依然不安全。这里有一篇关于”差分功率分析”的文章，这是此类技术中现在已被充分理解的一个例子。

差分功率分析是一种常见的旁路攻击。来源：维基百科

[译注] 旁路攻击（Side-Channel Attack）不攻击密码算法本身，而是利用实现过程中泄露的物理信息（功耗、时序、电磁辐射等）来恢复密钥。差分功率分析（Differential Power Analysis，DPA）通过统计分析大量功耗曲线与密钥假设之间的相关性来还原密钥。这类攻击曾被证实对 AES、RSA 等主流算法的硬件实现有效，是智能卡、IoT 设备安全的重大威胁。

已有人尝试证明对此类攻击者的安全性。然而，任何此类证明都需要某种关于攻击者的数学模型，用来证明安全性。有时使用”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

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

• 显式地：在代码中实现了斐波那契公式
• 间接地：通过类型系统（指定输入、输出和递归中间步骤都是整数）
• 通过”示例集合”的方式：测试用例

运行文件时，会对公式进行示例检查。类型检查器可以验证类型是否兼容：将两个整数相加是有效的操作，并产生另一个整数。类型系统在物理学中往往是检验工作的好方法：如果你在计算加速度，得到的答案单位是 $ \frac{m}{s} $ 而不是 $ \frac{m}{s^2} $，你就知道哪里出了问题。而”示例集合”式的”定义”（测试用例正是其一例）往往只是对人类来说处理概念更自然的方式，而非直接的显式定义。

[译注] 这里的类比非常精妙：量纲分析（dimensional analysis）正是物理学中最朴素的”类型系统”。如果一个公式的量纲不对，那必然有地方算错了，不需要知道具体数值就能发现错误。类型系统把这种思想推广到了编程语言：类型错误代表逻辑错误，编译器在运行前就能发现。

你用来描述意图的方式越多，理想情况下是需要你以不同思维方式来处理问题的非常不同的方式，如果所有这些表达都被证明彼此兼容，那么你实际上表达出了你想要的东西的可能性就越大。

安全编程是关于以多种不同方式表达你的意图，然后自动验证这些表达彼此兼容。

形式化验证让你能将这种方法延伸得更远。有了形式化验证，你可以用几乎任意数量的不同冗余方式来描述你的意图，程序只有在它们全部兼容时才会验证通过。 你可以指定一个优化实现和一个非常低效但人类可读的实现，并验证它们匹配。你可以请十个朋友提供你的程序应具备的数学属性列表，然后检查是否全部通过——如果没有，找出是程序错了还是数学属性错了。你还可以用 AI 极其高效地完成上述所有工作。

---

那么我如何开始？

现实来说，你不会自己写证明的。形式化方法至今未能大规模普及的全部原因，正是大多数人无法理解怎么写这些玩意儿。你能告诉我下面的代码是什么意思吗？

  /-- 辅助引理：在 foldl 层面，使用一个累加器进行逐点 ≤ 比较。 -/
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 签名变体的一个特定安全声明的证明中，众多子引理之一——即：除非存在哈希碰撞，一条消息的签名在至少一个哈希梯上需要比任何其他消息的签名更高的值，因此需要无法从其他签名中计算出的信息。）

[译注] SPHINCS（及其改进版 SPHINCS+）是一种基于哈希函数的数字签名方案，被 NIST 选为后量子密码学标准之一。它不依赖于格或椭圆曲线等数学结构，仅依赖于哈希函数的安全性，因此对量子计算机具有天然的抵抗力。”哈希梯”（hash ladder）是其构造中的核心概念：通过反复哈希一个值得到一条链，签名时”揭示”链上的某个位置，位置越高代表使用的是”更贵”的信息。

你不是手写代码和证明，而是让 AI 为你编写程序（直接用 Lean 写，或者如果你想要速度，就用汇编写），并在过程中证明任何期望的属性。

[译注·核心问题：AI 写的证明，怎么保证它是对的？]

这正是形式化验证最精妙的地方：你根本不需要信任 AI，因为证明的正确性由 Lean 本身来保证，而不是由 AI 保证。

具体流程是这样的：

1. AI（比如 Claude 或 Deepseek）输出一段 Lean 代码，声称证明了某个性质
2. Lean 的类型检查器——一个极其小巧、确定性的程序——逐行检验这段证明的每一步是否在逻辑上合法
3. 如果任何一步有问题，Lean 直接报错，AI 必须修改重来；只有 Lean 通过了，才算证明成立

为什么类型检查能验证数学证明？

这背后有一个深刻的数学原理，叫做 Curry-Howard 同构（命题即类型）：在 Lean 的类型系统里，”命题”和”类型”是同一件事，”证明”和”程序”也是同一件事。

举个直觉上的例子：

• 命题 A 且 B 对应类型”一个同时包含 A 的证明和 B 的证明的对”
• 命题 A 蕴含 B 对应类型”一个函数，输入 A 的证明，输出 B 的证明”
• 命题 对所有 x，P(x) 成立 对应类型”一个函数，输入任意 x，输出 P(x) 的证明”

所以，当你写 theorem fib_triple (k : Nat) : ... 时，你实际上是在声明一个函数的类型签名——这个函数接受一个自然数 k，返回一个”证明对象”。写证明的过程，就是在构造这个函数体。

类型检查器做的事情，和普通编译器检查 你传给函数的参数类型对不对 完全一样——只是这里检查的是逻辑推导步骤，而非数据类型。一旦类型检查通过，就意味着你的”函数”确实能在所有情况下返回”证明对象”，也就是命题在逻辑上成立。这个检查过程是纯机械的、不需要任何”理解”，因此可以被完全自动化，而且结果要么通过要么报错，没有模糊地带。

这就是”本质上自我验证”的含义：AI 可以乱写、可以绕弯路、可以生成一大堆无效的尝试，但最终能通过 Lean 类型检查的证明，在数学上就是正确的——这不依赖于对 AI 的信任，而是依赖对 Lean 这个极简核心（几万行代码，远比 AI 模型容易审计）的信任。

唯一需要人工检查的，是 Vitalik 在下文说的：**”最终你需要确认的是，所证明的命题是你真正想要的那件事”**——也就是说，AI 有时会偷懒，把一个难证的命题悄悄替换成一个容易证的弱化版本，然后宣称”证完了”。所以人的职责从”写证明”变成了”审核命题本身”。

这项任务有一个好处，它是本质上自我验证的，所以你不需要监督——你可以让 AI 自行运行数小时。可能发生的最糟糕的情况是它会在原地打转而毫无进展（或者，就像我的 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）生成的数字不相等，

那么以下两者均不成立：

• 对于所有数字，dig1 的数字 ≤ dig2 的数字
• 对于所有数字，dig2 的数字 ≤ dig1 的数字

在通过添加校验和（wotsFullDigits）生成的”扩展数字”中。也就是说，在 dig1 的扩展中，不可避免地某些地方的数字会更高，而在 dig2 的扩展中其他地方的数字会更高。

在用 LLM 写证明方面，我发现 Claude 足够用，Deepseek 4 Pro 也足够用。Leanstral 是一个有前景的替代品，它是一个专门针对编写 Lean 进行微调的较小的开放权重模型；以 119B 参数、每 token 激活 6B 参数，你可以在本地运行它，虽然速度较慢（我在我的笔记本电脑上可以获得大约 15 tok/sec）。根据基准测试，Leanstral 的表现优于体量大得多的通用模型：

[译注] Leanstral 是 Mistral AI 针对 Lean 4 定理证明任务专门微调的模型。这种”专项微调”的思路与 AlphaCode（代码生成）、AlphaFold（蛋白质折叠）的成功经验一脉相承：通用大模型在特定高难度任务上，往往不如规模更小但经过深度优化的专用模型。Vitalik 提到他在自己笔记本上运行 Leanstral，可参见他关于安全本地 LLM 的另一篇文章。

根据我目前的个人经验，它比 Deepseek 4 Pro 略差，但仍然有效。

---

形式化验证不会解决我们所有的问题。但如果我们想要一种不依赖于所有人都信任少数强大组织的互联网安全模型，我们就需要能够信任代码——包括在面对强大 AI 对手的情况下信任代码。AI 辅助的形式化验证让我们在这方面大踏步前进。

就像区块链和 ZK-SNARK，AI 与形式化验证是非常互补的技术。

区块链以隐私性和可扩展性为代价，给你开放的可验证性和抗审查性，而 ZK-SNARK 给你还回来……隐私性和可扩展性（实际上比以前拥有的更多）。

AI 以准确性为代价，给你大量编写代码的能力，而形式化验证给你还回来……准确性（实际上比以前拥有的更多）。

[译注] 这个类比十分精妙，揭示了一种”技术组合”的哲学：两种单独看有明显弱点的技术，组合起来后弱点相互弥补，优点相互增强。ZK-SNARK（零知识简洁非交互式知识论证）通过密码学手段，在不泄露具体数据的情况下证明某计算被正确执行，是以太坊 L2 扩容和隐私保护的核心技术。

默认情况下，AI 将催生大量非常粗糙的代码，bug 数量将会增加。确实，在某些情况下，让 bug 增加是正确的权衡：如果 bug 是轻微的，即便是有 bug 的软件也比没有那个软件要好。但网络安全有一个乐观的未来：**软件将（继续）分裂成一个”安全核心”周围的”不安全边缘碎片”**。

不安全的边缘碎片将在沙箱中运行，并被赋予完成工作所需的最低权限。安全核心将统管一切。如果安全核心崩溃，一切都会崩溃——你的个人数据、你的钱，以及更多。但如果某个不安全的边缘崩溃，安全核心会保护你。

对于安全核心，_我们不允许有 bug 的代码蔓延_。我们积极地将安全核心的规模保持在小范围内，甚至进一步缩小它。相反，我们把 AI 带来的全部额外算力投入到使安全核心更加安全上，使其能够在高度数字化的社会中承担我们对它施加的极高信任负担。

你操作系统的内核（至少是其中一部分）将是这样一个安全核心。以太坊将是另一个。希望你用于至少所有非性能密集型计算的硬件也将是第三个。涉及 IoT 的某些东西将是第四个。至少在这些安全核心中，”bug 不可避免，你只能努力在攻击者之前找到它们”这条旧格言将变成过去式，取而代之的是一个能获得真正安全的更希望之世界。但如果你想要把你的资产和数据交给编写糟糕的软件，而它可能会不小心把一切都发送进黑洞，那么，你也会有这份自由。

[译注] 文章结尾这段对未来安全架构的描述，与微内核（microkernel）设计哲学高度呼应——seL4 就是一个经过形式化验证的微内核，是目前已知最可靠的操作系统内核之一。”安全核心 + 不安全边缘”的分层架构思想，也是现代可信执行环境（TEE）如 Intel SGX、ARM TrustZone 的基本原理。Vitalik 对以太坊的定位与对操作系统内核的定位并列，意在强调：区块链不仅仅是金融工具，而是数字社会的基础设施信任层。

[译注] 最后总结下，我个人理解 V 神想要表述的是目前 AI 时代攻击者能够低成本快速挖掘漏洞，对于防守方来说可解的一个思路同样是 AI + 形式化验证。通过形式化验证降低软件漏洞风险，再通过 AI 加速形式化验证的开发，形式化验证的证明器（例如 lean 编译器本身）再去保证 AI 代码的目的约束，从而能够建设一个安全最小核心，类似 TEE/操作体统内核/以太坊等基础设施。这是一个从实际效果上来看切实有效的缓解手段和方向，译者理解大致如此。