原文标题：A shallow dive into formal verification
原文作者：Vitalik
原文编译：Peggy，BlockBeats
编者按：随着 AI 编程能力快速提升，软件安全正在面临一个新的悖论：AI 可以更高效地生成代码，也可以更高效地发现漏洞。对加密行业而言，这一问题尤其关键。智能合约、ZK 证明、共识算法和链上资产系统一旦出现缺陷，后果往往不是普通软件报错，而是不可逆的资金损失和信任崩塌。
Vitalik 在本文中讨论的，正是 AI 时代代码安全的另一条路径：形式化验证。简单来说，它不是依赖人类审计员逐行检查代码，而是把程序应当满足的性质写成数学命题，再用机器可检查的证明去验证这些性质是否成立。过去，形式化验证因门槛高、过程繁琐，一直停留在相对小众的研究和工程领域；但随着 AI 能够辅助编写代码和证明，这套方法正在重新获得现实意义。
文章的核心判断并不是「形式化验证可以解决一切安全问题」。相反，Vitalik 反复提醒，所谓「可证明安全」并不等于绝对安全：证明可能遗漏关键假设，规范本身可能写错，未被验证的代码、硬件边界和侧信道攻击也可能成为新的风险来源。但它依然提供了一种更可靠的安全范式：用多种方式表达开发者的意图，再让系统自动检查这些表达是否彼此兼容。
这对以太坊尤为重要。未来的以太坊将越来越依赖复杂底层组件，包括 STARK、ZK-EVM、抗量子签名、共识算法和高性能 EVM 实现。这些系统的实现极其复杂，但其核心安全目标往往可以被相对清晰地形式化。也正是在这类场景中，AI 辅助形式化验证有可能发挥最大价值：让 AI 负责编写高效代码和证明，让人类负责检查最终被证明的命题是否真的对应自己想要的安全目标。
从更宏观的角度看，这篇文章也是 Vitalik 对 AI 时代网络安全的一次回应。面对更强的 AI 攻击者，答案不是放弃开源、放弃智能合约，或重新依赖少数中心化机构，而是把关键系统压缩成更小、更可验证、更可信的「安全核心」。AI 会让粗糙代码大量增加，但也可能让真正重要的代码变得比过去更安全。
以下为原文：
特别感谢 Yoichi Hirai、Justin Drake、Nadim Kobeissi 和 Alex Hicks 对本文提供反馈与审阅。
过去几个月里，一种新的编程范式正在以太坊前沿研发圈以及计算领域的许多其他角落迅速兴起：开发者直接使用非常底层的语言编写代码，例如 EVM 字节码、汇编语言，或使用 Lean 编写代码，并通过在 Lean 中撰写可自动检查的数学证明来验证其正确性。
如果运用得当，这种方式既有可能生成极其高效的代码，也可能比过去的软件开发方式安全得多。Yoichi Hirai 将其称为「软件开发的最终形态」。本文将尝试解释这套方法背后的基本逻辑：软件的形式化验证到底能做什么，它的短板和边界又在哪里——无论是在以太坊语境中，还是在更广泛的软件开发领域。
什么是形式化验证？
形式化验证，指的是以一种可以被机器自动检查的方式，撰写数学定理的证明。
为了给出一个相对简单、但仍然有意思的例子，我们可以看一个关于斐波那契数列的基本定理：每三个数中就有一个偶数，其余两个则是奇数。
一个简单的证明方法是使用数学归纳法，每次向前推进三个数。
首先看基础情形。令 F1 = F2 = 1，F3 = 2。通过直接观察可以看出，这一命题——「当 i 是 3 的倍数时，Fi 为偶数；其他情况下，Fi 为奇数」——在 x = 3 之前都是成立的。
接下来是归纳步骤。假设该命题在 3k+3 之前都成立，也就是说，我们已经知道 F3k+1、F3k+2、F3k+3 的奇偶性分别是奇数、奇数、偶数。于是，我们可以计算下一组三个数的奇偶性：
由此，我们就完成了从「已知命题在 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 tactic，会自动把这一点和它对 fib(3k+4) 定义的理解结合起来。
在更复杂的证明中，你有时必须在每一步都明确说明：到底是哪一条数学定律允许你走出这一步，而且这些定律有时还带着一些晦涩的名字，比如 Prod.mk.inj。但另一方面，你也可以一步展开巨大的多项式表达式，并且只需要写一行诸如 omega 或 ring 这样的表达式，就能完成论证。
这里的不直观和繁琐，正是机器可验证证明虽然已经存在近 60 年，却一直停留在小众领域的重要原因。但与此同时，许多过去几乎不可能的事情，如今正因为 AI 的快速进展而迅速变得可行。
验证计算机程序
到这里，你可能会想：好吧，所以我们可以让计算机验证数学定理的证明，这样我们终于能确定，那些关于素数之类的疯狂新发现，到底哪些是真的，哪些只是藏在上百页 PDF 论文里的错误。也许我们甚至还能弄清楚望月新一关于 ABC 猜想的证明到底是否正确！但除了满足好奇心之外，这件事又有什么实际意义呢？
答案可以有很多。而对我来说，一个非常重要的答案是：验证计算机程序的正确性，尤其是那些涉及密码学或安全性的程序。毕竟，计算机程序本身就是一个数学对象。因此，证明一个计算机程序会以某种方式运行，本质上就是在证明一个数学定理。
举个例子，假设你想证明 Signal 这样的加密通信软件到底是否真正安全。你可以先用数学方式写清楚，在这个语境下，「安全」到底是什么意思。概括来说，你要证明的是：在某些密码学假设成立的前提下，只有拥有私钥的人，才能获知消息内容的任何信息。现实中，真正重要的安全属性当然有很多种。
而事实证明，确实已经有一个团队正在尝试弄清楚这件事。他们提出的其中一个安全定理，大致长这样：
以下是 Leanstral 对这一定理含义的总结：
passive_secrecy_le_ddh 定理是一个紧致归约，表明在随机预言机模型（Random Oracle Model）下，X3DH 的被动消息保密性至少和 DDH 假设一样难以攻破。
换句话说，如果攻击者能够攻破 X3DH 的被动消息保密性，那么他们同样也能攻破 DDH。由于 DDH 通常被假定为困难问题，因此 X3DH 也可以被认为能够抵御被动攻击。
该定理证明，如果攻击者只能被动观察 Signal 的密钥交换消息，那么他们无法以超过可忽略概率的优势，将最终生成的会话密钥与一个随机密钥区分开来。
如果再结合一个证明，说明 AES 加密被正确实现，那么你就可以得到一个证明：Signal 协议的加密机制能够抵御被动攻击者。
类似的验证项目也已经存在，它们用于证明 TLS 以及其他浏览器内密码学组件的安全实现。
如果你能做到端到端的形式化验证，那么你证明的就不只是某个协议描述在理论上是安全的，而是用户实际运行的那段具体代码在实践中也是安全的。从用户角度看，这会大幅提升「无需信任」的程度：为了完全信任这段代码，你不需要逐行检查整个代码库，只需要检查已经被证明成立的那些陈述。
当然，这里有一些非常重要的星号需要保留，尤其是关于「安全」这个关键字到底意味着什么。人们很容易忘记去证明真正重要的主张；也很容易遇到这样一种情况：需要被证明的主张，并不存在比代码本身更简洁的描述方式；还很容易在证明中偷偷引入一些最终并不成立的假设。你也很容易判断说，系统里只有某一部分真正需要形式化证明，但最后却在其他部分，甚至硬件层面，被一个关键漏洞击中。甚至 Lean 本身的实现也可能存在 bug。但在讨论这些令人头疼的细节之前，我们先进一步看看：如果形式化验证能够被理想且正确地完成，它可能带来怎样一种近乎乌托邦的前景。
面向安全的形式化验证
计算机代码里的 bug，本来就令人担忧。
当你把加密货币放进不可变的链上智能合约里时，代码 bug 会变得更加可怕。因为一旦代码出错，朝鲜黑客就可能自动把你的钱全部转走，而你几乎没有任何追索手段。
当这一切又被零知识证明包裹起来时，代码 bug 会变得更加可怕。因为如果有人成功攻破了零知识证明系统，他们就可以把所有资金提走，而我们可能完全不知道哪里出了问题——甚至更糟的是，我们可能根本不知道问题已经发生。
当我们拥有强大的 AI 模型时，代码 bug 还会变得更加可怕。比如像 Claude Mythos 这样的模型，再经过两年改进之后，可能已经可以自动化地发现这些漏洞。
一些人面对这一现实，开始主张放弃智能合约这一基本理念，甚至认为网络空间根本不可能成为防守方相对于攻击方拥有非对称优势的领域。
下面是一些引述：
为了加固一个系统，你需要花在发现漏洞上的 token，比攻击者花在利用漏洞上的 token 更多。
还有：
我们这个行业是围绕确定性代码建立起来的。写代码、测试、上线，然后知道它能正常运行——但以我的经验来看，这种契约正在失效。在真正 AI 原生公司的顶尖运营者中，代码库已经开始变成某种「你相信它能运行」的东西，而这种相信所对应的概率，已经无法再被精确说明。
更糟的是，有些人认为，唯一的解决办法是放弃开源。
这对网络安全来说，将是一个黯淡的未来。尤其对那些关心互联网去中心化与自由的人来说，这会是一个极其黯淡的未来。整个密码朋克精神，本质上都建立在这样一个理念之上：在互联网上，防守方拥有优势。搭建一座数字「城堡」——无论它体现为加密、签名还是证明——要比摧毁它容易得多。如果我们失去了这一点，那么互联网安全就只能来自规模经济，来自在全世界范围内追捕潜在攻击者，更广义地说，来自一种二选一：要么支配一切，要么走向毁灭。
我不同意这种判断。对于网络安全的未来，我有一个乐观得多的愿景。
我认为，强大的 AI 漏洞发现能力带来的挑战确实严峻，但它是一种过渡性挑战。等尘埃落定、我们进入新的均衡之后，我们将抵达一个比过去更有利于防守方的状态。
Mozilla 也认同这一点。引用他们的话：
你可能需要重新排列其他所有事务的优先级，以一种持续而专注的方式投入到这项任务中。但隧道尽头是有光的。我们非常自豪地看到，团队如何站出来应对这一挑战，其他人也会做到。我们的工作还没有完成，但我们已经越过拐点，并开始看见一个远不只是「勉强跟上」的、更好的未来。防守方终于有机会取得决定性的胜利。
……
缺陷的数量是有限的，而我们正在进入一个终于可以把它们全部找出来的世界。
现在，如果你在 Mozilla 的这篇文章里用 Ctrl+F 搜索「formal」和「verification」，你会发现两个词都没有出现。网络安全的积极未来，并不严格依赖于形式化验证，也不依赖于其他任何单一技术。
那它依赖什么？基本上，就是下面这张图：
过去几十年里，很多技术都推动了「漏洞数量下降」这一趋势：
类型系统；
内存安全语言；
软件架构改进，包括沙箱、权限机制，以及更普遍地明确区分「可信计算基」（trusted computing base）与「其他代码」；
更好的测试方法；
关于安全与不安全编码模式的知识积累；
越来越多预先编写并经过审计的软件库。
由 AI 辅助的形式化验证，不应被视为一种全新的范式，而应被看作一种强大的加速器：它正在加速一个早已向前推进的趋势和范式。
形式化验证并不是万能药。但在某些场景下，它尤其适用：也就是目标远比具体实现更简单的时候。这一点在以太坊下一次重大迭代中需要部署的一些最棘手技术里尤为明显，例如抗量子签名、STARK、共识算法和 ZK-EVM。
STARK 是一套非常复杂的软件。但它所实现的核心安全属性却很容易理解，也很容易形式化：如果你看到一个证明，它指向程序 P、输入 x 和输出 y 的哈希 H，那么要么是 STARK 所使用的哈希算法被攻破了，要么就是 P(x) = y。因此，我们有了 Arklib 项目，它试图创建一个经过完整形式化验证的 STARK 实现。另一个相关项目是 VCV-io，它提供基础性的预言机计算基础设施，可用于对各种密码学协议进行形式化验证，其中许多协议本身也是 STARK 的依赖组件。
更加雄心勃勃的是 evm-asm：这是一个试图构建完整 EVM 实现、并对其进行形式化验证的项目。在这里，安全属性没有那么清晰。简单来说，它的目标是证明这个实现与另一个用 Lean 编写的 EVM 实现是等价的；而后者可以在不考虑具体运行效率的情况下，尽可能追求直观性和可读性。
当然，理论上仍然可能出现这样一种情况：我们有十个 EVM 实现，它们都被证明彼此等价，却都共享同一个致命缺陷，而这个缺陷 somehow 会让攻击者从一个他们没有权限控制的地址中转走所有 ETH。但相比今天某一个 EVM 实现单独存在这种缺陷，这种情况发生的概率要低得多。另一个我们是在惨痛经验之后才真正意识到其重要性的安全属性——抗 DoS 能力——则相对容易被明确规定。
另外两个重要方向是：
拜占庭容错共识。在这个方向上，形式化定义所有期望的安全属性同样并不容易。但鉴于相关 bug 一直非常常见，尝试形式化验证仍然值得。因此，现在已经有一些关于 Lean 共识实现及其证明的进行中工作。
智能合约编程语言。相关例子包括 Vyper 和 Verity 中的形式化验证工作。
在所有这些案例中，形式化验证带来的一个巨大增量价值在于：这些证明是真正端到端的。很多最棘手的 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 实现本身，或者证明器的算术化表示，进行形式化验证。不过不用担心——这类工作也已经存在。
直接用汇编写代码，是我们五十年前经常做的事情。从那以后，我们逐渐转向用高级语言编写代码。高级语言会牺牲一定效率，但作为交换，它能让代码编写速度快得多，更重要的是，也让理解他人的代码快得多——而这对安全来说是必要条件。
借助形式化验证与 AI 的结合，我们有机会「回到未来」。具体来说，就是让 AI 来编写汇编代码，然后再写出形式化证明，验证这些汇编代码具备我们想要的属性。至少，这个目标属性可以只是：它与一个为了可读性而优化、用某种对人类友好的高级语言写成的实现完全等价。
这样一来，就不再需要一个代码对象同时在可读性和效率之间做平衡。我们会拥有两个彼此分离的对象：一个是汇编实现，它只为效率而优化，并根据具体执行环境的需求进行调整；另一个是安全主张，或者高级语言实现，它只为可读性而优化。然后，我们再用一个数学证明来证明二者之间的等价性。用户可以先自动验证一次这个证明；从那以后，他们只需要运行那个快速版本即可。
这非常强大。Yoichi Hirai 将其称为「软件开发的最终形态」，并非没有道理。
形式化验证不是万能药
在密码学和计算机科学中，有一个传统几乎和形式化方法本身一样古老：批评形式化方法，或者更宽泛地说，批评对「证明」的依赖。相关文献中有大量实践案例。我们先从密码学早期那些更简单的手写证明说起。Menezes 和 Koblitz 在 2004 年曾这样批评过它们：
1979 年，Rabin 提出了一种加密函数，它在某种意义上是「可证明」安全的，也就是说，它具备一种归约式安全属性。
所谓归约式安全主张是：任何能够从密文 y 中找出消息 m 的人，也必须能够分解 n。
在 Rabin 提出他的加密方案后不久，Rivest 指出，颇具讽刺意味的是，正是那个给它带来额外安全性的特征，在面对另一类攻击者时，也会导致系统彻底崩溃。这类攻击者被称为「选择密文」攻击者。具体来说，假设攻击者能够以某种方式诱使 Alice 解密一段由攻击者自己选择的密文。那么，攻击者就可以按照上一段中 Sam 所使用的同样流程来分解 n。
Menezes 和 Koblitz 随后又举了几个例子。它们共同呈现出一种模式：围绕「更容易被证明」来设计密码协议，往往会让协议变得不那么「自然」，也更容易在设计者根本没有考虑到的场景中崩溃。
现在，我们再回到机器可验证证明和代码。下面是一篇 2011 年论文中的例子，作者在经过形式化验证的 C 编译器中发现了 bug：
我们发现的第二个 CompCert 问题，体现在两个 bug 中。这两个 bug 会生成类似下面这样的代码：stwu r1, -44432(r1)
这里正在分配一个很大的 PowerPC 栈帧。问题在于，16 位位移字段发生了溢出。CompCert 的 PPC 语义并没有规定这个立即数取值宽度上的约束，因为它假设汇编器会捕捉到超出范围的值。
再看一篇 2022 年的论文：
在 CompCert-KVX 中，commit 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 操作。fallback 路径向移位操作传入了错误参数，导致在没有硬件 SHA-3 支持的 ARM64 平台上，SHA-3 摘要被破坏。这是一个 I 型失败：该内建函数被标记为已验证，而整个 NEON 后端并没有完成运行时安全性或正确性证明。
还有：
libcrux-psq crate 实现了一个后量子预共享密钥协议。在 decrypt_out 方法中，AES-GCM 128 解密路径会对解密结果调用 .unwrap()，而不是继续传递错误。一个畸形密文就可以让进程崩溃。
以上四个问题都可以归为两类：
第一类，是只有部分代码被验证了，因为验证其余部分太难；而结果证明，未被验证的代码比作者想象中更容易出 bug，而且这些 bug 往往更关键。
第二类，是作者忘记明确规定某个关键属性，而这个属性本来是需要被证明的。
Nadim 的文章对形式化验证的失败模式进行了分类；他还列举了其他失败类型。例如，另一个主要类型是：形式化规范本身是错的，或者证明中包含错误主张，却被构建系统静默接受。
最后，我们还可以看看发生在软件与硬件边界上的形式化验证失败。这里一个常见问题，是验证系统能否抵御侧信道攻击。即便你用一种理论上完全安全的加密方式保护了消息，但如果几米外的某个人能够捕捉电气波动，并在几十万次加密之后提取出你的私钥，那么你依然是不安全的。
「差分功耗分析」（differential power analysis）就是这类技术中一个如今已经被充分理解的例子。
差分功耗分析是一种常见的侧信道攻击。来源：Wikipedia
过去也有人尝试证明系统能够抵御这类攻击者。然而，任何这样的证明都需要某种关于攻击者的数学模型，然后你才能在这个模型下证明安全性。有时，人们会使用「d-probing model」：也就是假设攻击者能够探测电路中位置的数量存在一个已知上限。但问题在于，有些泄漏形式并不能被这种模型捕捉到。
这篇文章中观察到的一个常见问题，是转换泄漏（transitional leakage）：如果你观察到的信号并不取决于某个位置上的具体值，而是取决于这个值的变化，那么很多时候，你就可以从两个值——旧值和新值——之间恢复出所需信息，而不只是依赖某一个值。该文章还对其他形式的泄漏进行了分类。
几十年来，这些对形式化验证的批评，反过来也帮助形式化验证变得更好。相比过去，我们现在已经更善于警惕这类问题。但即便到今天，它仍然并不完美。
如果把视角拉远，这里其实有一条共同线索：形式化验证很强大。但无论市场宣传如何把它包装成可以带来「可证明的正确性」，所谓「可证明的正确性」从根本上并不能证明软件，或者硬件，在真正意义上是「正确的」。
对大多数人来说，「正确」大致意味着：这个东西的行为符合用户对开发者意图的理解。
而「安全」大致意味着：这个东西的行为不会以损害用户利益的方式，偏离用户的预期。
在这两种情况下，正确性和安全性最终都归结为一种比较：一边是一个数学对象，另一边是人类的意图或预期。严格来说，人类意图和预期本身也是数学对象——毕竟，人脑也是宇宙的一部分，而宇宙遵循物理定律；只要你有足够的算力，理论上就可以模拟它们。但它们是极其复杂的数学对象，无论是计算机还是我们自己，都无法真正理解，甚至无法读取。出于实际目的，我们可以把它们视为黑箱。我们之所以还能对自己的意图和预期有一些理解，只是因为每个人都有多年观察自身想法、并推断他人想法的经验。
也正因为我们无法把原始的人类意图直接塞进计算机里，形式化验证就没有办法证明某个系统与人类意图之间的比较。因此，「可证明的正确性」和「可证明的安全性」实际上并没有证明人类所理解的「正确性」和「安全性」——在我们能够模拟人脑之前，没有任何方法能真正做到这一点。
那么，形式化验证真正有用的地方是什么？
我倾向于把测试套件、类型系统和形式化验证，看作是同一种底层编程语言安全方法的不同实现形式——这可能也是唯一真正说得通的方法。它们的共同点在于：用不同方式对我们的意图进行冗余说明，然后自动检查这些不同说明之间是否彼此兼容。
比如，看下面这段 Python 代码：
在这里，你用三种不同的方式表达了自己的意图：
第一，直接表达：通过代码实现斐波那契公式。
第二，间接表达：通过类型系统说明输入、输出以及递归过程中的中间步骤都是整数。
第三，采用一种「案例包」的方法：也就是测试用例。
运行这个文件时，系统会用这些示例来检查公式是否成立。类型检查器则可以验证类型之间是否兼容：把两个整数相加是一个有效操作，并且会得到另一个整数。类型系统在物理计算中也常常很有用：如果你正在计算加速度，但得到的结果单位是 m/s，而不是 m/s²，那你就知道自己哪里算错了。而「案例包」式的定义，测试用例就是其中一种，往往也比直接、显式的定义更符合人类处理概念的方式。
你能用越多不同方式来表达自己的意图越好；理想情况下，这些方式应当彼此差异足够大，迫使你用不同的思考方式来处理同一个问题。这样一来，如果所有这些表达最终都能相互兼容，那么你真正表达出自己想要表达内容的概率也就越高。
安全编程的核心，就是以多种不同方式表达你的意图，然后自动验证这些表达是否彼此兼容。
形式化验证可以把这种方法进一步推进。借助形式化验证，你几乎可以用任意多种冗余方式来描述自己的意图；只有当这些描述彼此兼容时，程序才会通过验证。
你可以同时写出一个经过优化的实现，以及一个效率很低但便于人类阅读的实现，然后验证二者是否一致。你也可以请十个朋友分别列出他们认为这个程序应该满足的数学属性，再检查程序是否全部满足；如果没有通过，就进一步判断到底是程序错了，还是那条数学属性本身有问题。而 AI 可以让上述所有工作都变得极其高效。
那我该如何开始？
现实地说，你大概率不会亲自去写证明。形式化方法之所以一直没有真正普及，根本原因就在于：大多数人很难理解到底该怎么写这些该死的证明。
你能告诉我下面这段代码是什么意思吗？
（如果你想知道的话，它是某个证明中的许多子引理之一。这个证明针对的是 SPHINCS 签名某个变体的一项特定安全主张：也就是说，除非出现哈希碰撞，否则相较于任何其他消息的签名，为某一条消息生成签名，至少需要在某一条哈希链上使用一个位置更高的值。因此，它需要的信息无法从另一条签名中计算出来。）
你不需要手写代码和证明，而是让 AI 帮你写程序——可以直接用 Lean 写；如果你想追求速度，也可以用汇编写——并在这个过程中证明你想要的各种属性。
这项任务的一个好处在于，它本质上是自我验证的，所以你不需要一直盯着它。你完全可以让 AI 自己连续运行几个小时。最糟糕的情况，不过是它原地打转、没有取得进展；或者像我的 Leanstral 曾经有一次做的那样，为了让自己的工作更轻松，直接把它被要求证明的陈述替换掉。
你最终需要检查的是：它证明出来的那个命题，是否确实是你想要证明的东西。
在这个 SPHINCS 签名变体中，最终陈述如下：
这实际上已经勉强接近「可读」的边缘了：
如果由一个哈希摘要生成的数字（dig1），不等于由另一个哈希摘要生成的数字（dig2），那么以下说法就不成立：
对于所有数字，dig1 的每一位都小于或等于 dig2 的对应位；
对于所有数字，dig2 的每一位都小于或等于 dig1 的对应位。
这里比较的是通过加入校验和（checksum）后生成的「扩展数字」（wotsFullDigits）。也就是说，不可避免地，在某些位置上，dig1 的扩展数字会更高；而在另一些位置上，dig2 的扩展数字会更高。
在用大语言模型编写证明方面，我发现 Claude 已经足够好用，DeepSeek 4 Pro 也足够胜任。Leanstral 则是一个很有前景的替代方案：它是一个规模较小、开源权重、专门针对 Lean 写作微调的模型。它拥有 1190 亿参数，但每个 token 只激活 60 亿参数，因此可以在本地运行，尽管速度会比较慢——在我的笔记本电脑上，大约是每秒 15 个 token。
根据基准测试，Leanstral 的表现超过了许多规模大得多的通用模型：
根据我目前的个人体验，它比 DeepSeek 4 Pro 稍弱一些，但依然有效。
形式化验证不会解决我们所有问题。但如果我们希望建立一种互联网安全模型，而不是让所有人都去信任少数强大组织，那么我们就需要能够转而信任代码——包括在面对强大 AI 对手时，依然能够信任代码。AI 辅助的形式化验证，正可以让我们朝这个方向迈出重要一步。
就像区块链与 ZK-SNARKs 一样，AI 与形式化验证也是高度互补的技术。
区块链以隐私和可扩展性为代价，带来了开放可验证性与抗审查能力；而 ZK-SNARKs 又把隐私和可扩展性带了回来——事实上，甚至比原来更强。
AI 让你能够大规模编写代码，但代价是准确性下降；而形式化验证又把准确性带了回来——事实上，也比过去更强。
默认情况下，AI 会催生大量非常粗糙的代码，bug 数量也会增加。确实，在某些场景中，让 bug 增加甚至是正确的权衡：如果这些 bug 的影响较轻，那么即便是有缺陷的软件，也比没有这类软件要好。但在这里，网络安全仍然存在一个乐观的未来：软件将继续分化为围绕「安全核心」的「不安全边缘组件」。
这些不安全的边缘组件会运行在沙箱中，并且只被授予完成其任务所需的最低权限。安全核心则负责管理一切。如果安全核心崩溃，一切都会崩溃——你的个人数据、你的钱，以及更多东西都会受到影响。但如果某个不安全的边缘组件出问题，安全核心仍然可以保护你。
当涉及安全核心时，我们不会任由有 bug 的代码不断扩散。我们会积极控制安全核心的规模，使其保持足够小，甚至进一步收缩。相反，我们会把 AI 带来的全部额外能力，投入到提升安全核心本身的安全性上，让它能够承载高度数字化社会中极高的信任负担。
你的操作系统内核，或者至少其中一部分，将是这样的安全核心之一。以太坊会是另一个。理想情况下，至少在所有非高性能密集型计算中，你所使用的硬件也会成为第三个安全核心。某些与物联网相关的系统，会是第四个。
至少在这些安全核心中，那句老话——bug 不可避免，你只能努力赶在攻击者之前发现它们——将不再成立。它会被一个更有希望的世界取代：在那里，我们可以获得真正的安全。
当然，如果你愿意把自己的资产和数据交给那些写得很糟糕、甚至可能意外把它们全部送进黑洞的软件，那你也仍然会拥有这种自由。
