条件命题
形式化保证本质上都是条件命题：
A（假设集）：运行域成立、模型误差和感知误差有界、执行器有效、通信满足时延/完整性假设、扰动不超界、不存在未建模的成功攻击等。
P（保证性质）：在这些假设成立时，安全距离不被突破、任务顺序合规等性质成立。
它不是对任何环境、故障、攻击和任务的无条件保证。宣称”系统经过形式化验证所以安全”而不给出 A，是把条件命题冒充无条件命题——这正是本站废止无条件可靠类表述的原因（见修订说明第 6 条）。
可以追求的”确定性”在哪里
可以把 100% 放在受控软件门控逻辑上，而不能放在所有现场任务的成功率上：
只要许可、对象身份、关键状态或安全条件没有被明确验证为真，系统就不进入自主物理执行。
但这只是安全门控性质——永不行动的系统也能平凡满足。因此必须同时考察有效任务的通过与完成能力，见 UVR / FRR 成对指标。
A 被违反时发生什么
条件化保证的完整性还要求：假设被违反时系统行为仍是确定的。
| A 中被违反的假设 | 检测方式 | 确定行为 |
|---|---|---|
| 输入超出 ODD | 域外检测 / 置信度校准 | UNKNOWN → 拒绝或复核 |
| 感知误差超界 | 覆盖率监控、一致性校验 | 降级或停止 |
| 通信时延/完整性失效 | 看门狗、心跳、签名校验 | 安全停止 |
| 执行器异常 | 状态反馈残差 | FAILSAFE 接管 |
| 规范版本失配 | ES_adm 版本校验 | 拒绝执行 |
“检测不到假设违反”本身也是假设的一部分——这就是为什么假设集清单必须显式列出检测机制的覆盖边界。