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