什么是形式化安全验证？理论来龙去脉

一句话回答

形式化安全验证是用数学证明而非统计测试来保证系统安全性的方法体系。它不回答”系统在 99.9% 的情况下是安全的”，而是回答”在建模假设成立的前提下，系统在所有情况下都满足安全规约”。

两条独立的理论河流

这套方法不是单一来源，而是两条在不同时代独立发展的理论河流在 21 世纪初汇合的产物。

第一条河流：程序逻辑与模型检验

出发点：怎么证明一个程序是正确的？

1960 年代，计算机科学家开始追问这个问题。Floyd（1967）和 Hoare（1969）给出了第一个答案——Hoare 逻辑，用三元组 $\{P\}\, C\, \{Q\}$ 描述程序语义：若执行前满足前置条件 $P$，执行后一定满足后置条件 $Q$。这是”形式化”的本质：把自然语言的正确性要求翻译成数学断言，再用逻辑推导验证。

Hoare 逻辑处理的是静态属性（执行结束后的状态）。但真实系统持续运行，人们更关心的是：在整个运行过程中，某个坏事会不会发生？ 这引出了时序逻辑。Pnueli（1977，图灵奖）提出线性时序逻辑（LTL），引入了”始终”（$\square$）、“最终”（$\diamond$）、“直到”（$\mathcal{U}$）算子，可以精确描述随时间展开的行为属性。

Clarke、Emerson、Sifakis（1981–1982，2007 年共同获图灵奖）发明了模型检验（Model Checking）：给定有限状态系统和时序逻辑规约，自动枚举所有可达状态，机械地判断规约是否被满足。这是第一次把形式化验证变成可以自动运行的算法。

根本限制：模型检验只能处理有限状态系统。物理世界中的机器人状态空间是连续的，有无穷多个状态，无法枚举。

第二条河流：Lyapunov 稳定性与不变集理论

出发点：怎么证明系统不会发散？

Lyapunov（1892）的核心思想是构造一个能量型函数 $V(x)$：如果 $V$ 沿系统轨迹单调递减，系统就不会逃离平衡点附近。这是”证明好事持续发生（稳定性）“的数学方法。

Nagumo（1942）则在处理另一个方向：怎么证明系统状态永远不离开某个集合？ 他给出了几何条件：设安全集 $C = \{x : h(x) \geq 0\}$，$C$ 在动力学 $\dot{x} = f(x)$ 下正向不变的充要条件是——在边界 $\partial C$ 上，向量场不能指向 $C$ 的外部：

$h(x) = 0 \;\Rightarrow\; \nabla h(x) \cdot f(x) \geq 0$

这是”证明坏事永远不发生”的数学基础。Nagumo 定理此后在控制论里发展了几十年，但长期停留在分析层面——只能判断给定集合是否不变，没有系统方法在有控制输入时主动维持安全集。

两条河流的汇合

汇合发生在 2000 年代到 2010 年代，三个关键进展将两条线索接在了一起。

混合系统（Hybrid Systems） 是第一个桥梁。Alur、Henzinger 等人（1990 年代）提出混合自动机，把连续动力学（微分方程）和离散状态切换（有限状态机）统一在一个框架里，使得模型检验的思想可以部分扩展到连续系统——对连续状态做可达集分析，取代有限状态枚举。Goebel、Sanfelice & Teel（2012）进一步发展了 Flow-Jump 框架，提供了处理模态切换的严格数学工具。

信号时序逻辑（STL） 是 Maler & Nickovic（2004）针对连续时间信号对 LTL 的扩展。STL 的关键创新是鲁棒度 $\rho(\varphi, x, t)$——一个实数，量化当前轨迹距离违反规约有多远：正值代表满足，负值代表违反，绝对值代表安全余量。例如规约：

$\varphi = \square_{[0,T]}\; d(x(t),\; \mathcal{O}) \geq d_\mathrm{safe}$

表达”在整个时段内，与障碍物距离始终不小于安全间距”，而 $\rho(\varphi, x, t)$ 实时告诉你距离违反规约还有多少余量。这把逻辑判断（是/否）变成了可以在控制律中使用的连续量。

控制屏障函数（CBF） 是 Ames、Grizzle、Tabuada 等人（关键论文 2014–2017）的贡献，是执行层的核心工具。他们把 Nagumo 条件推广到有控制输入的情形，并允许一定的”松弛”：

$\dot{h}(x, u) \geq -\alpha(h(x))$

其中 $\alpha$ 是 class-K 函数（严格递增、$\alpha(0)=0$）。这个条件允许 $h$ 在安全集内部适度下降，只要下降速率与 $h$ 当前值成比例，就能保证 $h$ 不会穿越零点进入不安全区域。

将 Nagumo 条件转化为约束，得到实时可解的二次规划（QP）：

$u^* = \arg\min_{u} \|u - u_\mathrm{ref}\|^2 \quad \text{s.t.} \quad \frac{\partial h}{\partial x} f(x, u) + \alpha(h(x)) \geq 0$

$u_\mathrm{ref}$ 是来自 AI 或规划器的参考指令，$u^*$ 是经安全过滤的最终指令——在对 $u_\mathrm{ref}$ 最小修改的前提下，保证安全集不被逸出。这个 QP 在现代处理器上约 0.1–1 ms 可解，满足实时控制频率要求。

认识论地位：与测试的根本区别

形式化验证的结论是条件性的——“在建模假设成立的前提下”。如果物理建模有误差（比如简化了某些动力学），证明对模型仍然成立，对真实系统的覆盖程度取决于模型误差的大小。这就是为什么形式化验证需要与鲁棒控制和不确定性量化同时使用。

对 EICPS 具体说：CBF 证明的是”在 EKF 状态估计误差在已知范围内、且动力学建模正确的前提下，机械臂末端不会进入禁止区域”。EvidencePack 把这个证明的条件和结论都记录下来，使安全性可审计，而不只是声称”系统是安全的”。

时间线

在 EICPS 中的位置

STL 是 Brain 层向 Spine 层传递安全规约的语言（接口 A 的内容），$\rho$ 是 Spine 层实时监控的信号。CBF 是 Spine 层的执行过滤器，在 1 kHz 频率下对 AI 指令做最小修正。EvidencePack 把每次任务的 $\{P, A, x_{act}, \varphi, \rho^*, v\}$ 打包，将”安全性已被验证”从声明变为可追溯的数学事实。

形式化安全验证是整个 EICPS 框架之所以能从遥操作走向自主操作的数学支柱——它替代了遥操作中操作员实时判断这一角色，承担了 Human-on-the-Loop 架构下原本由人承担的安全兜底职能。

→ 什么是 Safe Autonomy？EICPS 与它的关系 · 旧方案形式化验证为什么是结构性失败？ · 什么是 EvidencePack？ · 如何证明安全性？