形式化验证闭环

本章建立EICPS的形式化验证闭环。形式证据链不是事后审计工具，而是系统运行的内置结构：每次执行都同步生成可机器验证的证据包，使系统的每个决策在事后都可被独立追溯和核查。

10.1 形式证据链的设计原则

10.1.1 为什么需要形式证据链

安全关键系统的可靠性不仅要求系统”做对”，还要求系统”能证明自己做对”。这一要求来自两个独立的动机。事故调查的可追溯性：带电作业发生安全事故时，监管机构和工程师需要重现事故过程，精确定位每个决策节点（LLM规划的输出是什么？CBF在何时激活？传感器数据在何时开始出现异常？），而这些信息在事后无法从结果反推，必须在执行过程中实时记录。形式验证的可执行性：第四部分的三环验证（V-SEM/V-PLN/V-SAF）需要在真实执行数据上运行——没有完整的执行记录，验证就无法进行。形式证据链是验证链运行的数据基础。

形式证据链的设计原则是最小完备性：记录足以重现所有形式验证所需的信息，不记录超出这一需求的冗余数据（防止存储开销失控）。

10.1.2 证据包的结构定义

每次任务执行对应一个形式证据包（Formal Evidence Package，FEP），包含以下字段：

• 执行标识：任务ID、执行时间戳、机器人ID、操作员ID（可选）
• Brain层记录：原始任务描述 $\tau$、LLM生成的ESTL描述、编译后的STL规约包 $\Phi$、HTN分解树（包含多轮对话历史，若有）
• Spine层记录：每个监控周期（100ms）的STL鲁棒度值序列 $\{\rho_i(t)\}$、安全仲裁触发事件（时间戳、触发原因、仲裁输出）
• Body层记录：关键时刻（任务阶段切换、安全仲裁触发前后）的状态估计 $\hat{T}$、CBF活动标志序列、EKF协方差矩阵摘要
• 执行结果：最终任务状态（成功/失败/超时）、规约满足摘要（每条规约的最终鲁棒度）

FEP的存储格式采用结构化JSON（便于机器解析），每次执行后自动上传到云端证据库（Firebase Firestore），并生成本地备份。

10.1.3 证据的不可篡改性保证

形式证据链的可信性依赖证据的不可篡改性：记录的数据必须反映系统的真实行为，而不能被事后修改。EICPS通过两个机制保证不可篡改性：实时流式写入（证据数据在生成时立即写入，而非在执行结束后批量上传，防止执行中断导致的数据丢失，同时防止”选择性记录”）；哈希链接（每个证据记录的哈希值链接到下一条记录，类似区块链的内容验证机制，任何事后修改都会破坏哈希链）。在第13章V-SAF验证中，证据链的完整性校验是形式验证流程的第一步。

10.2 Brain层证据的生成与格式

10.2.1 LLM推理过程的完整记录

Brain层证据的核心是LLM推理过程的完整记录，而非仅仅记录最终输出。完整记录包括：每次LLM调用的输入提示（含系统提示、任务描述、ESTL语法指导）、LLM的原始输出文本（在ESTL解析之前）、ESTL语法解析结果（成功解析的ESTL对象或解析错误信息）、规约库查询日志（查询了哪些词汇条目、返回了哪些规约模板）、参数实例化日志（每个参数从哪个数据源取得什么值）。

这一完整记录使V-PLN验证（第12章）得以实施：通过分析”LLM原始输出”与”最终执行规约”之间的差异，可以精确量化LLM幻觉（生成了不合规的ESTL描述）的发生频率和性质。

10.2.2 ESTL编译的符号证明

ESTL到STL的编译是一个形式化转换过程，理想情况下应伴随符号编译证明：对于每次编译，系统生成一个证明记录，说明编译结果在何种意义上等价于ESTL描述的意图（根据编译规则§9.1.3）。当前实现中，编译证明采用轻量化方式：编译器在每次翻译时标注所应用的编译规则（按规则编号索引），并对生成的STL公式进行语法验证（确保公式是格式良好的STL），而非完整的语义等价性证明。完整的语义证明留作未来工作（需要依赖Coq或Lean等定理证明器的集成）。

10.2.3 HTN分解树的序列化与可视化

HTN分解树以有向无环图（DAG）形式序列化到证据包中，其中每个节点记录：任务名称（ESTL中的任务ID）、方法选择（使用了方法库中的哪个方法）、前置条件评估结果（满足/不满足，以及当时的相关状态值）。这一序列化表示支持事后的交互式可视化——通过网站的证据查看工具（第10.4节），可以将HTN分解树以树状图形式渲染，直观展示任务分解的每个步骤。

10.3 Spine/Body层证据的连续记录

10.3.1 STL鲁棒度轨迹的压缩存储

Spine层的STL鲁棒度评估以100ms为周期持续记录，一次典型的带电作业任务（30分钟）会产生约18,000条鲁棒度记录（每条规约一条）。直接存储所有记录会占用大量空间，EICPS采用分段线性压缩策略：在鲁棒度变化平稳的阶段（斜率小于阈值），以较低频率记录（每10条保留1条）；在鲁棒度快速变化的阶段（接近安全边界或触发预警），以全分辨率记录。压缩比通常在5-10倍，同时保留所有关键事件（鲁棒度极小值、预警触发点）的完整记录。

10.3.2 CBF活动事件的事件驱动记录

与连续记录的STL鲁棒度不同，CBF活动事件采用事件驱动记录：只在CBF约束状态发生变化时（从不活动到活动，或从活动到不活动）记录一条事件，记录内容包括时间戳、触发原因（哪个障碍物的 $h$ 值降至阈值）、仲裁前的名义控制输入 $u_{\mathrm{nom}}$、仲裁后的安全控制输入 $u^*$、QP求解时间。事件驱动记录的存储效率远高于固定频率记录：在典型任务中，CBF活动事件的数量在几十到几百个量级，而非持续记录的数万条。

10.3.3 EKF状态估计的关键时刻快照

Body层的EKF状态估计以10ms为周期运行，存储所有10ms级记录不现实（一次任务约180,000条）。EICPS采用关键时刻快照策略：在任务阶段切换时刻、CBF仲裁触发前后（各保存3秒窗口的密集记录）、STL预警时刻、以及每分钟的定期快照时，存储完整的EKF状态（均值 $\hat{T}$、协方差 $P$）。关键时刻快照确保了在需要详细分析的时刻（安全事件附近）有足够的数据分辨率，同时将非关键阶段的存储开销降至最低。

10.4 证据链的访问与验证工具

10.4.1 证据查看器：结构化可视化界面

EICPS提供基于Web的证据查看工具，允许工程师和审计员查看特定执行的完整证据包。查看器的核心功能包括：时间轴视图（将Brain层、Spine层、Body层的事件在同一时间轴上可视化，直观显示三层的协同模式）、STL鲁棒度图（绘制每条规约的鲁棒度随时间的变化曲线，高亮预警和仲裁触发事件）、HTN树视图（交互式展示任务分解结构，可点击每个节点查看详细信息）、状态轨迹3D视图（在SE(3)空间中可视化机械臂末端执行器的轨迹，叠加安全集边界）。

10.4.2 自动化验证流水线

形式证据链支持自动化批量验证：给定一批执行记录（FEP集合），验证流水线自动运行V-SEM/V-PLN/V-SAF三环验证（第11-13章），生成验证报告。验证流水线是第四部分的执行基础设施——三环验证不是手工进行的，而是在形式证据链数据上自动运行的程序。验证结果（每条执行记录通过/未通过哪些验证项目）被追加到对应的FEP中，形成”执行记录 + 验证结果”的完整档案。

10.4.3 证据链与监管报告的自动生成

形式证据链可以自动生成符合监管要求的作业报告：给定一次执行的FEP，系统提取关键信息（执行时间、操作类型、安全仲裁次数、最终结果），按照电力行业作业报告格式（GB/T规范）自动填充报告模板。自动生成的报告与人工填写报告的主要差异在于数字来源的精确性：报告中的”安全距离最小值”、“任务完成时间”等数据直接来自证据链中的数字记录，而非操作员的主观印象，消除了人工填写报告的主观性。

写作占位 — 与现有电力行业作业报告系统（PMIS）的集成方案

10.5 第三部分的完成：从框架到系统

10.5.1 三层架构作为数学理论的工程实例

第三部分（第7-10章）建立的三层架构，是第二部分数学框架在工程系统中的实例化。对应关系逐一落实：三流形乘积结构 $\mathcal{M}_{\mathrm{phy}} \times \mathcal{M}_{\mathrm{sem}} \times \mathcal{M}_{\mathrm{data}}$ 对应Body/Brain/Spine三层各自的状态管理；Flow-Jump混合系统 $\mathcal{H}$ 对应Spine层的仲裁逻辑和三层的事件驱动交互；SE(3)几何对应Body层的EKF和控制器实现；规范闭合性对应Brain层的词汇约束和规约库设计。数学框架的每个关键概念在工程实现中都有精确对应，而非模糊的”参考借鉴”。

10.5.2 形式证据链作为架构的内生属性

形式证据链不是系统运行之后附加的审计功能，而是EICPS架构的内生属性：三层架构的每个接口协议（§7.5.1）都以”可记录性”作为设计约束，STL规约的精确语义使得鲁棒度的数字记录是自然的，ESTL编译过程的符号化使得编译历史的完整保存是可行的，EKF状态估计的概率框架使得不确定性的数字化记录是内置的。系统不需要为可追溯性额外付出特别的架构代价——可追溯性是形式化工具选型的自然产物。

10.5.3 第四部分的接续：验证链的输入

第三部分提供了两样东西作为第四部分（验证链）的输入：形式化的系统架构（Brain/Spine/Body三层的精确接口定义，使V-SEM/V-PLN/V-SAF验证有明确的验证对象）和形式证据链（每次执行的完整可机器验证记录，是V-SEM/V-PLN/V-SAF验证的数据来源）。第四部分不是对第三部分系统的外部审查，而是利用系统内生证据对系统自身属性的内部证明——这是EICPS框架中”形式化自主”概念的完整实现：系统不仅自主执行，还自主验证自身的执行质量。

第三部分在此完成。第四部分将把Brain层（V-SEM语义验证）、Brain层输出质量（V-PLN规划质量）、Body层安全（V-SAF执行安全）逐一通过形式化验证链量化和证明。

参考文献

写作占位 — 本章参考文献列表（随正文写作逐步完善）