maintain-formal-verification-skill

维护形式化验证技能

在 Codex 上，遵循本技能前，请阅读平台映射，包括其中针对各项技能的说明。

在 GitHub Copilot 上，遵循本技能前，请阅读平台映射，包括其中针对各项技能的说明。

在 Muse 上，遵循本技能前，请阅读平台映射，包括其中针对各项技能的说明。

形式化检查会证明其所描述内容的一项性质。当代码发生变化而验证没有更新时，即使检查描述的代码早已不存在，它仍可能继续通过。这种通过最危险，因为它看起来像一份证明。本技能用于维护由 /create-formal-verification-skill 生成的形式化验证技能，或任何针对具名代码运行模型检查器、证明器或代码级验证器的项目本地技能。项目本地技能负责处理 Agent 使用该技能时所做的更改。本技能负责处理被跳过的更改：合并、未使用该技能时所做的编辑，以及在多个提交中逐渐累积的偏差。

结果

为每项检查指定一种结果，并说明是哪一种：

• 同步：自上次同步以来，没有任何更改影响检查所描述的内容，且检查通过。
• 已更新：代码发生了变化，验证现在描述的是新代码，且检查通过。
• 缺陷：验证描述的是当前代码，但代码违反了该性质。这是代码本身的问题，不是偏差。
• 受阻：无法使检查重新与代码一致，或无法运行。请明确说明原因。

一项检查可能同时属于“已更新”和“缺陷”：更新使验证重新描述代码，随后该性质在代码上验证失败。

编辑范围

只编辑验证相关内容：模型、测试框架、性质文件，以及形式化验证技能本身。运行期间绝不编辑产品代码，除非用户要求。当某项性质在当前代码上验证失败时，不要削弱性质或模型来让检查通过。请报告失败。

执行步骤

1. 找到检查。 形式化验证技能没有固定名称，因此要根据其用途查找：它是针对具名代码运行模型检查器、证明器或其他验证器的项目技能。/create-verification-skill 编写的项目 verify 技能负责驱动应用，不属于此类。阅读找到的每项技能，或用户指定的那一项。对于每项检查，记录其性质、覆盖的代码、边界与假设、运行命令，以及上次确认其描述与代码一致时的提交。如果不存在形式化验证技能，请停止并指向 /create-formal-verification-skill。如果技能未记录同步提交，请使用最近一次修改验证文件的提交，并说明你这样做了。

2. 按原样运行。 更改任何内容之前，先运行每项检查一次，并记录结果。此时通过并不能说明代码正确，只能说明旧描述仍然成立。此时失败可能是偏差，也可能是缺陷。在第 5 步之前，不要判断是哪一种。

3. 阅读所有受覆盖代码的变更。 比较同步提交到当前提交之间受覆盖文件的差异，并阅读每条提交说明。还要查找移动过的代码：即使受覆盖函数被重命名、拆分或移到其他文件，它仍属于受覆盖代码。还要查找触及检查所保护状态的新代码，例如写入相同字段的新函数。对于每项变更，判断它属于以下哪种情况：

   • 没有影响。 该变更不会改变验证所描述的任何内容，例如格式、注释，或验证未覆盖的代码路径。应根据模型或测试框架核对，而不是根据提交说明。
   • 验证已无法描述代码。 原本不可再分的一步现在变成了两步，新增或删除了分支，检查被移动，有新的路径能到达受保护状态，或某个值现在有了不同的范围。必须修改模型或测试框架。
   • 有意更改了承诺。 该变更改变了代码所作的承诺，并且变更中的证据表明这是有意的：文档注释、测试、变更日志或提交说明。必须修改属性，并引用该证据。
   • 承诺可能被破坏。 代码发生了变更，但没有证据表明承诺也发生了变化。将随后出现的失败视为候选缺陷。

4. 根据代码更新，而不是根据结果更新。 修改模型或测试框架，使每个发生变更的部分都能再次指向审查者可以打开的代码，并确保代码中的一个不可再分步骤在验证中仍对应一个步骤。重新运行前，先根据代码编写更新，不要为了让检查通过而调整更新内容。只有承诺有意发生变化时才修改属性。记录旧表述、新表述和证据。除非变更使边界不再正确，否则保留原有边界。如果必须缩小边界，请在报告中说明。

5. 重新运行并判断每项结果。

   • 通过： 现在，检查可能会在一个已失去失败能力的描述上通过。按照属性所防范的方式破坏新代码，例如删除新检查或重新排列新步骤，并确认检查能捕获该问题。然后撤销破坏。
   • 失败： 逐步对照真实代码重放反例。如果某一步在代码中不可能发生，则说明验证有误。修正验证，并说明错误所在。如果每一步都可能发生，则说明这是缺陷。指出引入缺陷的提交，用代码自身的措辞按步骤讲述反例，并用一句话说明造成的损害。如果通过针对真实代码的廉价测试或复现能证明缺陷，请将其作为证据写入报告。不要将该测试或复现提交到产品代码中。

6. 更新形式化验证技能。 更新每项检查覆盖的代码、命令、边界、假设和同步提交。将同步提交设为你已检查的提交。对于受阻的检查，不要移动同步提交，并在报告中说明。然后以接手的下一个 Agent 的身份完整执行一次形式化验证技能，确认其中的步骤仍可运行。

报告

针对每项检查，向用户说明：

• 结果，以及你阅读过的提交；
• 验证中改了什么以及原因，并简要说明每项变更的理由：代码结构发生了变化，或有证据表明承诺有意发生了变化；
• 重新运行的结果，以及你用来证明更新后的检查仍能失败的破坏方式；
• 每项缺陷的白话说明：用代码中的措辞按步骤描述反例、造成的损害，以及引入缺陷的提交；
• 验证仍未覆盖的内容，包括它本应覆盖但尚未覆盖的新代码。

明确指出哪些失败是验证漂移，哪些是代码缺陷。对于更新前通过、更新后失败的检查，请说明旧的通过结果基于过时的描述。

将验证更新单独作为一次变更，不要与任何产品修复放在一起。