maintain-formal-verification-skill

维护形式化验证技能

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

结果

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

• 同步：自上次同步以来，没有任何更改会改变检查所描述的内容，并且检查通过。
• 已更新：代码发生了变化，验证现在描述的是新代码，并且检查通过。
• 缺陷：验证描述的是当前代码，而代码不满足该属性。这是关于代码的发现，不是偏移。
• 受阻：无法使检查重新与代码保持一致，或无法运行检查。请准确说明原因。

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

编辑范围

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

通过

1. 找到检查项。 验证技能没有固定名称，因此要根据它的用途来查找：查找会针对指定代码运行模型检查器、定理证明器或其他验证器的项目技能。阅读找到的每个技能，或用户指定的技能。对于每项检查，收集其属性、覆盖的代码、界限和假设、运行命令，以及上次确认其仍能描述该代码的提交。如果不存在验证技能，请停止并指向 /create-formal-verification-skill。如果技能没有记录同步提交，请使用最近一次修改验证文件的提交，并说明你这样做了。

2. 按原样运行。 在做任何更改之前，每项检查都运行一次，并记录结果。检查通过并不能说明代码正确，只能说明旧描述仍然成立。检查失败可能是代码与描述不一致，也可能是错误。直到第 5 步之前，都不要判断是哪一种。

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

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

4. 根据代码更新，而不是根据结果。 更改模型或测试框架，让每处变更都能再次指向审阅者可以查看的代码，并确保代码中一个不可分割的步骤在验证中仍对应一步。重新运行之前，先根据代码编写更新；不要为了让检查通过而调整更新。只有承诺有意更改时才更改属性。记录旧措辞、新措辞和证据。除非更改导致界限不再适用，否则保留原有界限。如果必须缩小界限，请在报告中说明。

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

   • 通过： 检查现在可能是因为描述失去了发现错误的能力才通过的。按照该属性所保护的方式破坏新代码，例如移除新检查或重新排列新步骤，并确认检查能够捕获问题。然后撤销该破坏。
   • 失败： 按步骤将反例在真实代码中重现。如果某一步在代码中无法发生，则验证有误。修正验证，并说明哪里出了问题。如果每一步都可能发生，则这是一个错误。指出引入错误的提交，用代码自身的措辞按步骤说明反例，并用一句话说明造成的损害。如果对真实代码进行低成本测试或复现能够证明该错误，请将其作为证据加入报告。不要将其提交到产品代码中。

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

报告

针对每项检查，告知用户：

• 检查结果，以及你查看过的提交；
• 验证内容有哪些变化及其原因，并简要说明每项变化的原因：代码结构发生了变化，或有意改变了约定（并提供证据）；
• 重新运行的结果，以及你用来证明更新后的检查仍能失败的故障；
• 每个错误的通俗说明：用代码中的措辞列出反例步骤、造成的危害，以及引入该错误的提交；
• 验证仍未覆盖的内容，包括应该覆盖但尚未覆盖的新代码。

明确说明哪些失败是验证内容过时所致，哪些是代码中的错误。对于更新前通过、更新后失败的检查，要说明旧检查通过是因为描述已经过时。

将验证更新单独提交，与任何产品修复分开。