随身携带你的解释器

# Ship Your Interpreter 原文来源: https://www.basis.ai/blog/ship-your-interpreters/ 发布日期: 2026年10月16日 ##### 文章作者: Kiran Gopinathan (https://www.basis.ai/about/people/kiran-gopinathan/)、Nikhil Pimpalkhare (https://www.basis.ai/about/people/nikhil-pimpalkhare/)、Yiyun Liu (https://www.basis.ai/about/people/yiyun-liu/)、Zenna Tavares (https://www.basis.ai/about/people/zenna-tavares/) 我们让 LLM 为一种小型编程语言编写精确的数学规则，即形式语义（formal semantics），规定该语言应有的行为。随后我们使用 Lean——一个用于检查数学证明的工具——证明了该语言的解释器（即运行该语言所编写代码的程序）即使在被编译为 RISC-V 计算机芯片能理解的底层指令之后，仍然遵循这些规则。 LLM 在发现和利用生产环境软件中的漏洞方面正变得越来越强大，越来越多的 AI 辅助黑客攻击案例在现实中被报道。幸运的是，LLM 在编写*经验证的软件*（verified software）方面也在快速进步：这类程序附带数学证明，由计算机检查，能够排除整类整类的漏洞。 今年 4 月，我们的智能体[构建了一个 JavaScript 到 WebAssembly 的编译器](https://www.basis.ai/blog/verified-compiler/)，但未能证明该编译器保持了程序行为。数月之后，我们的智能体[验证了 Linux 的 nftables 编译器](https://www.basis.ai/blog/verified-nftables/)，它将防火墙规则转换为内核执行的指令。9 月，MIT 的研究员 Frans Kaashoek 和 Nickolai Zeldovich 使用 AI 智能体[验证了 xv6 操作系统内核](https://arxiv.org/abs/2609.04043)，一直验证到其机器码层面。 Basis 的目标是开发能够合理扩展到所有软件的验证方法，使得支撑关键基础设施的系统在设计层面就是安全的，并且能够跟上攻击者日益增强的能力。 随着 LLM 能力的不断提升，瓶颈正在从定理证明转向规范（specification）问题：我们如何确信我们所证明的命题捕捉到了我们真正关心的行为？ 要对程序做出任何证明，首先需要对其功能进行数学描述。这从描述其所用编程语言开始：每条语句、循环和函数调用在运行时的含义是什么。这些描述被称为*形式语义*，可以用纸笔书写，但越来越多地以 Lean 等证明辅助工具的形式表达。少数几种语言拥有形式语义（Standard ML、WebAssembly，以及通过 CompCert 的 C 语言），越来越多处理器执行的 RISC-V 指令集同样拥有形式语义。开发这些语义中的每一个都花费了数年的专家工作。 然而，大多数程序使用的语言没有形式语义，这构成了大规模部署经验证软件的主要瓶颈：没有语义，就没有精确的东西可供证明。 一个自然的解决方案是让 LLM 来编写语义，但 LLM 会犯错，而一个有缺陷的语义会破坏建立在其上的所有证明。测试有所帮助，但正如我们将在下文中展示的，一个语义可能通过所有测试却仍然是错误的。我们需要的是一种能够验证语义本身的方法。 没有形式语义的语言仍然有解释器或编译器，在实践中定义了其程序的含义。这里我们考虑一个激进的想法：让 LLM 证明其语义在每一个程序上都与真实解释器一致，将解释器视为事实标准。 为此，我们将解释器编译为 RISC-V——其含义已有形式化定义。这给出了一个精确（虽然难以阅读）的描述，说明解释器对任何程序做了什么。然后 LLM 为该语言编写可读的规则，并在 Lean 中证明：对于每个可能的程序，这些规则预测的结果与编译后的解释器打印的输出完全一致。如果某条规则是错误的，证明就会卡住。 我们报告了一项实验：我们让 LLM 为一种小型语言共同开发语义及其证明。我们使用 Lean 证明了该语言的解释器——运行该语言所编写代码的程序——即使在被编译为底层机器指令后仍遵循这些规则。整个开发成果——语义和证明——发布在 [GitHub](https://github.com/BasisResearch/ship-your-interpreter) 上。 本文余下的部分将详细介绍这个实验，首先解释为什么语义是更大规模验证工作的瓶颈，以及为什么测试不足以建立对语义的信任。然后我们展示证明过程如何改进了语义，我们如何处理内存推理，以及我们在此基础上构建了哪些工具。 ## 每个经验证的程序都始于语义 在你能证明程序做任何事情之前，你必须定义每个操作如何转换其状态，也就是定义它的*语义*。大多数语言在参考手册中以非形式化的文字描述其语义，并将具体细节留给编译器或解释器的实现。 *形式*语义将规则以数学方式写出，精确到足以让 Lean 4 这样的证明检查器使用。著名的例子包括 CompCert 对 C 语言的语义、CakeML 对 ML 的语义，以及 JSCert 对 JavaScript 的语义。每一个都花费了数年的专家工作，而且通常只覆盖了其语言的一个受限子集。 在本实验中，我们使用了 WHILE 的扩展版本，WHILE 是教科书（如 Nielson 和 Nielson 的 *Semantics with Applications* (https://orbit.dtu.dk/en/publications/semantics-with-applications-a-formal-introduction/)）中使用的小型命令式语言。我们的版本包含整数、字符串、带闭包的一等函数、`if`、`while` 和 `for` 循环，以及运行时错误。其解释器有 1,855 行 C 代码。一个 WHILE 程序如下所示（它打印 55）： ``` var i = 0; var sum = 0; while (i < 10) { i = i + 1; sum = sum + i; } println(sum); ``` LLM 为 WHILE 编写的语义是一组规则，每种表达式和语句对应一条规则。这些规则描述了如何根据表达式的子表达式来求值。对于整数加法，规则如下： ``` st, env ⊢ l ⇓ a, st' st', env ⊢ r ⇓ b, st'' a + b = c ───────────────────────────────────────────────────────── st, env ⊢ l + r ⇓ c, st'' ``` 规则从下往上读。最底部的一行是其结论。从环境 `env` 中的状态 `st` 开始，表达式 `l + r` 求值（`⇓`）为 `c`，留下状态 `st''`。状态保存变量值、闭包以及到目前为止所有打印输出；环境说明哪些变量在作用域内。线上方的前提解释了结果如何由子表达式得出。首先 `l` 求值为 `a`，留下状态 `st'`。然后 `r` 在该状态下求值为 `b`，留下 `st''`。最后一个前提 `a + b = c` 使用 WHILE 的 64 位回绕算术将两个整数值相加。 以 `\(1 + 1) + x` 为例，状态为 `[x ↦ 5]`，环境为 `{x}`：`x` 保存 5 且在作用域内。应用规则得到： ``` [x ↦ 5], {x} ⊢ (1 + 1) ⇓ 2, [x ↦ 5] [x ↦ 5], {x} ⊢ x ⇓ 5, [x ↦ 5] 2 + 5 = 7 ──────────────────────────────────────────────────────────────────── [x ↦ 5], {x} ⊢ (1 + 1) + x ⇓ 7, [x ↦ 5] ``` 也就是说，要对 `\(1 + 1) + x` 求值，我们先对 `\(1 + 1)` 求值得到 2，然后查找 `x` 得到 5，再将两个值相加得到 7。两个子表达式都没有改变状态，所以 `[x ↦ 5]` 保持不变。为了证明第一个前提的合理性，我们再次应用加法规则： ``` [x ↦ 5], {x} ⊢ 1 ⇓ 1, [x ↦ 5] [x ↦ 5], {x} ⊢ 1 ⇓ 1, [x ↦ 5] 1 + 1 = 2 ────────────────────────────────────────────────────────────── [x ↦ 5], {x} ⊢ 1 + 1 ⇓ 2, [x ↦ 5] ``` 这些规则的应用构成一棵树，从表达式各部分的值推导出整个表达式的值。LLM 用 Lean 写了大约 400 行这样的规则（[完整语义](https://github.com/BasisResearch/ship-your-interpreter/blob/fb07094cff916318c34b07494a7d739f1e53989b/Vsa/While/Semantics.lean)）。每条规则单独看起来都是合理的，但最终用户没有严谨的方法来判断它们是否忠实描述了 WHILE 程序在实际运行时的行为。 ## 一个语义可以通过所有测试却仍然是错误的 检查语义的常规方法是运行它。取一组测试用例，分别在语义下和真实解释器下运行每个程序，然后比较它们的输出。遗憾的是，在实践中，这个过程不足以建立对所生成语义的信任。 例如，我们语义的早期版本通过了为 WHILE 解释器生成的测试套件，但当函数名达到 59 个字符时与二进制文件产生分歧： ``` fn aaa...aaa() {} // 59 个 a 的名称 println("" + aaa...aaa); semantics: binary: ``` 二进制文件丢掉了右尖括号 `>`，对于更长的名字，它还丢掉了名字的一部分。测试套件中没有一个测试尝试过这么长的函数名。 原因在 [C 解释器](https://github.com/BasisResearch/ship-your-interpreter/blob/fb07094cff916318c34b07494a7d739f1e53989b/c/src/interp.c#L80)中，当用 `+` 拼接时它会将值转为字符串： ``` static char *stringify(Value v) { ... char buf[64]; switch (v.kind) { ... case VAL_FN: { const char *name = v.as.fn->fn_expr->as.fn.name; if (name) snprintf(buf, sizeof buf, "", name); else strcpy(buf, ""); break; } default: strcpy(buf, ""); break; } ... } ``` `stringify` 直接返回字符串值。任何其他值先被打印到栈上的 64 字节缓冲区中，然后复制到一个新分配的字符串中。具名闭包通过 `snprintf` 格式化为 `""`，匿名闭包格式化为 `""`，内置函数则落入默认分支，格式化为 `""`。`snprintf` 最多向 64 字节缓冲区中写入 63 个字符。 最初的语义对拼接和打印使用了相同的渲染规则，忽略了这个限制。为了证明与二进制文件的一致性，LLM 必须给拼接一个单独的渲染器。[修正后的语义](https://github.com/BasisResearch/ship-your-interpreter/commit/d0d2609425f0024a0b8a2ad0570f14723b391a8d)将闭包的渲染截断到前 63 字节： ``` "" + f ⇓ take 63 ("") ``` 这类细节是实现在内部积累的，但没有人明确写下来——这正是手工转录或由 LLM 编写的语义可能遗漏这类细节的原因。而且这并非没有程序会注意到的细节：动态语言中的代码经常依赖函数的字符串形式，用于日志记录、基于名字的分发或序列化值的比较。 即使是这样简单的违规，也会破坏建立在语义之上的任何验证工作，并可能留下隐藏安全漏洞的空洞。要构建安全且可扩展的语义，我们需要超越测试，因为测试套件只能检查某些人（或某个智能体）想到要写的程序。 ## Ship Your Interpreter "Ship Your Interpreter" 意味着将语义与人们实际运行的实现进行核对。将该语言已有的解释器编译出来，让 LLM 证明二进制文件*精化*（refines）了语义，也就是说两者对每个程序的打印输出达成一致。 我们[证明](https://github.com/BasisResearch/ship-your-interpreter/blob/fb07094cff916318c34b07494a7d739f1e53989b/VsaIris/Interp/EndToEnd.lean#L159)的定理如下： ``` theorem endToEnd_refinement : ∀ p c, Loaded interpRunLayout p (fillZero c) → (∀ out, BigStep p out ↔ Halts c out 0) ∧ (Diverges c → ¬ ∃ out, BigStep p out) ``` 该定理表明：对于任何 WHILE 程序 `p` 和*任何*机器配置 `c`，如果机器配置满足属性 `Loaded`，则语义与编译后的二进制文件的行为一致。`Loaded interpRunLayout p (fillZero c)` 这里表示 `c` 是一台即将通过解释器二进制文件运行 `p` 的机器。第一个结论 `∀ out, BigStep p out ↔ Halts c out 0` 表示：语义推导出输出 `out` 当且仅当机器以退出码 `0` 停止并打印了 `out`，也就是说对于成功终止的程序，预测的输出是等价的。第二个结论表明：机器无限运行（`Diverges c`）的任何程序 `p`，语义都不会为其推导出终止输出。 我们可以将这个定理可视化为一个*交换方图*（commuting square），展示语义和二进制文件如何对程序的输出达成一致。在下面的图中，上方的箭头将程序 `p` 与语义预测的输出 `out` 联系起来。下方的箭头将机器状态 `c` 与二进制文件成功停止时打印的输出联系起来。左侧的虚线是将程序与该机器状态联系起来的 `Loaded` 条件。在该条件下，定理说明两个输出是一致的，如右侧的双线所示。橙色箭头表示证明一致性失败时 LLM 被送回修订语义规则的过程。上方的箭头通过 BigStep 将程序 p 与输出 out 联系起来。下方的箭头通过 Halts 将机器状态 c 与 out 联系起来。Loaded 在左侧连接 p 和 c；双线在右侧标记输出相等。橙色箭头将失败的证明义务送回语义进行修正。对于加载到机器中的程序，语义与成功执行在输出上达成一致。 该定理在两个方向上都能捕获错误的语义。如果语义过于宽松，它会推导出二进制文件从不打印的输出，左到右的半边就会失败。如果语义过于严格，它对二进制文件做了某件事没有对应的规则，右到左的半边就会失败。无论哪种情况，LLM 都会得到一个无法完成的证明义务。根据我们的经验，该义务通常指向出错的规则。 RISC-V 是一种开放的处理器设计。我们使用其形式模型，用 [Sail](https://github.com/riscv/sail-riscv) 编写并翻译成 Lean，来定义每条机器指令如何执行。二进制文件是实际的 ELF 可执行文件：1,855 行解释器 C 代码由 gcc 编译，与 dlmalloc 和 newlib 链接，总共 25,336 条指令。作为对比，用 MachCSL 验证的 xv6 内核是 8,697 条 RISC-V 指令，由 6,593 行 C 和汇编构建，尽管其证明还涵盖了并发性（我们的不需要）。C 编译器的输出、C 库和内存分配器都在我们的定理之内。想要信任该结果的人只需阅读上面的定理陈述、`Loaded` 假设以及 `Halts` 和 `Diverges` 的两个简短定义。他们不需要信任 `BigStep`，因为证明已经将其与二进制文件进行了核对。 ## 协同开发语义与证明 开发证明迫使 LLM 对语义中的四个细节做出说明： - 整数算术必须在 64 位回绕，因为对最小整数取反与机器的行为不符； - `for` 循环的初始化器必须忽略中断状态（abrupt status），因为 C 代码就是如此； - 内置函数在 `print` 和拼接中的渲染方式必须不同； - 长闭包名必须截断到 63 字节。 每项修正要么始于一个无法完成的证明义务，要么始于一次二进制文件运行结果与语义不一致。63 字节截断是一个典型的例子。拼接情况的证明需要语义中的渲染与二进制文件一致，而对长名字来说这并不一致，因此在规则修改之前该义务无法完成。证明还捕获了 LLM 生成的关于 C 库的引理中的错误。LLM 陈述了每个函数的功能，然后对机器码证明该陈述。一个在单次 `malloc(24)` 之后任何堆都无法满足的分配器预留、一个对回绕大小不成立的 `realloc` 引理，以及一个写入 `errno` 但其引理中未提及的 `exit` 例程，都以同样的方式暴露出来——无法完成的证明义务。 ## 分离逻辑使二进制证明可行 所有证明均由 LLM 撰写。大部分困难在于对内存的推理。我们需要一个 `malloc`——分配内存的函数——的规范，使我们能够证明所有