用途
该技能面向“测试覆盖不到、但一旦出错代价极高”的代码区域，为其建立形式化验证。测试只检查有人想到要写的用例，而形式化验证在给定范围内检查所有情况：模型中步骤的每一种顺序、有界范围内的每一个输入，或全部输入。该技能会找出仓库中最值得验证的部分，验证其中一条性质，并留下一个项目本地技能，使后续智能体能够针对该性质检查改动。
主要能力
- 从代码本身选择验证目标：优先选择代码做出的承诺，且该承诺被破坏会伤害用户、测试又很少覆盖到破坏情形。选择仓库中最强的此类目标，而非最容易验证的目标。
- 让问题决定工具：在模型检查器、证明助手、SMT 验证器或其他工具中选择成本最低者。事件是否可能以坏顺序发生，通常适合对设计的小模型使用模型检查器，TLA+ 是任何语言下的默认选择；代码本身是否对每个输入都表现正确（如内存安全、溢出、数据结构不变量），通常适合在代码上运行的验证器。若该语言没有可运行的验证器，应如实说明，并用生成的输入测试真实代码，而不是手工建立函数模型。必须在任意规模成立、有界不够的性质可能需要证明。优先选择仓库开发者能安装并运行的工具，并向用户说明选择理由。
- 生成项目本地技能：创建真实目录
.agents/skills/<name>/及相对符号链接.claude/skills/<name>->../../.agents/skills/<name>，使 Claude Code 与 Codex 线程都能加载，并提交两者。技能需带 frontmatter 指明区域与使用时机，否则不会注册。 - 交付前自证：按后续智能体的方式，用一处会破坏该性质的临时改动运行生成的技能，必须能捕获该破坏；随后撤销临时改动，确认检查回到初始状态。
使用方式
技能会从代码库中寻找答案，只向用户询问无法观察到的事项。若用户指定了区域或缺陷，则从那里开始。生成技能时使用仓库真实的命令、路径与名词，不留占位符。技能中记录覆盖范围（每个检查覆盖哪些文件与函数）以及最后一次确认验证与代码相符的提交；当被覆盖代码在该提交之后发生变化时，后续智能体可据此判断验证需要重新审视。
适用场景
适用于需要为关键代码建立可重复形式化验证的仓库，尤其是测试难以覆盖、出错后果严重的部分。
限制
验证须忠于代码：模型或证明的每一部分都应指向审查者可打开的真实代码，视为不可分割的一步在代码中也应是不可分割的一步，命名来自本仓库。检查必须能够失败：从未见过失败的检查不能证明任何事，需在破坏变体（如移除检查或重排步骤）上展示每条性质失败。发现应保持为发现：当前代码破坏性质时，应以代码术语报告反例，不得为通过而弱化性质或模型，也不得在用户未要求时修改产品代码。须如实说明范围：说明验证了什么、在哪些边界与假设下、遗漏了什么；通过只覆盖模型或有界范围，而非整个系统。应无需工具即可读懂：用各一句平实的话陈述性质与危害，用代码语言以简短步骤序列讲述反例。应低成本重跑：一条命令、可复现的工具版本、足够短的运行时间。应与代码保持同步。
交接
向用户说明验证了什么、使用了哪个工具及原因、边界、检查以平实语言发现了什么、如何运行、以及不覆盖什么。仅当发现相近目标时才建议第二个目标。若改动后未重新检查，可指向 /maintain-formal-verification-skill 使验证重新对齐。