如何认证一门年轻语言达到了生产可用？

每一个语言的作者，迟早都要面对这样一句话，通常来自那个决定自己的团队要不要押注的人：

我怎么知道这个东西生产可用了？

对一门有十年生产历史的语言，答案又简单又便宜：指着用户就行。Postgres 有三十年的生产伤疤。Java 有二十五年没垮掉的交易系统。伤疤就是认证。

一门年轻的语言没有伤疤。更糟的是，如果你构建这门语言的前提就是让 AI agent 写大部分代码 — 这正是 SuperJ 的设计前提 — 你连“我的资深工程师会做 review”都靠不上。reviewer 也是机器。伤疤必须在代码上线之前、靠构造去挣得，而不是等事故之后。

这篇文章是我们花一个月构建这样一套认证之后得到的答案。它不是一篇关于直觉或氛围的故事。它是一次测量战役的报告，结尾有一个数字 — 并且它带着这样的认证不能说什么的诚实边界，因为边界正是大多数语言声明悄悄跳过的部分。文章最后是我们对自己认证做的审计，因为一个不会失败的 checker 不是 checker，而我们发现了五种让自己的 checker 悄悄不会失败的方式。

前提：“生产可用”必须分解

“生产可用”不是一个性质。它至少是四个，而且它们的测试方式各不相同：

1. 语言做到了手册说的 — 语义与 spec 一致。
2. SDK 做到了它的签名说的 — 每一个公开 API 都 behave。
3. 编译器发出的代码保留了源码的语义 — 优化流水线不会破坏程序。
4. 内存模型兑现了它的承诺 — 没有静默泄漏，确定性的回收。

每一项都需要不同的验证技术。test suite 检查 (1) 和 (2) 中你想到的那些用例。formal proof 对所有用例检查它们 — 但只对可判定的性质。differential harness 把 (3) 和一个参照物对拍。测量仪器检查 (4)。认证就是这样一种纪律：拒绝把它们混为一谈，拒绝在任何一项上超出其技术真正能看到的东西去做声明。

下面描述的工具大约花了两周。它产出的是一份横跨 43 个类别、共 2,644 项检查的报告，其中每一条声明要么被机器检查，要么以声明的精度被测量，要么被显式标记为不可证明。最后一个类别上的零 — 没有任何未记账的东西 — 才是真正的产品。

Layer 1：一致性台账 — 改造 JCK 的想法

Java 有 JCK：一个一致性套件，spec 里的每一条规范性陈述都有正反两个一致性测试。JCK 的通过就是业界对“Java 按预期工作”的定义。一门年轻的语言没有业界，所以没人会为你建一个 JCK — 这反而是好事，因为你可以建一个更好的：为你自己的手册建一个 JCK，用你要求别人语言的那套纪律来检查它。

结构很简单。把手册解析成离散的、编号的 claim。每条 claim 至少一个测试。一个 linter 在任何 claim 没有覆盖测试时让构建失败。

{
  "id": "I002",
  "sec": "identical-to-java",
  "topic": "Control flow",
  "text": "if/else, for, while, do-while, break/continue..."
}

对 SuperJ 的手册，这产出了 92 条 claim，分四类 — 与 Java 相同、从 Java 移除、与 Java 不同、SuperJ 新增。分类才是有意思的部分。“与 Java 相同”的 claim 验证起来很便宜 — JLS 这个 oracle 现成的。“SuperJ 新增”的 claim 最贵，因为唯一的 oracle 是手册自己的行文 — 这意味着行文必须规范到可以拿来测试，而且测试必须反转成（跑到红）才算数。

每条 claim 然后在台账里拿到一个可证明性层级：

• A — 已形式化证明。 有一个机器检查的证明覆盖它。
• B/C — 可证明，有证明形状 — differential 网格、穷举小定义域、状态机。
• D — 描述性。 一个环境变量的文档、一个表头、一个包列表。不是语言语义；留在测试层，而且这完全没问题。

战役结束后的最终计数：92 条 claim 中 77 条已形式化证明，零条未评估，12 条显式描述性，3 条钉为 divergence cell。Divergence cell 是营销页面会藏起来、而认证必须亮出来的部分：编译器与手册不一致的地方，用红色测试钉住，直到编译器跟上来才转绿。没有可见红色 cell 的认证是在用 omission 撒谎。

Layer 2：全定义域证明 — “对所有输入都对”变成定理的地方

测试是抽样。对整数来说，“抽样”和“穷举”只有在定义域很小时才是同一回事。对 32 位整数，定义域是 2³² — 你没法靠抽样到达确定，但 z3 可以证明。诀窍是把语言的算术定律陈述为对整个定义域的 SMT 查询：

law('wraparound involution (a+b)-b == a', (a + b) - b != a)
law('overflow rule: INT_MIN / -1 == INT_MIN (JLS 15.17.2)', ...)

在整个 bitvector 定义域上 unsat 意味着：在全部 4,294,967,296 个输入中不存在反例。不是“我们测了很多输入” — 这条定律是定理。得到这种待遇的数值内核：

定义域	定理数	“全定义域”的含义
int32	10 条定律	全部 232 对
long, i128, i256, i512	36 条定律	全部 264…2512 个值
float/double 符号代数	4 条定律	全部 264 个位模式，含 NaN
SIMD byte lanes	lane 定律	全部 65,536 个 (a,b) 对 × 16 lanes

三条让证明可信而不是表演性质的工程笔记：

第一：模型必须与真编译器 differential 对拍。SuperJ 算术最初的形式化模型漏掉了 JLS 15.17.2 溢出规则，而真编译器正确实现了它 — 是 differential 抓住了它。语言是对的，模型是错的。没有那个 1,124 格的编译器-vs-模型网格，这些证明会一直在漂亮地证明错误的东西。

第二：对 z3 的语义要懂到超过你信任它的程度。z3 的 % 是 bvsmod — floored division，符号跟随除数。Java 的 % 是 irem，符号跟随被除数。天真的“已验证的 matching law”会产出一个看起来像编译器 bug 的假反例，浪费你一天。修法是定义式的：先用 a - (a/b)*b 构造 Java 的余数，然后再证那条定律。

第三：穷举性是关于编码的声明，不是一种氛围。“对全部 2³² 个输入证明”只有当编码真的覆盖 2³² 个输入时才成立。你的验证器的验证器在读那份 z3 脚本，而那个验证器就是你。

long 之问：你怎么证明一个 2⁶⁴ 的定义域？

这是读 C 认证工作的人（CompCert、ISO C 标准的附录、LLVM 正确性文献）总会问到大类型时的时刻。long 是 64 位。它的有符号范围是 −9,223,372,036,854,775,808 … +9,223,372,036,854,775,807。你不可能在宇宙的生命周期里穷举它 — 2⁶⁴ 次迭代、每秒十亿次，是 292 年。测试甚至没法可靠地叫出那些边界 case 的名字。那凭什么能声称 long 的算术在数学上正确？

答案与 CompCert 用的同一招，借自硬件验证，它建立在一个观察上：那些数字从来不需要被枚举 — 需要枚举的只是它们服从的规则。

SuperJ 里的 long 被定义为 64 位二进制补码整数，其行为由一小组定律固定。每条定律都是一个全称量化陈述 — “对定义域中所有的 a、b，这个恒等式成立” — 而一条看似无限大的定义域上的定律之所以能变成一次有限的 SMT 查询，是因为 z3 的编码方式：一个 64 位值就是一个恰好 64 个 cell 的位向量，所以 solver 推理的是位结构，不是数值大小。问 z3 (a + b) - b != a 是否可能对 64 位的 a, b 成立，就是在让它找一个反例位模式；如果 solver 返回 unsat，就不存在这种模式 — 这就是对全部 2⁶⁴ 对的证明，在笔记本电脑上大约四十秒跑完。

具体来说，long 内核带九条定律，分三个家族：

环定律（代数课，在有限群上）：(a+b)-b == a 以及 (a*b)*b⁻¹ 式的 wraparound 恒等式。它们证明 wrapping 是一个对合 — 加完再减，精确回到出发点，对每一对输入都成立，包括边界上。如果编译器哪天“优化”掉了一个溢出检查而且做错了，这条定律会抓住那次翻译。

除法的边缘 case — Java 派生语义咬人的地方：

LONG_MIN / -1 == LONG_MIN        (JLS 15.17.2, the overflow rule)
x % y has the sign of x, not y   (truncated division, not floored)

第一个是著名的 case：-9223372036854775808L / -1 应该是 +9,223,372,036,854,775,808 — 这个数在定义域里不存在 — 所以 spec 把它钉在 LONG_MIN 本身。test suite 只能围绕边界抽样；证明钉住的是整个格：每一对输入 a / b 都被同时对照 spec 公式检查过。第二个是坑 C 移植者（floored bvsmod）和 Python 移植者（floored %）的那个：符号约定是被证明的，不是被假设的 — z3 定律对全部 a、全部 b ≠ 0 陈述了它。

移位与掩码定律：a << (s & 63) 永不逃出定义域，移位计数掩码是 63（不是 127 — 那是 i128 的掩码；每个位宽有自己的），并且掩码幂等。每条都是一行的全称恒等式。

扩展性是漂亮的部分。一个 512 位整数的定义域是 2⁵¹² — 比可观测宇宙的原子数还大一个你写不下来的倍数。证明不在乎。Bitvector 定律在陈述上与位宽无关；变的只是模数。i128/i256/i512 的证明就是 int32 的证明换个位宽重跑 — 36 条定理，同样的形状，每条依然对整个定义域穷举。这是 SMT 路线相对测试的收益：确定性对定义域大小的代价是常数。i512 — 一个其值数比任何物理存在能数清的都多的类型 — 的认证，和 byte 的认证一样完整。

而锚定现实的仍然是 differential：solver 证明的每条定律，还会在定律所关于的边界值上逐格对真编译器检查 — LONG_MIN、LONG_MIN + 1、-1、0、+1、LONG_MAX — 因为对模型的证明加上对产物的 differential，才能让“这门语言数学上正确”和“这个二进制算出数学上正确的答案”是同一个意思。

这正是 C 世界用形式语义工作（CompCert 内核、Cerberus 的 ISO C11 语义）追求的标准 — 在精确陈述的定义域上的、机器检查的小定律。区别在范围与诚实：CompCert 证明编译器保持语义；一门年轻的语言可以用更便宜的方式获得同等信心 — 直接在完整定义域上证明语义本身，并把产物与模型做 differential 对拍。这是同一数学标准下的认证，只是裁剪到一门年轻语言真正养得起的大小。

Layer 3：编译器本身 — translation validation

你没法像 CompCert 证明它的内核那样证明一个闭源编译器。你能做的是 translation validation：对每个函数证明编译器的输出保持了你在乎的性质。SuperJ 的测试语料编译成 LLVM IR，其中横跨 124 个文件的 3,528 个发出函数现在每一个都带着：

• 没有静默的未定义行为。从每个函数入口块出发的符号走查，除了被 no-return 调用支配的情况，绝不能到达 unreachable。finally 外提产生的死 IR 豁免；常量分支（br i1 1）只走活的那条边。
• 边界守卫。每一处非常量下标的用户数组访问，都被一个显式检查所支配。常量折叠的下标、rodata、编译器生成的 dispatch 走查豁免 — 理由被记录在案，不是一句带过。
• CFG 完全性。每个块都终止；每个分支目标都存在。
• Profile 等价。89 个程序 × {debug, release, AVX2} — stdout 和 exit code 逐字节一致。优化流水线是在语料上被认证的，不是被信任的。
• 数值精化。40 个生成程序，由形式化模型独立算出期望输出；模型、debug 构建、release 构建三方逐字节一致。

诚实边界：这是 translation validation，不是编译器验证。它检查的是编译器的输出，不是编译器。完备性的上限是语料 — 这正是为什么下一步（已作为上游 ticket 提出）是把验证器跑进 superj test：每一次测试构建在被构建时就被验证，语料从快照变成移动的前沿。

Layer 4：零垃圾 — 一门 no-GC 语言欠你的认证

在 Java 里，“它泄漏吗”有一个律师式答案：GC 会回收它。在 SuperJ 里没有回收器，所以这个问题是存在性的 — 手册诚实地回答了它：泄漏是程序保活着的、作者并不打算保活的内存，而语言唯一不加警告允许的形状是一个故意保活的全局 arena 引用。这个定义让 leak-freeness 部分地变成关于意图的陈述 — 没有任何工具能证明意图。所以认证把它分解成可证明的部分：

Arena 回收是定理。每个 arena {} 块在每条退出路径上都被丢弃 — 走到末尾、return、break、continue、throw、带标签的 break — 任意嵌套深度，LIFO 顺序，且每个分配点验证 drops == creates。作为语句文法上的 pushdown 系统证明，由运行时 oracle 落地。

栈放置安全是定理 — 而且它的补集也被检查。如果编译器说一个值死在栈上，那就没有任何执行路径在它死后读它。以 z3 陈述在逃逸分析的动作代数上，检查为 UNSAT，并带复合可靠性（callee 的干净摘要保持结论）。定理的补集也被机器检查：witness-completeness pass 证明 dump 恰好报告源码实际展现的那些逃逸 — 两个方向都不冤枉人 — 在一个枚举动作空间的 18 形状网格上验证。（仍然经验性的部分 — 对未见过的语法的覆盖 — 在边界一节。）

Flatness 是有两个尺度的定律。任何区域跑 N 和 10N 两次迭代。一个每轮保有 r 的泄漏对 N 是线性的，在数学上不可能躲过比值测试；一个真正 flat 的区域 delta 为 0。这把手册的“跨尺度 flat”守则变成一个带判定代数的 checker：

判定	含义
FLAT	两个尺度上 delta 都是 0 — 认证零垃圾
BOUNDED	增长 ≤ 一个 4 MiB chunk — 表格预分配，设计使然
LINEAR-RETENTION	随 N 增长 — 按测得速率计的泄漏
INTENTIONAL	有文档的代价（exception 对象：80 B/次 throw）

然后是：SDK，一个方法一个方法地来。全部 2,910 个公开 API 方法从 SDK stub 枚举出来，合成 flatness 探针，编译，在两个尺度上运行：

判定	数量	含义
FLAT	1,799	在规范形状下认证零垃圾
BOUNDED	207	增长在一个 chunk 之内（表容量）
CARVEOUT	527	只在复用形状下 flat — 一个系统性原因，已开 ticket
NEEDS-FIXTURE	52	需要活对象（fixture、callback）
SIDE-EFFECT	541	网络/进程/GPU — wrapper 层检查

3,126 个已记账的方法每一个在台账里恰好有一个判定，对账保证零未测量。仅这一役就掉出两个真实缺陷：一个即使在 arena 块内也每轮泄漏约 126 B 的 SDK carve-out（#4790），以及 — 那个让整个演习显得活起来的 — 一个 CRITICAL SIGSEGV：HttpClient.request 传 null 参数会让运行时裸段错误崩溃，而不是抛 NullPointerException（#4814）。这种东西用例子是找不到的。只有拒绝让任何一个方法处于未记账状态，才能找到它。

大多数认证会跳过的部分：我们选择不去证明什么

上面每一条 claim 都带着一条边界，而且这些边界是在结果出来之前写下的：

• 逃逸分析：安全性质已被证明；“抓得住一切”的部分保持经验性。这个区分很重要，所以完整写出来。机器检查的是：(a) 安全定理 — 每个被判定为 -> STACK 的分配只在其分配帧内被读，陈述在 5 动作摘要代数 {return, store-to-static, store-to-array, store-to-global, native-barrier} 上，带复合可靠性（callee 的干净摘要保持结论）；(b) witness 双向性 — 源码见证的每个逃逸都以 non-STACK 出现在 dump 里，且 dump 里每个 non-STACK 判定都对应一个源码 witness（两个方向都不冤枉人），在枚举动作空间的 18 形状网格上验证；(c) arena 回收完全性 — 每个块在每条退出路径上丢弃，drops == creates，作为 pushdown 系统证明。保持经验性的是：形状空间完备性 — 分析器的推理是否覆盖程序表达逃逸的每一种语法方式。18 个形状枚举的是动作空间；一种结构解析器和分析器都没见过的全新语法形式，对两者都不可见，两者会一致地、一起地错。#4744（一个 dead-branch promotion）恰好属于这一类：一个按源码推理应该是 STACK 的 dump 判定。红色 cell 保持红色就是这个原因：不是因为安全定理弱，而是因为对未见语法的完备性受枚举所限，且边界是用 ticket 强制执行的，不是靠信念。

• Checker 也是代码。Translation validator 约 600 行 Python。它自己的可靠性建立在 LLVM 文本解析上，后者咬了我们四次（多行 switch 终结符、!dbg 元数据、SSA 临时值复用、常量分支）。每一咬都变成了一个测试。

• 没有 assessor 的“认证”只是一个声明。ISO 风格的符合性评估需要第三方。我们构建的是让这种评估变得可评估的证据基座。

• 与 javac 的两处活跃分歧，在 definite-assignment 和 reachability 上 — 已 filing、已钉红，且形式化模型刻意跟随 JLS，让这些钉子重新变红直到编译器跟上。

没有记录边界的认证是营销。边界才是让它可审计的东西。

审计：我们自己的认证可能悄悄撒谎的五种方式

建完上面这一切之后那个不舒服的问题是：谁来检查 checker？我们对认证框架本身做了一次专门审计 — 每一道 gate、每一个 exit code、每一个分母 — 发现了五个对这类战役而言都很通用的缺陷。它们每一个的形状都相同：一个报了数字却不会失败的检查。

1. 从不 gate 的 gate。spec-tag linter 打印“100.0% contract-cited, 92/92 claims covered” — 然后无条件 exit 0。数字是真的，但那道闸门是戏剧装置：下游永远不会注意到任何回归。metamorphic harness 同病：一个编译失败的程序被悄悄从分子和分母里同时丢掉，所以一个把 60 个程序全弄坏的生成器 bug 会打印“0/0, all identical”然后通过。两者现在都 hard-fail。教训成了一条规则：没有失败 exit code 的检查是 dashboard，不是 gate。

2. 正则盲区 — 1,463 个测试里 1,462 个不可见。linter 的 @Test 模式要求注解、修饰符和方法名在同一行。语料里主流风格是把 @Test 放在单独一行 — 1,463 个测试方法里恰好一个匹配单行形式。那个“100% cited”是在 885 个方法的分母上算出来的，而真实计数是 1,113 — linter 在给它看不见的测试做认证。更糟的是，citation 正则不认识测试计划自己的 XX-NNN ID 格式，于是 // EXC-013: — 一个引用得完美无缺的 contract — 被算作 untagged。报告的兜底测试枚举器带着同样的单行假设。两者现在都接受多行形式。通用教训：当验证器声称“所有 X”时，用第二种机械手段交叉核对其分母与 ground truth（这里是：suite runner 自己的 .out 文件，它们列出每个真正跑过的测试）。

3. 没有警报的覆盖率回退。一次 SDK 更新加了 40 个公开方法。方法覆盖率从 2,910/2,910 悄悄滑到 2,870/2,910 — 98.6% — 而我们自己的项目笔记还在声称“每个包 100% 可测”。好几天没人发现。修法是一个 ratchet：一个基线文件钉住已覆盖总数，报告类别在 SDK 长出语料没提到的方法时就失败。补齐那 40 个之后（每个方法一个新探针，带 happy path、edge 和 error case：*Into 无分配变体、Bech32 plain-charset 对、listInto 对非目录文档化的 -2、WebSocket 方向感知的 bindFromClient/bindFromServer 及其 masking 规则），基线上调，ratchet 重新上膛。绝对百分比让人麻痹；delta 才能抓住。

4. 没接线 — 红了但看不见。metamorphic harness、spec linter、method-coverage 报告和 profile sweep 单独跑都是绿的，但都没出现在 HTML 报告里 — 所以任何一天它们红了，报告（人类真正读的那个东西）都还会说一切通过。四者现在都是报告类别。同样，那个 80 格的负编译矩阵从来没被收集 — 输出格式不同，collector 的解析器干脆什么都没找到，“119 cells, PASS”从未提到它不知道存在的 80 格。

5. 过期的 pin 和过期的二进制。两个负测试被标成 expected-to-fail，对应的 bug 其实早已在上游修好 — 矩阵一直红在“修复已落地，去翻 pin”上，却没有任何人被指派去看它。还有，memory sweep 发现两个 suite 二进制的源码已被删除；它们产生不出 memlog，而 sweep 的 exit code 把“没有日志”当成了没事。ticket 关了 pin 就必须翻；判定必须区分“passed”和“仪器缺席”。

审计还缩小了一个声明，而这是最健康的信号：memory sweep 之前报告扫了 113 个 suite；诚实的数字是 148，因为四个项目里的 37 个 suite 被悄悄排除在了它的 glob 之外。同样的代码，同样的工具 — 范围本身就是 bug。

代价是什么

• 最终报告里 2,644 项检查，2,643 绿。唯一红的那个是一个我们拒绝停止失败的、有 ticket 的编译器 bug。
• 29 个验证层（外加 14 个项目 suite 集），从全域 SMT 定理到逐方法垃圾证书，全部接进一份带 drill-down 的 HTML 报告。
• 大约两周的 agentic 时间，formal 类别从零重验约 40 秒，以及一张本会变成生产环境凌晨 3 点的崩溃 ticket。

把模式推广

如果你在认证任何系统 — 一门语言、一个数据库、一个协议栈 — 配方可以推广：

1. 让 spec 可数。每条规范性句子变成一条编号 claim。不能枚举的 spec 无法做一致性测试。
2. 可判定的就穷举证明。小定义域胜过抽样。全定义域胜过小定义域。bitvector 上的 z3 是软件工程里最便宜的确定性。
3. 对建模的一切做 differential 测试。在真实系统同意它之前，模型是错的。differential 是语言自己的 bug 冒头的地方。
4. 验证编译器的输出，不要信任它的输入。对闭源编译器，translation validation 是唯一诚实的技术 — 而且它与未来每一次构建都组合。
5. 测量那个运行时藏不住的性质。对 no-GC 语言，就是分配台账本身。跨尺度的 flatness 是“无泄漏”的定理形态。
6. 写下你没有证明的东西。边界一节是认证的签名。它之上的一切是证据；它之下的一切是带着 ticket 号的未来工作。
7. 审计认证本身 — 用会失败的 exit code。每道 gate 都要有一个红路测试：当它守护的东西真的回退时它打印什么，以及有没有东西失败？我们的审计在一个恰好为避免静默通过而建的框架里发现了五个静默通过缺陷。meta 层不是偏执；它是同一条规则往上抬一级。

“生产可用”不是一枚你被授予的徽章。它是一本你守得住的台账 — 每一行背后是一个定理、一次测量，或一个恰好说明它为什么还红着的 ticket。

完整的证据链 — 21 个 formal runner、2,910 方法的 SDK 台账、2,644 项检查的报告 — 在 review 仓库里公开。