创建形式化验证技能
测试只检查有人想到要写的用例；形式化验证则在给定范围内检查所有情况：模型中步骤的每一种顺序、有界范围内的每一种输入，或全部输入。本技能会找出仓库中最需要这种验证的部分，验证它的一个性质，并留下一个项目本地技能，使下一个智能体能够依据该性质检查某次改动。写这个技能时，要面向一个在改动过程中、毫无背景地读到它、且从未见过你工作的智能体。用户必须能够信任结果，并在不学习验证语言的情况下据此行动。
从代码中选择目标
依据代码库作答，只向用户询问无法观察到的事项。如果用户指定了某个区域或某个缺陷，就从那里开始。
好的目标是代码做出的一种承诺，一旦被破坏会伤害用户，而测试很少覆盖破坏它的情形。应选择仓库中该类最强目标，而不是最容易验证的目标。
让问题选择工具
选择能以最低成本回答该问题的工具：模型检查器、证明助手、基于 SMT 的验证器或其他工具。事件能否以错误顺序发生，通常适合用针对设计的小模型做模型检查，而在任何语言中，TLA+ 都是这类场景的默认选择。代码本身是否对每种输入都表现正确，例如内存安全、溢出或数据结构不变量，通常适合用直接运行在代码上的验证器。如果该语言没有可运行的验证器，要说明这一点，并用生成的输入测试真实代码，而不是对函数做手工模型。某个性质必须在任意规模下都成立、仅有界不够时，可能需要证明。优先选择仓库开发者能够安装并运行的工具，并向用户说明选择它的原因。
何为好的验证
忠于代码。模型或证明的每一部分都指向评审者能够打开的代码。验证视为不可分割的一步，在代码中也确实是一步。名称取自本仓库。
能够失败。从未见过失败的检查证明不了什么。要在被守护代码的破坏变体上展示每个性质失败，例如移除某项检查或调整步骤顺序。
发现仍是发现。当现有代码破坏该性质时，用代码的术语报告反例。不要为了让检查通过而弱化性质或模型，也不要改动产品代码，除非用户要求。
诚实说明范围。说明验证了什么、在哪些边界和假设下成立、遗漏了什么。一次通过只覆盖该模型或该边界，而非整个系统。
无需工具也能读懂。用各一句平实的话陈述性质和危害。用代码中的词语把反例讲成一段简短步骤序列。
重跑成本低。一条命令、可复现的工具版本、足够短的运行时间，使下一个智能体愿意在每次相关改动上使用它。
与代码保持同步。记录每项检查覆盖的文件和函数，以及你最后一次确认验证仍描述这些代码的提交。该提交之后若被覆盖的代码发生变化，下一个智能体应能看出验证需要重新审视。
生成 verify 技能
编写一个带 frontmatter 的项目本地技能，在其中指明区域并说明何时使用。没有 frontmatter，技能不会注册。仅凭该技能，下一个智能体必须能够判断某次改动是否触及被验证代码、运行检查、区分真实缺陷与建模错误，并在改动属于预期时更新验证。把覆盖记录和同步提交写入技能，并告诉下一个智能体只有在确认验证描述了新提交处的代码后，才能推进同步提交。使用本仓库的真实命令、路径和名词，不留占位符。
如果检查是 TLA+ 模型，告诉下一个智能体用 pstack 的 /statechart 技能读取每个结果。它会把检查器发现的每一处不变量违反，以平实语言表示为最短路径。检查通过时，/statechart 会画出系统在状态间迁移的图表。按名称引用 /statechart。它的命令、选项和文件路径会随版本和机器不同而变化，因此不要把它们复制进生成的技能或其脚本中。
交付前先证明
像下一个智能体那样，按照生成的技能，对真实代码中一个破坏该性质的临时改动执行一遍。它必须捕获该破坏。然后撤销临时改动，确认检查回到初始状态：通过，或仅在你将要报告的发现上失败。从未运行过的 verify 技能只是草稿。如果技能漏掉破坏，或某一步无法运行，应修正技能或验证本身，而不是临时改动。
交付
告诉用户你验证了什么、用了哪个工具及原因、边界、检查用平实语言发现了什么、如何运行、以及它不覆盖什么。只有在找到相近目标时才建议第二个目标。在改动后未重新检查的情况下，指向 /maintain-formal-verification-skill 以让验证重新对齐。