怎么证明系统是安全的？

“证明安全”在不同语境下含义不同，需要先区分三个层次：物理意义上的安全（状态不越过安全边界）、时序逻辑意义上的安全（任务全程满足形式化约束规约），以及可审计意义上的安全（有机器可读的证据链可供事后验证）。EICPS 对三个层次都有答案。

物理安全：CBF 前向不变性

控制屏障函数定义安全集 $\mathcal{C} = \{x : h(x) \geq 0\}$，其中 $h(x)$ 是与具体场景相关的安全函数（如人员安全距离、关节力矩上限、工作空间边界）。

CBF 控制律在每个 1ms 控制周期内强制：

数学上可以证明：只要初始状态 $x_0 \in \mathcal{C}$，系统在全时域内不会逸出 $\mathcal{C}$。这个保证是确定性的，不依赖 AI 的正确性，不依赖预测视域的长短。当 Brain 层产生幻觉或错误指令时，CBF 修正控制输入——这是”脊髓反射弧”的工程实现，安全优先于执行指令。

时序逻辑安全：STL 在线验证

任务开始前，将场景特定约束形式化为 STL 规约 $\varphi$，例如：

• $\square_{[0,T]} h_{dist}(x) \geq d_{safe}$（全程保持安全距离）
• $\diamond_{[0,5]} \text{reach}(x, \text{target})$（5 秒内到达目标）

Spine 层在 1kHz 下持续计算鲁棒度 $\rho(t)$——它不只是是/否判断，而是量化”约束满足余量”的实数：

• $\rho > \rho_{warn}$：正常执行
• $0 < \rho \leq \rho_{warn}$：预警，触发保守行为
• $\rho \leq 0$：约束违反，强制 Jump 到 FAILSAFE 模态

STL 和 CBF 的分工：CBF 负责”当下不越界”（空间不变性），STL 负责”全程满足规约”（时序逻辑），两者共同构成 EICPS 的双层安全保障。

可审计安全：EvidencePack

任务结束后，系统自动生成 EvidencePack $\{P, A, x_{act}, \varphi, \rho^*, v\}$，将规约、全程最小鲁棒度、最终判决与实际轨迹一起封装为结构化证据，写入 Firestore。

审计人员无需重跑仿真，只需检查六元组：$\rho^* > 0$ 且 $v = \text{PASS}$，则该次任务在形式化层面合规。安全声明从”系统看起来没有出问题”变成”这是可机械检验的证据”。

需要诚实说明的局限

两条安全路径都是”下游保证”——它们保证 AI 的错误输出不会穿透到物理执行层，但它们本身不能保证 AI 不产生错误输出。

此外，CBF 的有效性依赖 $h(x)$ 的正确设计。若安全函数定义不完整（遗漏了某类碰撞场景），CBF 对该场景无效。安全性证明的质量取决于安全函数定义的完整性，后者是场景分析的工程责任，不是控制理论自动保证的。

→ 实时安全监控（CBF） · 安全约束验证（STL） · 场景验证