用途
测试只检查有人想到要写的用例，形式化验证则检查某个声明范围内的所有情况：模型中步骤的每一种顺序、某个边界内的所有输入，或全部输入。本技能的作用是：在代码库中找到最需要这种验证的部分，验证其中的一条属性，并留下一个项目本地的技能，让下一个智能体在改动代码时能对照该属性进行检查。
生成的技能面向一个冷启动的读者——他在改动进行中读到它，从未见过你的工作。用户应当能够信任结果，并在不学习验证语言的情况下据此行动。
主要能力
- 从代码本身选择验证目标：优先选择代码做出的承诺，且该承诺一旦被破坏会伤害用户、而测试很少覆盖到破坏它的情形。应选择仓库中最强的此类目标，而不是最容易验证的那个。
- 让问题决定工具：在模型检查器、证明助手、SMT 验证器或其他工具中选择成本最低者。事件是否可能以错误顺序发生，通常适合用模型检查器对设计的小模型进行验证，TLA+ 是任何语言下的默认选择；代码本身是否对每个输入都表现正确（如内存安全、溢出、数据结构不变量），通常适合在代码上运行的验证器。若该语言没有可运行的验证器，应如实说明，并用生成的输入测试真实代码，而不是手工建立函数模型。必须在任意规模下成立、边界不够用的属性，可能需要证明。优先选择仓库开发者能安装并运行的工具，并向用户说明选择理由。
- 生成项目本地技能：技能需带 frontmatter，指明区域并说明何时使用；没有 frontmatter 技能不会注册。仅凭该技能，下一个智能体必须能判断某次改动是否触及被验证的代码、运行检查、区分真实缺陷与建模错误，并在改动是有意为之的情况下更新验证。技能中需包含覆盖记录和同步提交（sync commit），并告知下一个智能体只有在确认验证描述了新提交处的代码后，才能推进同步提交。使用仓库真实的命令、路径和名词，不留占位符。
- 交付前自证：按生成的技能走一遍，就像下一个智能体那样，在一个会破坏该属性的临时改动上运行。它必须捕获该破坏。然后撤销临时改动，确认检查回到初始状态：通过，或仅在你将要报告的发现上失败。从未运行过的验证技能只是草稿。若技能漏掉破坏或某步骤无法运行，应修复技能或验证，而不是修改临时改动。
使用方式
从代码库中回答目标选择问题，只向用户询问无法从代码中观察到的事项。若用户指定了区域或缺陷，从那里开始。
选择工具时，优先选择仓库开发者能安装和运行的工具，并说明理由。
生成技能时，写入项目本地的技能位置；对 Codex 优先使用 .agents/skills/。生成的验证文件和临时变异应保留在该仓库或一次性副本内。工具安装和外部访问遵循原生权限。已有的 proof-orchestrator 负责选择证明路径；model-capability-router 负责模型选择。模型检查只证明其声明的模型和边界，不证明未检查的产品代码。不要修改产品代码，也不要为了获得通过而弱化属性。
适用场景
- 代码中存在一旦破坏就会伤害用户、而测试很少覆盖的承诺。
- 需要验证事件顺序、输入边界、内存安全、溢出或数据结构不变量等属性。
- 希望为后续智能体留下可复用的、与代码同步的验证技能。
限制
- 验证通过只覆盖模型或边界，不覆盖整个系统。
- 若某语言没有可运行的验证器，只能如实说明并用生成输入测试真实代码。
- 不得修改产品代码或弱化属性以求通过；发现的问题应如实报告，并附上以代码术语表述的反例。
- 验证技能必须与代码保持同步：需记录每个检查覆盖的文件和函数，以及最后一次确认验证描述这些代码的提交；被覆盖代码在该提交之后发生变化时，下一个智能体应能看出验证需要重新审视。
- 交付前必须实际运行验证并确认能捕获破坏，否则只是草稿。
- 关于收费、价格、平台等信息，资料中暂未提供。