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