一句话

代码改了而形式化验证没跟上时把它拉回一致：读 sync commit 之后的每个变更，更新模型和性质，重跑，并分辩每个失败是验证漂移还是代码真 bug。

何时用

• 适合：merge、重构、未经 verify 技能的编辑触碰了被验证覆盖的代码之后；「模型还忠于代码吗」。
• 不适合：生成新的验证（用 pstack-create-formal-verification-skill）；用技能内部流程就能处理的单步变更。

怎么用

/maintain-formal-verification-skill

1. 找到跑模型检查器/证明器/代码级 verifier 的项目本地技能，读出性质、覆盖代码、边界、运行命令、sync commit。
2. 原样先跑一遍记录结果；这一步的过只说明旧描述还成立。
3. 逐个 diff 覆盖代码的变更并分类：无影响、验证不再描述代码、承诺有意改变（要引用证据）、承诺可能被破坏。
4. 按代码而不是按结果更新模型；性质只在承诺有意改变时动，并记录新旧措辞和证据。
5. 重跑并判定：过了就人为破坏新代码确认它还能抓到；挂了就逐帧对真实代码重放反例，能复现的是 bug，给出引入它的 commit。
6. 更新技能里的覆盖、命令、边界、sync commit，并按技能流程走一遍确认步骤仍可跑。

产出

• 每个检查一个结论：in sync / updated / bug / blocked；验证更新放在独立改动里，不混产品修复。

要点与坑

• 最危险的是「还在过但描述的是已不存在的代码」；本技能就是为这种情况存在。
• 只编辑验证侧文件，绝不顺手改产品代码；blocked 的检查不推进 sync commit。
• 工具链与 pstack-create-formal-verification-skill 相同（TLA+ 等）；方法可借鉴到任何模型检查工作流。

关联

• 上游：pstack-create-formal-verification-skill · 同类：pstack-maintain-verification-skill · 读结果：pstack-statechart
• 所属：00-pstack-概览