Loading...
系列： 形式化验证系列 · 第 1 部分，共 3 部分 读者对象： 完全的新手。无需具备数学、编程或密码学背景。 你将收获： 清晰理解“证明”软件正确意味着什么、它为何从根本上不同于测试、什么是机器检查的证明，以及这类证明能够承诺的确切（且诚实的）界限。
大多数软件之所以被信任，是因为它经过了测试：我们在许多输入上运行它，并观察其行为。形式化验证提出了一个更大胆的问题。我们能否以数学上的确定性证明，一个系统对每一种可能输入都会按预期运行，包括从未有人想过要尝试的输入？本文将从零开始构建这个概念。先讲直觉，等符号真正必要时再引入。
这是一个真实故事，也是这个系列存在的原因。
2022 年，注重隐私的加密货币 Zcash 推出了一个名为 Orchard 的新屏蔽资金池，让人们能够隐藏交易金额。四年来，它运行得毫无问题，并通过了多次专业审计。随后，在 2026 年 5 月，一名安全研究员仔细推理其底层数学（借助 AI 工具）后，发现了系统数学中的一个约束不足之处。这个漏洞可能让攻击者创造无限量的伪造货币，而且由于金额被隐藏，没有人会察觉。这个缺陷一直都存在。
它不是通过测试发现的。四年来，每一项测试都通过了。它是由某人对数学进行推理发现的。而团队修复它时，并未只是打补丁后继续前进。他们编写了一份机器检查的数学证明，涵盖超过 2,700 个独立定理，证明替代方案根本不可能包含这一类缺陷。
这就是形式化验证，它带给你的不是“我们试了很多情况，它们都能工作”，而是“我们证明了它对每一种情况都成立”。对于漏掉一个情况就会造成灾难的系统（货币、飞机、医疗设备、密码学），这种差异就是一切。
几十年前，计算机科学家 Edsger Dijkstra 为测试中的盲点命名，而这至今仍然正确：
测试可以显示 bug 的存在，但永远无法显示 bug 的不存在。
如果一项测试通过，你只知道系统在该输入下能够工作。对于你没有尝试的输入，你一无所知；而危险的 bug 几乎总在无人尝试的情况中。
想象一下，你负责一栋有一千扇门的建筑，你的工作是保证每扇门在夜间都锁上。
两者的区别在于抽样现实与证明设计的属性。测试进行抽样。形式化验证进行证明。这就是整个核心，其他一切都是严谨完成此事的工具。
每一种形式化验证，无论多么先进，恰好都由三种要素构成。清楚把握它们，其余都是细节。
| 支柱 | 通俗含义 | 建筑类比 |
|---|---|---|
| 规格说明 | “正确”意味着什么的精确陈述 | “每扇门都必须在夜间锁上” |
| 系统 | 实际被检查的对象（程序、电路或协议） | 建筑及其锁定机制 |
| 证明 | 系统始终满足规格说明的严谨论证 | 按下“锁定”会锁上所有门的逻辑论证 |
还有第四种较为隐性的要素，使整个过程值得信赖：
你可能会听到的证明助手包括 Lean、Rocq（原 Coq）和 Isabelle。实际上，它们是极其严格的逻辑检查引擎。开篇故事中的 Zcash 证明是用 Lean 编写的。值得注意的是，现代 AI 模型越来越多地被用于协助编写这些证明，由人类加以引导；这已将曾经需要数年的工作缩短至数周。机器仍会检查每一步，因此提速并不以牺牲任何确定性为代价。
“证明”这个词可能令人畏惧，因此让我们用一个具体、可检验的例子来揭开它的神秘面纱。没有密码学，只有学校算术。
断言： 对于每一个整数 n，和 0 + 1 + 2 + ... + n 等于 n(n+1)/2。
你可以测试它。n = 5 得到 0+1+2+3+4+5 = 15，以及 5 × 6 / 2 = 15。✓ 相符。试试 n = 10：其和为 55，而公式给出 10 × 11 / 2 = 55。✓ （这些结果均已计算并确认；实际上，直接检查时，该断言对从 0 到 999 的每一个 n 都成立。）
但测试数值，即使测试一千个，也永远无法达到“对每一个整数”。整数有无穷多个。证明通过一种称为归纳法的技术，以有限的论证弥合这道无限鸿沟：
n = 0，和就是 0，而公式给出 0 × 1 / 2 = 0。两者一致。✓k 成立。现在加上下一个数 k+1。到 k+1 为止的和为 (sum up to k) + (k+1) = k(k+1)/2 + (k+1)。经过一行代数变换，可将其改写为 (k+1)(k+2)/2，这恰好是将 k 替换为 k+1 后的公式。✓既然它在起点（0）成立，而且每一步都会将其带到下一个数，那么它就对所有整数永远成立，只需一个有限论证。这就是证明。证明助手做的正是这种推理，只不过会机械地验证每个步骤——包括“那一行代数”——确实从此前内容推出。
值得领会的跃迁：证明将“无穷多种情况”转化为一个有限且可检查的论证。这正是测试在结构上所欠缺的超能力。
形式化验证之所以强大，部分原因在于它澄清了 bug 究竟从何而来。任何规则检查系统中的缺陷都可以追溯到以下三处之一：
| bug 来源 | 含义 | 能通过证明消除吗？ |
|---|---|---|
| 规格说明 | 数学或规则本身有误（缺少条件、定义错误） | 可以，这正是形式化验证的主场 |
| 实现 | 代码未能忠实执行正确的规格说明 | 部分可以；此类失败常会留下可检测的证据 |
| 失效的假设 | 整个系统所依赖的某件事结果被证实为错误 | 不可以；假设是不可再约简的基础 |
这个分类的重要性超乎表面所见，第 2 和第 3 部分都围绕它展开。最深层、最危险、可能永远隐藏的 bug，往往存在于规格说明中：即系统应当做什么的数学描述。而规格说明正是机器检查的证明可以直接检查的对象，并且能一次覆盖所有情况。这就是严肃的形式化验证工作首先瞄准它的原因。
形式化验证很强大，但它的承诺是精确的；误解它会使人误入歧途。因此，应该谨慎地表述：
证明保证的是：在既定假设下，系统符合规格说明。仅此而已。
由此带来四个后果，每一个都很重要：
这份精确性并未削弱形式化验证，反而正是它的强处。它告诉你确切地得到了什么。正如我们将在第 3 部分看到的，Zcash 团队明确陈述其范围和假设（“我们在这些已命名的假设下证明了供应健全性，而非隐私”）正是这种诚实的典范。
为了保持可读性，我们进行了简化。真实的规格说明是用精确的形式语言写成的，而不是英语句子；形式化验证有多种风格（交互式定理证明、模型检查、基于 SMT 的方法），分别适用于不同问题；即使有 AI 协助，编写这些证明仍然是需要技能和付出努力的工作。我们也略过了证明助手如何在内部表示逻辑。这些都不改变核心：一个规格说明、一个系统，以及在既定假设下证明两者一致的机器检查证明。需要时，我们会回到这些细节。
| 术语 | 通俗含义 |
|---|---|
| Formal verification | 从数学上证明系统在所有情况下均符合规格说明 |
| Specification | 对“正确行为”含义的精确陈述 |
| System | 实际被检查的程序、电路或协议 |
| Proof | 为所有情况确立断言的一条有限逻辑步骤链 |
| Proof assistant / theorem prover | 检查证明每一步的软件（Lean、Rocq、Isabelle） |
| Machine-checked | 由计算机逐步验证，而非仅由人类阅读 |
| Induction | 一种证明技术：起点为真，每一步将其带到下一步 |
| Assumption | 证明所依赖的条件；若为假，保证可能不成立 |
形式化验证会取代测试吗？ 不会。两者相辅相成。测试能以较低成本发现实际问题和错误假设；验证则排除测试可能永远不会抽样到的整类 bug。
既然它如此强大，为什么不对所有东西进行形式化验证？ 它成本很高，且需要专业技能，尽管 AI 协助正在降低这一成本。它适用于罕见 bug 会造成灾难的系统，而这恰恰是其成本能够获得回报的领域。
经过形式化验证的系统仍然可能失败吗？ 是的，如果规格说明错误、定义被错误表述、假设不成立，或失败发生在未被指定的范围之外。证明只覆盖它声称覆盖的内容。
机器检查的证明是否比人类证明更值得信赖？ 对于大型、复杂的证明，通常是的。机器不会忽略微妙缺口或接受含糊论断，尽管它仍然信任被提供给它的规格说明和定义。
如果 AI 协助编写证明，为什么要信任它？ 因为证明助手会机械地检查每一步。AI 提出步骤；机器验证它们。错误步骤会被直接拒绝，因此 AI 加速了工作，却不削弱保证。
你证明一家银行的软件“绝不会让账户余额变为负数”。一年后，钱仍在不断丢失。这两件事如何能同时为真？（答案如下。）
该证明只保证了一项属性：余额绝不会变为负数。钱可能以这项属性从未涵盖的方式丢失，例如，一个 bug 将资金转入了错误的（但余额仍非负的）账户，或系统中从未被指定的一部分存在缺陷。验证精确完成了它所承诺的事情，仅此而已。这正是第 6 节注意事项的实际体现：证明覆盖规格说明，而不是关于“正确”的每一种可想象概念。
第 2 部分 · Orchard Bug： 我们将完整讲述真实的 2026 年故事。一个隐私系统使用密码学证明来隐藏金额，而其数学中一行约束不足的内容意味着这些证明可以被造假，从而允许无限量、不可见的伪造。我们将确切了解“约束不足的电路”意味着什么、为何这类 bug 能够永远隐藏，以及它为何不止发生过一次。
属于 ZecHub 的形式化验证系列。