生产可用是一个谓词，不是一个徽章

这个声明

三个条款。每一个都可检查。零个可商量。

“这个发布是生产可用的”不是一种情绪 — 它是一个逻辑合取，每个条款都由具名的检查器带着公开的通过标准支撑。如果检查器没有运行，该条款就是 FALSE。如果证据过期，证书就是 FALSE。如果检查器本身坏了，证书就是 FALSE。

完整的声明

PR-v1 = C1 ∧ C2 ∧ C3

// 常设，而不是快照：
// 检查器每个发布周期重新运行 · 证据 90 天后过期
// 重发时覆写同一批公开文件 — 一个旧的 TRUE 永远不会赖着不走

每个条款背后是什么

条款，以及条款之下的证据

C1 · gating

Spec 一致性

语言的行为与规格说明所说的一致。

声明台账：手册中全部 92 条编号声明，每一条都映射到覆盖它的证据 — 没有证据的声明不能计入。
每一条语言测试都引用它的契约（spec、手册或工单），否则 spec-lint --strict 失败：100% 已引用。
覆盖 Java 共享子集的 JCK 风格一致性套件，以退出码判定。
蜕变差分测试：随机生成的程序经过保语义重写后，必须在 SuperJ、javac 与各变换之间产出逐字节相同的输出 — 发布门运行 60 程序四方案一致批次，并已验证 1,000 程序的活动运行。
负面一致性：非法构造必须以正确的诊断被拒绝 — 每个诊断码既有触发格子，也有防误报的静默格子。

C2 · gating

健全性 — 无未定义行为

安全的 SuperJ 无法到达未定义行为：没有内存不安全、没有错误分派、没有未证明的逃逸、没有未检查的算术危害。

全域证明 — 穷举，不是抽样：算术与转换定律由 SMT 在全部 2³² 个 int 值上验证，外加边界守卫、逃逸放置、arena 回收、确定赋值，以及完整的 1,112,064 个码点 Unicode 往返。
翻译验证：整个语料库发出的 LLVM IR 逐函数检查 — CFG 完备性、无静默不可达代码、边界守卫在场。
敌意输入：181 个攻击用例穿过解析器和解码器；敌意源码的编译器模糊测试；profile × sanitizer 矩阵。
SIGSEGV 审计：184 个发出的 IR 文件中的每一个空指针解引用点都被分类并证明有守卫，带有残余棘轮；所有语料库二进制零信号死亡。
单调发现台账 — 已关闭的缺陷类别重新出现即导致条款失败。还有 checker-P0 规则：检查器里的一个缺陷会使引用它的所有声明失效。检查器检查它们自己，带有植入缺陷的自测。

C3 · gating

零垃圾

内存的行为与文档一致 — arena 回收精确且 O(1)，栈放置安全，没有任何 SDK 表面的分配行为未被测量。

SDK 平坦度台账：全部 15 个包台账，3,598 个表面测得 FLAT，414 个 BOUNDED，1,054 个已记录的 carve-out — 并且零个没有判定的表面。一个未测量的表面即导致条款失败。
双尺度平坦度定律：每个“零分配”声明都在 N 和 10N 次迭代下用逐字节精确的仪表测量。速率增长就是泄漏；常数不是。
逃逸分析健全性的形式化：放置定理（判定 STACK ⇒ 无死后读取）是机器检查的；等级健全性在全语料库范围带棘轮。
Carve-out 随证书同行：每一条已记录的例外，连同它的工单，都列在边界里 — 绝不悄悄携带。

另有四个条款已建成并报告，但在 PR-v1 中刻意不作为门。一个暗示了自己并不具备的完备性的条款集会是第一个谎言 — 所以分阶段是明确的：PR-v2 加入 C4 ∧ C5，PR-v3 加入 C6。

C4 · not-gating

确定性

已建成并报告。自 PR-v2 起成为门。

C5 · not-gating

性能包络

版本化的常数固定在指定的机器上，武装了 >2× 回归棘轮。自 PR-v2 起成为门。

C6 · not-gating

往返重放

跨发布的语料库重放。自 PR-v3 起成为门。

C7 · not-gating

常设发布

让这一页保持诚实的机制。已报告，尚未作为门。

信任问题

为什么要相信厂商对自己颁发的证书？

问得对 — 自颁发的证书只会和它的激励一样好。六个性质把这一份和新闻稿区分开来。

反驳是本地的

这个声明的任何部分都不需要你信任我们。证据页面上的每一条命令都可以对着公开语料库复制粘贴运行。如果证书说 FLAT 而你的运行说 LEAK，你就反驳了它 — 在本地、在几分钟内、不必问任何人。一个你能自己反驳的声明，和一个你必须凭信接受的声明，是两种不同的东西。

它失败即关闭 — 而且失败过

这张证书是先变成 FALSE、之后才变成 TRUE 的。当 SDK 在语料库下方移动时 — 1.3.6514 的 string 模型重构 — 96 条测试与它们的钉住值矛盾，证书随之折叠，以 FALSE 渲染并具名失败的条款，直到迁移落地。一扇公开拒绝过自己项目的门，才是激励可供检查的门。

证据带有出处戳

每一次报告运行都盖有 {计划修订版、SDK 版本、语料库哈希、git 提交、工具版本}。证书无法漂移离开它的证据：过期证据，或来自不同提交的证据，渲染为 FALSE — 而不是“应该没问题”。

它有抓住自己的公开记录

认证活动审计了它自己的仪器，发现了认证可能撒谎的五种方式 — 从未把过门的门、悄悄缩小的分母、只在口头上的覆盖率、没接线的报告层、过期的钉住值。全部修复，并变成了证书现在强制执行的规则。被撤回的声明从不被编辑掉：有一个只追加的更正台账。完整的故事 →

边界随证书同行

每一张发出的页面都必须带有这不证明什么一节。只列通过项的契约是营销；边界才是让它成为一次测量的东西。如果一张证书页面没有边界一节，把它当作无效。

它是指针，不是载荷

发布只附带几百字节、指向证据的指针 — 工具链里不捆绑测试代码、验证器或语料库。声明与证据只隔一跳，证据按发布重新生成。没有任何东西以你无法检查的方式被打包。

诚实的部分

这不声明什么

每一张证书页面都必须带有它的边界，逐字来自契约。这是我们的。

没有编译器的完整形式化证明。证明覆盖特定的定律 — 全域算术、边界守卫精确性、逃逸放置安全性、arena 回收、CFG 完备性。流分析的完备性仍然是经验的：网格、预言机、模糊测试 — 不是定理。
unsafe 访问被排除在外。SuperJ 有一个显式的低层访问表面（SPEC 4.13）。无 UB 声明覆盖的是安全的语言。
没有性能保证。PR-v1 测量性能但不设门；版本化常数自 PR-v2 起设门。
没有升级兼容性声明。对先前发布的往返重放自 PR-v3 起设门。今天的机制是漂移分类。
不是零已知缺陷。签发时，有一个上游缺陷已知并被钉住（MerkleTree.computeTreeNative 静默无操作，上游 #6127）— 在报告中作为红行可见，在边界中解释而不是隐藏。零注意事项的证书才是你该怀疑的那一种。
没有未知之未知的声明。逃逸/arena 文法已在组合下验证封闭并被大量对抗性抽样；“不存在未知的未知”不是任何人能诚实做出的声明，这张证书也不做。

反驳它

自己验证 — 不必信任任何人，包括我们

你的终端

# 10 秒钟的检查 — 声明此刻是否成立？
$ curl -s https://superj.dev/readiness/PR-v1.json

# 真正的检查 — 自己运行每一道门（约 30 分钟，带出处戳）
$ git clone <认证仓库>   # 链接见发布说明
$ python3 scripts/test-report.py
$ python3 tools/readiness-cert.py        # 退出码 0 = 声明今天成立

JSON 里任何非 TRUE 的状态，或超出过期规则的 age_days，都意味着声明不再成立。如果 readiness-cert.py 以非零退出，它会打印失败的条款和被打破的目标 — 那份输出就是反驳。存档它，引用它：证书自己的契约说它必须让位。

事件	会发生什么
检查器每个发布周期重新运行	新证据，相同的文件名。
一个条款变红	公开页面在同一 URL 翻转为 FALSE — 没有可以被忘记的归档步骤。
证据过期（90 天，测试/测量层）	证书渲染为 FALSE，直到重新签发。
被钉住缺陷的工单关闭	钉住翻转为固定契约断言；红行当天变绿。
契约增长（PR-v2 = +C4 ∧ C5，PR-v3 = +C6）	新契约版本，新指针文件；旧的保留自己的状态。

生产可用是一个谓词，
不是一个徽章。