定义
η_cert : (Clause, Interpretation) → SignedConstraintArtifact
规范编译的原子产物。它的可信性来自条款级专家评审、签署、测试和版本治理，而不来自本体或 CBF 的自动证明——这是与”自动形式化”路线的根本区别。
最低字段要求
| 编译产物字段 | 最低要求 | 责任与验证 |
|---|---|---|
| 来源与适用性 | 标准号、版本、条款、上下文、适用对象/工况 | 规范专家确认 |
| 解释与形式化 | 术语绑定、条件、义务/禁止、例外、变量、单位 | 领域专家与形式化人员双审 |
| 执行映射 | 规则、HTN/BT 前置条件、连续约束、FAILSAFE | 机器人/控制人员确认 |
| 测试与发布 | 正例、反例、边界例、域外例、签名、有效期 | 独立验证后版本化发布 |
| 变更与证据 | 影响分析、撤销/替换关系、运行日志与结果 | 全链可追溯、可复盘 |
缺任何一栏，产物不得发布。
签署协议要点
- 条款级双审：领域专家审解释的忠实性，形式化人员审规则的可执行性。单人不能同时担任两角色。
- 测试用例四类齐备：正例（应许可）、反例（应拒绝）、边界例（临界条件）、域外例（应 UNKNOWN）。域外例常被遗漏，但它验证的正是默认拒绝机制。
- 有效期与版本：标准修订、设备变更、运行域调整都触发影响分析；被替换的产物保留撤销记录，运行日志可回指历史版本。
- 回归测试：产物库任何变更后，全部已发布产物的测试用例重跑。
感知量不得当真值使用
约束进入运行时后，估计量必须带误差处理。以安全距离为例，距离估计 d̂(x)、感知误差上界 ε_perc（覆盖率 1−α 的统计上界）下，采用鲁棒裕度：
- 适用域：可信传感通道覆盖范围内
- 假设：ε_perc 为覆盖率 1−α 的统计上界；最坏端到端时延已计入
- 失效条件：分布外输入（夜间/雨雾/新塔型）使覆盖率假设不成立
- 证据状态：【建模约定】，未经现场标定
任何公式在本站发布必须同页给出以上四项（W1.0 治理规则 2.3）。