create-formal-verification-skill

创建形式化验证技能

在 Codex 上，遵循此技能前，请先阅读平台映射，包括其中针对各项技能的说明。

在 GitHub Copilot 上，遵循此技能前，请先阅读平台映射，包括其中针对各项技能的说明。

在 Muse 上，遵循此技能前，请先阅读平台映射，包括其中针对各项技能的说明。

测试只会检查有人想到要编写的用例。形式化验证会检查指定范围内的每一种情况：模型中每一种步骤顺序、界限内的每一个输入，或每一个输入。这项技能会找出仓库中最需要验证的部分，验证它的一项属性，并留下一个项目本地技能，让下一个 Agent 能据此检查改动是否符合该属性。编写技能时，要设想使用者是第一次接触它、正在进行改动的 Agent。用户必须能够信任结果并据此采取行动，而无需学习验证语言。

根据代码选择目标

根据代码库作答，只询问用户无法观察到的信息。如果用户指出了某个区域或错误，就从那里着手。

好的目标是代码所作出的承诺：一旦被破坏就会损害用户，而测试很少覆盖导致问题的情况。选择仓库中最有价值的目标，而不是最容易验证的目标。

根据问题选择工具

选择能以最低成本回答问题的工具：模型检查器、证明助手、SMT 支持的验证器或其他工具。若问题是事件是否可能以错误顺序发生，通常适合用针对小型设计模型的模型检查器；任何语言都默认优先考虑 TLA+。若问题是代码本身对每个输入的行为是否正确，例如内存安全、溢出或数据结构不变量，通常适合使用直接运行于代码上的验证器。如果没有适用于该语言的验证器，请如实说明，并使用生成的输入测试实际代码，而不是为函数手写模型。如果某项属性必须在任何规模下都成立，有限界限不足以证明它，则可能需要证明。优先选择仓库开发者能够安装和运行的工具，并向用户说明选择理由。

优秀技能的标准

• 忠实于代码。 模型或证明的每个部分都对应到审查者可以打开查看的代码。验证过程中视为一个不可分割步骤的内容，在代码中也必须是一个不可分割步骤。名称应取自此仓库。
• 能够失败。 从未见过失败的检查，证明不了任何事。应展示每项属性在其所保护代码的错误变体上失败，例如删除一项检查或调换步骤顺序。
• 如实报告发现。 如果当前代码违反了属性，应使用代码中的术语报告问题及反例。不要弱化属性或模型直到检查通过，也不要修改产品代码，除非用户提出要求。
• 明确说明范围。 说明验证了什么、使用了哪些界限和假设，以及遗漏了什么。通过检查只适用于模型或界限范围内，不代表整个系统。
• 无需使用工具也能读懂。 分别用一句通俗的话说明属性及其可能造成的危害。用代码中的术语，以简短的步骤序列描述反例。
• 重新运行成本低。 提供一条命令、可复现的工具版本，以及足够短的运行时间，让下一个 Agent 能在每次相关改动后都运行检查。
• 与代码保持同步。 记录每项检查覆盖的文件和函数，以及最近一次确认验证仍准确描述这些内容时的提交。覆盖的代码在该提交之后发生变化时，下一个 Agent 就能看出验证需要重新检查。

生成形式化验证技能

编写一个项目本地技能，并添加前置元数据，说明其针对的领域以及何时使用。技能名称应体现该领域，绝不要使用 verify 或 verify- 前缀，因为驱动技能 /create-verification-skill 会使用这些名称。在 Claude Code 中，技能应位于 .claude/skills/<area>/SKILL.md。没有前置元数据，技能就无法注册。仅凭该技能，下一位 Agent 必须能够判断某项更改是否影响已验证的代码、运行检查、区分真正的错误与建模错误，并在有意更改时更新验证。将覆盖范围记录和同步提交写入技能，并告知下一位 Agent：只有在确认验证内容与新提交中的代码相符后，才能将同步提交前移。使用此仓库的实际命令、路径和术语，不要留下任何占位符。

如果检查使用 TLA+ 模型，请告知下一位 Agent 使用 pstack 的 /statechart 技能阅读每项结果。它会用通俗语言展示检查器发现的每个不变量违规，以及到达该违规的最短路径。检查通过时，/statechart 会绘制系统在各状态之间转换的图表。请按名称提及 /statechart。它的命令、选项和文件路径会随版本和机器而变化，因此不要将其中任何内容复制到生成的技能或其脚本中。

交接前证明有效

像下一位 Agent 一样，完整执行一次生成的技能：在临时更改中破坏真实代码里的目标性质。它必须能够发现这个破坏。然后撤销临时更改，并确认检查恢复到原先状态：通过，或仅因你将报告的问题而失败。未经实际运行的形式化验证技能只是草稿。如果技能未能发现破坏，或某个步骤无法运行，请修复技能或验证，而不是修改临时更改。

交接

告知用户你验证了什么、使用了哪种工具以及原因、验证范围、检查以通俗语言发现了什么、如何运行检查，以及检查未覆盖什么。只有发现了紧密相关的目标时，才建议验证第二个目标。若更改后未重新检查，请引导用户使用 /maintain-formal-verification-skill 使验证恢复一致。