create-formal-verification-skill

创建形式化验证技能

测试会检查人们想到要编写的案例。形式化验证会检查指定范围内的所有案例：模型中的每一种步骤顺序、范围上限内的每个输入，或每个输入。这项技能会找出仓库中最需要验证的部分，验证其中一项属性，并留下项目本地的技能，让下一个 Agent 能据此检查变更。编写技能时，要设想 Agent 第一次读到它时正处于变更过程中，而且从未见过你的工作。用户必须能够信任结果，并据此采取行动，而不必学习验证语言。

根据代码选择目标

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

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

根据问题选择工具

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

优秀技能的特征

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

生成验证技能

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

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

交接前验证

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

交接

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