该技能用于形式化验证的日常维护。形式化检查只能证明其所描述内容的一个性质；如果代码改了而验证没改，检查可能继续通过，但它描述的已是不存在的代码，这种通过最危险，因为它看起来像证明。本技能负责处理“漏掉”同步的情况：合并、未走该技能的直接编辑，以及跨多个提交累积的漂移。项目本地的验证技能负责处理使用该技能期间产生的变更，本技能负责其余部分。
【主要能力】
-
定位检查项：形式化验证技能没有固定名称，按用途寻找：对具名代码运行模型检查器、证明器或其他验证器的项目技能。由 /create-verification-skill 生成的驱动应用的 verify 技能不属此类。对每个检查收集：性质、覆盖代码、边界与假设、运行命令、最近一次确认其描述代码的提交。若不存在形式化验证技能，则停止并指向 /create-formal-verification-skill；若技能未记录同步提交，则用最后一次修改验证文件的提交，并说明这一点。
-
原样运行：改动前先运行每个检查一次并记录结果。通过不代表代码正确，只说明旧描述仍成立；失败可能是漂移，也可能是缺陷，需在第 5 步再判定。
-
阅读被覆盖代码的每次变更：从同步提交到当前提交做 diff，阅读每条提交信息；留意被移动的代码（重命名、拆分、移到其他文件的功能仍属被覆盖代码），以及触及被检查状态的新代码。逐项判断变更类型：无影响；验证不再描述代码（需改模型或测试框架）；承诺被有意改变（需改性质并引用证据，如文档注释、测试、变更日志或提交信息）；承诺可能被破坏（作为缺陷候选）。
-
依据代码更新，而非依据结果更新：让模型的每个变化部分重新指向评审者可打开的代码，保持代码中一个不可分割步骤在验证中也是一步。先写出更新再重跑，不按“怎样能通过”来塑造更新。仅当承诺被有意改变时才改性质，并记录旧措辞、新措辞与证据。除非变更使其失效，否则保留边界；若必须降低边界，在报告中说明。
-
重跑并逐项判定：
- 通过：检查可能已失去失败能力。按性质防范的方式破坏新代码（如移除新增检查或重排新增步骤），确认检查能捕获，然后撤销破坏。
- 失败：将反例逐步回放到真实代码。若某步骤在代码中不可能发生，则验证有误，修复验证并说明错在哪里；若每一步都能发生，则是缺陷：指出引入它的提交，用代码自身的语言把反例讲成步骤序列，用一句话说明危害。若对真实代码的廉价测试或复现能证明缺陷，作为证据写入报告，但不提交到产品代码。
- 更新形式化验证技能：更新每个检查覆盖的代码、命令、边界、假设与同步提交；同步提交设为你检查的提交。受阻的检查不移动同步提交，并在报告中说明。随后像下一位智能体那样按形式化验证技能执行一遍，确认其步骤仍可运行。
【报告内容】对每个检查说明：结果及阅读过的提交；验证改了什么、为什么（代码形态变化或承诺被有意改变及证据）；重跑结果，以及用于证明更新后检查仍能失败的破坏方式；每个缺陷的通俗描述：用代码语言表述的反例步骤、危害、引入提交；验证仍未覆盖的内容，包括本应覆盖而未覆盖的新代码。明确区分哪些失败是验证漂移、哪些是代码缺陷；对更新前通过、更新后失败的检查，说明旧通过基于过时的描述。验证更新应与产品修复分开提交。
【适用场景】适用于存在形式化验证技能或项目本地验证技能（运行模型检查器、证明器或代码级验证器）的项目，在代码合并、他人直接编辑或长期漂移后恢复验证与代码的一致性。
【限制】不修改产品代码（除非用户要求）；不为通过而削弱性质或模型；受阻时须说明原因；在 Codex 与 GitHub Copilot 上须先阅读平台映射及其按技能注释再遵循本技能。