关于 maintain-formal-verification-skill
此技能用于随代码变化维护形式化验证检查，并区分验证漂移与代码缺陷，面向使用模型检查器、证明器或代码验证器的项目。
主要功能
- 01查找并记录验证检查
- 02对照模型审查覆盖代码的变化
- 03更新验证且不弱化属性
- 04将结果分类为同步、已更新、缺陷或受阻
- 05测试通过的检查是否仍能发现失败
- 06报告漂移、缺陷、覆盖范围与证据
适用场景
- 01合并后复查验证
- 02发现代码修改导致的过时检查
- 03调查形式化检查失败
- 04更新项目级验证指南
安装
复制下面的命令，在终端中运行。
npx skills add https:/安装后在 Claude Code 中输入/maintain-formal-verification-skill确认已加载。
附带文件agents/openai.yaml
详细介绍
维护形式化验证技能
形式化检查可以证明其所描述内容的一项性质。代码发生变化而验证没有更新时，检查可能仍然通过，却描述着已不存在的代码。这种通过最危险，因为它看起来像是证明。本技能用于维护由 create-formal-verification-skill 技能生成的验证技能，或任何针对具名代码运行模型检查器、证明器或代码级验证器的项目本地技能。项目本地技能负责处理 Agent 使用该技能时自行做出的更改。本技能负责处理那些绕过该技能的更改：合并、未使用该技能所做的编辑，以及多次提交中逐渐累积的偏差。
结果
为每项检查指定一种结果，并说明是哪一种：
- 同步：自上次同步以来，没有任何更改影响检查所描述的内容，且检查通过。
- 已更新：代码发生了变化，验证现在描述的是新代码，且检查通过。
- 缺陷：验证描述的是当前代码，而代码违反了该性质。这是代码问题，不是偏差。
- 受阻：无法使检查恢复一致，或无法运行检查。请准确说明原因。
一项检查可以同时是已更新和缺陷：更新使验证重新描述代码，随后该性质在代码上验证失败。
编辑范围
只编辑验证内容：模型、测试框架、性质文件和验证技能本身。运行期间绝不编辑产品代码，除非用户要求这样做。当某项性质在当前代码上验证失败时，不要弱化性质或模型来让检查通过。请报告失败。
通过
-
找到检查项。 验证技能没有固定名称，因此要根据它的用途来查找：查找会针对指定代码运行模型检查器、定理证明器或其他验证器的项目技能。阅读找到的每个技能，或用户指定的技能。对于每项检查，收集其属性、覆盖的代码、界限和假设、运行命令，以及上次确认其仍能描述该代码的提交。如果不存在验证技能，请停止并指向
/create-formal-verification-skill。如果技能没有记录同步提交，请使用最近一次修改验证文件的提交，并说明你这样做了。 -
按原样运行。 在做任何更改之前，每项检查都运行一次，并记录结果。检查通过并不能说明代码正确，只能说明旧描述仍然成立。检查失败可能是代码与描述不一致，也可能是错误。直到第 5 步之前，都不要判断是哪一种。
-
阅读覆盖代码的每项更改。 对比同步提交和当前提交之间覆盖文件的差异，并阅读每条提交说明。还要查找移动过的代码：被覆盖的函数即使重命名、拆分或移动到另一个文件，仍属于覆盖代码。还要查找会触及检查所保护状态的新代码，例如写入相同字段的新函数。对每项更改，判断它属于以下哪一种：
- 没有影响。 更改不会改变验证所描述的任何内容，例如格式、注释或验证未覆盖的代码路径。要根据模型或测试框架进行核实，而不是根据提交说明。
- 验证不再能描述代码。 原本不可分割的一步现在变成两步、添加或删除了一个分支、检查被移动、新路径可以触及受保护状态，或某个值现在的取值范围不同。必须更改模型或测试框架。
- 承诺有意更改。 更改改变了代码的承诺，并且更改中的证据表明这是有意的：文档注释、测试、变更日志或提交说明。必须更改属性，并引用该证据。
- 承诺可能遭到破坏。 代码发生了更改，但没有证据表明承诺也发生了更改。将随后出现的失败视为潜在错误。
-
根据代码更新，而不是根据结果。 更改模型或测试框架，让每处变更都能再次指向审阅者可以查看的代码，并确保代码中一个不可分割的步骤在验证中仍对应一步。重新运行之前，先根据代码编写更新；不要为了让检查通过而调整更新。只有承诺有意更改时才更改属性。记录旧措辞、新措辞和证据。除非更改导致界限不再适用，否则保留原有界限。如果必须缩小界限，请在报告中说明。
-
重新运行并判断每项结果。
- 通过： 检查现在可能是因为描述失去了发现错误的能力才通过的。按照该属性所保护的方式破坏新代码，例如移除新检查或重新排列新步骤，并确认检查能够捕获问题。然后撤销该破坏。
- 失败： 按步骤将反例在真实代码中重现。如果某一步在代码中无法发生，则验证有误。修正验证，并说明哪里出了问题。如果每一步都可能发生，则这是一个错误。指出引入错误的提交，用代码自身的措辞按步骤说明反例，并用一句话说明造成的损害。如果对真实代码进行低成本测试或复现能够证明该错误，请将其作为证据加入报告。不要将其提交到产品代码中。
-
更新验证技能。 更新每项检查覆盖的代码、命令、界限、假设和同步提交。将同步提交设为你已检查的提交。对于受阻的检查，不要移动同步提交，并在报告中说明。然后，像下一位 Agent 一样完整执行一次验证技能，以确认其中的步骤仍能运行。
报告
针对每项检查，告知用户：
- 检查结果，以及你查看过的提交；
- 验证内容有哪些变化及其原因，并简要说明每项变化的原因：代码结构发生了变化，或有意改变了约定（并提供证据）；
- 重新运行的结果，以及你用来证明更新后的检查仍能失败的故障；
- 每个错误的通俗说明：用代码中的措辞列出反例步骤、造成的危害，以及引入该错误的提交；
- 验证仍未覆盖的内容，包括应该覆盖但尚未覆盖的新代码。
明确说明哪些失败是验证内容过时所致，哪些是代码中的错误。对于更新前通过、更新后失败的检查，要说明旧检查通过是因为描述已经过时。
将验证更新单独提交，与任何产品修复分开。