create-formal-verification-skill

创建形式化验证技能

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

根据代码选择目标

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

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

根据问题选择工具

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

优秀技能的特征

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

生成 verify skill

编写一个项目本地的 skill，添加 frontmatter，注明其覆盖范围以及何时使用。没有 frontmatter，skill 就永远不会注册。仅凭这个 skill，下一个 Agent 就必须能判断某项更改是否涉及已验证的代码、运行检查、区分真正的 bug 和建模错误，并在有意更改时更新验证。将覆盖记录和同步提交写入 skill，并告知下一个 Agent：只有在确认验证描述的是新提交中的代码后，才能将同步提交前移。使用此仓库实际的命令、路径和术语，不要留下任何占位符。

如果检查使用的是 TLA+ 模型，告诉下一个 Agent 使用 pstack statechart skill 阅读每项结果。它会以通俗文字展示检查器发现的每项不变量违反情况及其最短路径，并指出其中哪些违反情况已被某项更改修复。检查通过时，statechart skill 会绘制系统在各状态之间转换的图表。请按名称引用 statechart skill。它的命令、选项和文件路径会随版本和机器而变化，因此不要将其中任何内容复制到生成的 skill 或其脚本中。

交接前先验证

按照生成的 skill，以接手的 Agent 会采用的方式，在真实代码中做一项会破坏该属性的临时更改，并完整执行一次。它必须能发现问题。然后撤销临时更改，并确认检查恢复到原先状态：通过，或仅对你将要报告的问题仍然失败。从未运行过的 verify skill 只是草稿。如果 skill 未能发现问题，或某个步骤无法运行，就修复 skill 或验证，而不是临时更改。

交接

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