一句话

在 bug 代价最高、测试最够不到的地方选一条性质，用合适的工具（默认 TLA+ 模型检查）形式化验证它，并留下一个项目本地技能让以后的 agent 一键复查。

何时用

• 适合：并发竞态、重试、状态机、解析器、unsafe 代码，测试很难覆盖到出错用例的地方。
• 不适合：普通行为验证（先用 pstack-create-verification-skill）；只想要一次分析不要产物。

怎么用

/create-formal-verification-skill 针对任务租约和重试逻辑，一个任务绝不能并发跑两次

1. 从代码里选目标：代码做出的承诺、破坏会害用户、测试罕至。用户点名就从那里开始。
2. 让问题选工具：事件顺序类用模型检查（TLA+ 默认），逐输入行为用跑在代码上的 verifier，无合适工具就明说并用生成输入测真实代码。
3. 验证一条性质，并展示它在被破坏的变体上真的失败；当前代码已破坏性质就如实报告反例，不削弱性质，不动产品代码。
4. 写项目本地技能：覆盖范围、sync commit、一条命令、如何分辨真 bug 与建模错误；TLA+ 结果要求用 pstack-statechart 读。
5. 照生成的技能跑一遍 scratch 破坏，必须抓到，再恢复原状。

产出

• 一个项目本地 verify 技能（含覆盖记录和 sync commit）加移交说明：验证了什么、工具与边界、发现了什么、不覆盖什么。

要点与坑

• 「从没见它失败过的检查什么都证明不了」是核心规则；技能必须教下一个 agent 在覆盖代码变更后推进 sync commit。
• 配套维护见 pstack-maintain-formal-verification-skill。
• 工具链要装在仓库开发者机器上；TLA+/TLC 首次运行要下载，注意网络。

关联

• 下游：pstack-maintain-formal-verification-skill、pstack-statechart · 同类：pstack-create-verification-skill
• 所属：00-pstack-概览