形式化验证的可行性由什么决定？——规范闭合性与结构性失败的对偶

一句话回答

不取决于工具，不取决于算力，取决于问题的数学前提是否成立。 EICPS 系列工作中散落的三个结论——规范闭合性（Paper-01）、结构性失败（Q-24）、分离式设计（Q-26）——其实是同一个方法论命题的三个侧面：“让形式化成为可能”本身就是研究对象。

对偶的两面

正面（Paper-01）：找到使前提成立的领域属性。 开放世界中，语义覆盖只能是统计下界 $\mathrm{SEC} \geq 1-\delta$，且 $\delta > 0$ 不可消除。Paper-01 识别出电力作业规程的规范闭合性（文件枚举完备性使任务分布支撑集有限可枚举），从而把开放世界的统计问题转化为闭合域的形式化问题，SEC 升级为确定性等式 $=1$。形式化在这里变得可能，不是因为换了更强的工具，而是因为发现了一个使数学前提成立的领域属性。

反面（Q-24）：诊断使前提坍塌的物理结构。 旧作业方案中，机械臂与振动导线力学耦合，状态空间被 PDE 拖入无穷维（$\mathbf{w}(\cdot,t) \in [L^2([0,L])]^4$），CBF 李导数与 STL 鲁棒度的有限维代数前提同时坍塌。形式化在这里必然失败，不是因为工具不够好或算力不够强——换任何求解器都无济于事，因为前提不成立。

两面共享同一个判据结构：

$\text{形式化可行} \iff \text{数学前提成立（有限可枚举 / 有限维 / 解析 / 实时可解）}$

第三元：改造问题使前提成立

对偶之外还有第三种姿态（Q-26）：当前提天然不成立时，改造问题本身。分离式设计（定位锁紧 + 工具独立操作）不是优化旧方案，而是重构作业结构使每个阶段回到有限维解析 ODE——主动创造形式化可处理性的三个条件。这与 Paper-01 的”发现”形成互补：一个是识别世界已有的良好属性，一个是通过设计把世界改造成具有良好属性。

三种姿态的方法论总表

三种姿态的共同点：把注意力从”用什么工具验证”转移到”什么条件下验证是可能的”——这是元层次的问题，也是 EICPS 区别于”拿现成工具套场景”类工作的方法论标志。

认识论根基

这个对偶之所以成立，根源在形式化验证结论的条件性全称结构（→ Q-28）：形式化验证证明的是”在建模假设成立的前提下，系统在所有情况下满足规约”。前提是结论的一部分——所以研究前提（何时成立、何时坍塌、如何创造）与研究工具同等重要，甚至更重要：工具是文献里现成的（Nagumo→Ames，Pnueli→Maler），前提工程才是领域工作者的主战场。

对后续工作的意义

这个三元结构是 P-09 论文（形式化可处理性驱动的硬件设计）引言的天然框架：Paper-01 已发表”识别”一元，P-09 补齐”诊断 + 改造”两元，合起来是一个完整的方法论主张。它同时划定了主张的边界（→ 专著 §15.5.3）：分离式设计是”当前唯一经验证”而非”唯一可能”的改造方案——改造姿态的解空间刻画本身是开放问题。

→ Q-24 结构性失败 · Q-26 分离式设计的数学必要性 · Q-28 形式化验证的来龙去脉 · Paper-01 语义覆盖