Loading...
系列： 形式化验证 · 第 3 篇，共 3 篇 读者： 新手。第 1 和第 2 篇介绍了形式化验证以及 Orchard 漏洞；本篇收官之作将展示这两个理念如何在真实系统中相遇。我们会在讲解过程中回顾所需的一切知识。 你将收获： 准确理解 Zcash 对其新的“Ironwood”资金池究竟证明了什么、该证明的结构、其涵盖与未涵盖的范围、旧资金池如何被安全弃用，以及这为何指向构建加密货币的新标准。
在第 1 篇中，我们了解了证明一个系统正确意味着什么。在第 2 篇中，我们看到一个测试遗漏了四年的真实缺陷：一个约束不足的椭圆曲线乘法，可能允许无限量、不可见的伪造。本篇文章便是这一事件的解决方案：Zcash 如何不仅推出补丁，更通过机器检验的证明，证明整类漏洞已经消失。
当一个漏洞威胁到货币时，通常的回应是修补它，然后继续前进。Zcash 做了更具雄心的事。伴随一个名为 Ironwood、于 2026 年 7 月 28 日激活的新屏蔽资金池，其工程师发布了一份经机器检验的数学证明：在 Lean 证明助手中写成的逾 2,700 条定理，确立该新资金池在其声明的假设下无法产生伪币。该证明公开存放于开源 ironwood 仓库中，三个研究人员与密码学家团队耗时一个多月才完成。
这件事的重要性超越了 Zcash。它是最清晰的现实世界示范之一：你可以将一个正在运行的金融系统，精确定义“不可伪造”意味着什么，并证明它，而非寄希望于测试已经足够周全。它将承诺变成了定理。
第 2 篇以使这一切成为可能的洞见结束。请回顾它，因为本文的一切都建立于此：
一种不可检测的伪造漏洞只能存在于协议的规范中，也就是电路必须强制执行内容的数学描述。任何可检测的问题都会在公开账目中显现。因此，证明规范健全，就能一次性消除整类隐藏伪造漏洞。
为什么说“只能存在于规范中”？因为每个区块都会永久记录每笔交易的完整内容，包括其证明。如果软件错误地接受了一笔无效交易，任何人都可通过修正后的软件重放历史并发现它。该证据是永久且公开的。只有底层数学中的缺陷能够永远隐藏，因为不存在可以用来重放对照的“正确版本”。这正是形式化验证所针对的缺陷。
测试检验的是抽样输入上的行为，而 Orchard 漏洞之所以隐藏，恰恰是因为没有任何抽样输入触及它。关于规范的证明会同时覆盖所有输入，包括无人会想到尝试的边界情况。这是唯一足以让人有把握地弃用一个存在四年之久、不可见缺陷的保证类型。
该证明确立了一个核心性质，而这个性质构建于更深层的基础之上。
余额完整性： 存储在屏蔽资金池中的隐藏价值，永远不会超过流入其中的净公开价值。
这是用通俗语言表达的反伪造性质。货币可以进入屏蔽资金池（公开可见）并离开它（公开可见），但在金额被隐藏的内部，价值无法凭空产生。让我们用一个小型账本来具体说明（算术已验证）：
5 + 3 = 8 的输入产生价值 4 + 4 = 8 的输出。流入价值等于流出价值。余额完整性成立。✓8 的输入，却产生 4 + 4 + 2 = 10 的输出。这会从无中铸造 2 个单位。余额完整性禁止这种情况：资金池支付的价值永远不得超过流入它的价值。✗余额完整性是这样一个数学陈述：第二种情景永远无法产生有效交易。
为了保证余额完整性，研究人员首先必须证明有关零知识证明系统本身的一个更深刻、更微妙的性质。普通健全性（第 2 篇中“只有真实陈述才有见证”）对于屏蔽资金池而言竟然不够，原因很有意思：因为一笔隐藏交易可以包含任何内容，几乎每个陈述在技术上都存在某个见证。因此，研究人员证明了一项更强的性质：
知识健全性： 任何能产生有效交易证明的人，都必须实际拥有一个有效见证，即真实、被正确导出且位于正确地址的币。
其形式化工具是一个提取器：给定任何能够说服验证者的证明者，该程序可以从其身上提取出实际见证。如果总能提取出见证，那么一个有说服力的证明者就必然真正拥有见证。用第 2 篇的语言来说，知识健全性是这样的形式化承诺：不存在健全性缺口，不存在让虚假陈述蒙混过关的缺失约束。这正是 Orchard 漏洞所缺失的性质。证明该性质对于所有可能的证明者都成立，就是将那扇门彻底关上。
这项验证是一项严肃的人类工作，并非一键即可得出结果：
ironwood 仓库。为了推理该性质，Lean 模型将整个账本描述为一列交易，每笔交易都带有其操作、声明的公开价值和签名。研究人员称为 ValidLedger 的谓词直接转录了网络的共识规则：每项操作的见证必须满足所需条件，不得有任何消费标记（nullifier）重复出现，每个被引用的树状态都必须是系统真实达到过的状态，并且每个签名都必须验证通过。定理随后量化了每一个有效账本。这句话——“每一个有效账本”——正是关键所在：并非样本，而是全部，是任何真实攻击者可能组装出来的一切的超集。
余额完整性的结果由若干账本层面的定理组合而成，每一条都证明一条伪造路径已被关闭：每次消费都对应于一个真实的先前输出、总价值守恒、收到的票据始终可消费且无法被盗取，以及消费需要正确授权。一个独立部分——绑定签名——将每笔交易的隐藏价值与其声明的公开金额绑定，因此隐藏账目与公开账目无法悄然不一致。
一个微妙且诚实的问题是：该证明针对数学模型，但网络运行的是 Rust 代码。我们如何知道代码与模型一致？
团队划出了一条谨慎的边界，称为验证者的指纹。边界之上，Lean 证明将验证者视作精确的数学对象进行推理。边界之下则是普通的 Rust 实现。关键论证与第 2 篇相同：
真实软件偏离已证明模型的任何方式，都会是一个实现漏洞；而实现漏洞只能产生可检测的伪造，因为每个被接受的证明都会被永久记录，且可通过修正后的软件重放。
因此，证明处理不可检测的一类（规范），永久公开记录则处理可检测的一类（实现）。两者之间，不存在不可检测的伪造漏洞可以藏身之处。团队还通过运行真实验证者并确认它在捕获的案例中完全复现指纹，进行了交叉核对。
第 1 篇强调，证明只保证系统在声明的假设下符合规范，绝不意味着“永远不会有任何漏洞”。Zcash 的团队对这一点十分精确，而诚实的教育写作也必须如此。
该证明将 Ironwood 的安全性归约为一组小型、标准且命名明确的假设。特别是，其健全性依赖于 Ironwood 所使用椭圆曲线上离散对数问题的困难性（这是经过充分研究的假设，目前已知的最佳攻击需要大约 2^126 次操作，远超任何可行的计算能力），以及哈希函数的标准建模假设。有两条边界值得明确说明：
这些边界的明确命名丝毫不会削弱成就，反而正是它值得信赖的原因。该主张是精确的：*在标准密码学假设下，该资金池无法产生不可检测的伪币。*这是一条定理，而不是希望，其准确范围也被公开说明。
证明新资金池健全后，仍有一个问题：存在四年缺陷的旧 Orchard 资金池怎么办？你无法取消其过去的隐藏性，但可以限制其未来。
Zcash 引入了一种称为旋转闸门的机制。规则简单而强大：
价值只能从旧资金池流出，且不得超过可验证流入其中的金额。
由于资金进出屏蔽资金池时均公开可见（只有内部活动被隐藏），旋转闸门让整个网络可以检查流出的金额从未超过流入的金额。如果旧资金池内曾生成伪币，它们会触及这一上限，无法退出。随着诚实资金迁出且没有多余价值出现，社区将获得强有力的公开证据，表明该缺陷从未被利用。这是在不破坏隐私的前提下审计私密资金池供应量的最接近方法，它在保留 Zcash 隐私的同时，让供应完整性更接近 Bitcoin 等链的透明模型。
Ironwood 本身复用了已修正的证明电路，以一个空资金池重新开始，并增加了前瞻性保护措施（包括在未来量子计算机威胁到当今密码学时，资金仍可恢复的规定）。新的屏蔽活动现在通过 Ironwood 进行，而旧 Orchard 资金池则仅限于提款。
Ironwood 是 Zcash 构建方式更广泛转变的一部分。其下一代扩容工作（一种名为 Tachyon、基于递归证明并采用名为 Ragu 工具包的架构）正在一种有时称为高保障密码学的理念下开发：不将机器检验的形式化验证视为事后补充，而是将其作为交付新型密码系统的标准组成部分。
其逻辑很有说服力。前沿密码学正是人类直觉最薄弱、一个微妙且未经测试的边界情况可能隐藏数年的领域，正如 Orchard 所展示的。证明规范是唯一能扩展到“所有可能输入”、并通过构造消除这些缺口的技术。团队已表示，随着时间推移，他们有意将这种审查进一步延伸至实现层及更远处。预计这一标准将在 Zcash 内外得到更广泛采用。
为清晰起见，我们做了简化。实际的 Lean 开发比本文概述详细得多，包含对操作、陈述、承诺、nullifier 和签名的精确定义；“余额完整性”和“知识健全性”拥有严格的形式化定义，而我们仅用文字说明；归约至离散对数困难性会经过数个中间模型（证明者的代数模型和哈希的随机预言机模型），我们将其压缩为“标准假设”；并且我们在概念层面描述了指纹和旋转闸门。这些都不改变核心故事：一个“不可伪造”的规范、覆盖所有有效账本的机器检验证明、对范围与假设明确且诚实的声明，以及对有缺陷资金池的安全弃用。如需权威说明，请查阅 Project Tachyon 已发布的验证文档和 ironwood 证明仓库。
| 术语 | 通俗含义 |
|---|---|
| Ironwood | Zcash 的新屏蔽资金池（2026 年），取代有缺陷的 Orchard 资金池 |
| Balance integrity | 资金池支付的价值永不超过公开流入其中的价值 |
| Knowledge soundness | 有效证明要求证明者持有真实见证 |
| Extractor | 从任何有说服力的证明者处提取见证的程序 |
| Lean | 用于机器检验验证的证明助手 |
| ValidLedger | 定理据以推理的共识规则形式模型 |
| Fingerprint | 已证明数学与正在运行的 Rust 软件之间的边界 |
| Under stated assumptions | 只要指定的密码学假设成立，证明便成立 |
| Turnstile | 将资金池流出限制为其可验证存款的规则 |
| High-assurance cryptography | 将形式化验证作为标准步骤来构建密码系统 |
该证明是否意味着 Ironwood 没有漏洞？ 不，它也未作此声称。它在声明的假设下证明了一项精确性质——余额完整性。这排除了不可检测的伪造，而非所有可以想象的漏洞。
该证明是否保证我的交易是私密的？ 不。验证涵盖供应健全性（没有伪币），而非资金池独立的隐私保证。后者采用不同方式论证。
为什么要信任由人类（和 AI）编写的证明？ 因为它经过机器检验。Lean 证明助手会以机械方式验证每一步，因此信任建立在规范和已命名的假设上，而非任何人类或 AI 在每一步中的谨慎程度上。
旧 Orchard 资金池中仍存的币会怎样？ 它们可以被提取，但只能提取至可验证流入的金额上限，这由旋转闸门强制执行。这既保护了供应完整性，也有助于证明旧缺陷从未被利用。
这就是故事的终点吗？ 这是一个里程碑，而非终点。Zcash 的未来架构（Tachyon 及 Ragu 工具包）正在将形式化验证作为标准实践来构建，并将这一方法进一步延伸。
有人声称：“既然 Ironwood 已经过形式化验证，Zcash 就不可能再有任何事情出错。”请运用这三篇文章中的理念，给出两个不同的理由，说明该主张为何过于绝对。（答案见下文。）
第一，该证明在声明的假设（离散对数困难性和标准哈希建模）下涵盖的是一项特定性质（余额完整性）。如果某项密码学假设被攻破，或者在已指定范围之外出现问题（例如隐私、钱包软件或某个未经证明的组件），该证明对此无任何结论。第二，形式化验证保证系统符合已写下的规范；如果该规范本身未能捕捉某项真实需求，证明将忠实地认证错误的事物。这两点都是第 1 篇限定条件的重述：证明是精确且有边界的，它之所以强大，恰恰是因为其范围诚实，而非对任何事情都不会出错的笼统保证。
在三篇文章中，我们从一个一般理念走向一个实际应用：证明软件正确而非仅测试它意味着什么（第 1 篇）、一个真实的约束不足电路如何可能铸造不可见的货币（第 2 篇），以及覆盖余额完整性的机器检验证明如何永久消除那类漏洞（第 3 篇）。贯穿始终的是一个单一且诚实的承诺：不是“永远不会有任何漏洞”，而是“在声明的假设下，这一精确性质对每一种情况都成立”。对于隐藏自身金额的货币而言，这正是值得证明的承诺。
属于 ZecHub 的 Formal Verification 系列。