create-formal-verification-skill

创建形式化验证技能

在 Claude Code 中，每个会话开始时，请先阅读Claude Code 适配器，再使用此技能。它会将 pstack 技能中的 Cursor 名称映射到 Claude Code。

测试检查的是人们想到要编写的用例。形式化验证会检查既定范围内的所有情况：模型中的每种步骤顺序、边界以内的每种输入，或所有输入。此技能会在代码库中找到最需要验证的部分，验证它的一项属性，并创建一个项目本地技能，让下一个 Agent 能据此检查变更是否满足该属性。编写此技能时，要设想使用者是一个对你的工作一无所知、在变更过程中临时打开技能阅读的 Agent。用户应该能够信任验证结果，并据此采取行动，而无需学习验证语言。

根据代码选择目标

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

好的目标是代码所作出的承诺：一旦失守就会损害用户，而测试又很少覆盖到出错的情况。选择代码库中最重要的此类目标，而非最容易验证的目标。

根据问题选择工具

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

优质验证的标准

• 忠实于代码。 模型或证明的每个部分都应能对应到审阅者可以查看的代码。验证中视为一个不可分割步骤的操作，在代码中也应是一个不可分割步骤。使用本代码库中的名称。
• 确实可能失败。 如果从未见过检查失败，它就证明不了任何东西。用该检查所保护代码的一个错误变体，展示每项属性都会失败，例如删除一个检查或调换步骤顺序。
• 如实报告发现。 如果当前代码违反了该属性，请使用代码中的术语，并附上反例。不要削弱属性或模型来让它通过；除非用户要求，否则不要更改产品代码。
• 如实说明范围。 说明验证了什么、采用了哪些边界和假设，以及排除了哪些内容。通过结果只适用于该模型或边界，不代表整个系统。
• 无需工具也易于理解。 分别用一句通俗的话说明属性和违反它会造成的危害。用代码中的术语，简要描述反例的步骤序列。
• 重新运行成本低。 提供一条命令、可复现的工具版本，并确保运行时间足够短，让下一个 Agent 会在每次相关变更时使用它。
• 与代码同步维护。 记录每项检查覆盖的文件和函数，以及最近一次确认验证仍能准确描述这些代码时的提交。覆盖的代码在该提交之后发生变更时，下一个 Agent 应能看出需要重新检查验证。

生成验证技能

编写一个项目本地技能，包含说明适用领域及使用时机的 frontmatter。没有 frontmatter，技能就永远不会注册。仅凭该技能，下一个 Agent 就必须能够判断某项更改是否涉及已验证的代码、运行检查、区分真实 bug 与建模错误，并在更改符合预期时更新验证。将覆盖记录和同步提交写入技能，并告知下一个 Agent：只有在确认验证准确描述新提交中的代码后，才能推进同步提交。使用此仓库中的真实命令、路径和术语，不留任何占位符。

如果检查使用的是 TLA+ 模型，告诉下一个 Agent 使用 pstack 的 /statechart 技能阅读每项结果。它会用通俗语言展示检查器发现的每个不变量违规的最短路径，以及哪些违规已被某项更改修复。检查通过时，/statechart 会绘制系统状态转换图。请直接使用 /statechart 这个名称。其命令、选项和文件路径会随版本及机器而变化，因此不要将其中任何一项复制到生成的技能或脚本中。

交接前验证

按照生成的技能，以接手工作的下一个 Agent 的身份，在真实代码中进行一项会破坏该属性的临时更改，并完整执行一次技能流程。技能必须能够发现问题。然后撤销临时更改，并确认检查恢复到原先状态：要么通过，要么只剩下你将要报告的发现。如果验证技能从未运行过，它就只是草稿。如果技能未能发现问题，或某个步骤无法运行，就修复技能或验证，而不是修改临时更改。

交接

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