maintain-formal-verification-skill

更新于 2026-10-20

维护形式化验证 skill

形式化检查证明的是它所描述对象的一条性质。代码变了、验证没变，检查可能还在通过，但它描述的代码已经不存在。这种通过最危险，因为它看起来像一份证明。这个 skill 是 /create-formal-verification-skill 所生成验证 skill 的维护循环，也适用于任何项目本地的 skill：对指定代码跑模型检查器、证明器或代码级验证器的那种。项目本地 skill 处理的是 agent 使用它期间自己做的改动。这个 skill 处理绕过它的改动：合并、没走 skill 的编辑，以及许多提交累积出来的漂移。

结果

给每条检查一个结果，并说明是哪一个：

in sync：上次同步以来，没有任何改动改变这条检查描述的内容，检查通过。
updated：代码变了，验证现在描述的是新代码，检查通过。
bug：验证描述的是当前代码，而代码违反了这条性质。这是关于代码的 finding，不是漂移。
blocked：检查没能重新对齐，或者跑不起来。说清楚到底是什么挡住了。

一条检查可以同时是 updated 和 bug：更新让验证重新描述代码，然后性质在它上面失败。

改动范围

只改验证本身：模型、harness（运行检查的脚手架代码）、性质文件，以及验证 skill 本身。一轮运行进行中绝不改产品代码，除非用户要求。一条性质在当前代码上失败时，不要为了让检查通过而弱化性质或模型。报告这个失败。

Pass

找到检查。 验证 skill 没有固定的名字，按它做的事来找：一个项目 skill，对指定代码跑模型检查器、证明器或其他验证器。读你找到的每一个，或者用户点名的那一个。对每条检查，收集这些内容：性质、覆盖的代码、上界和假设、运行它的命令，以及最后一次确认它与代码相符时所在的提交。没有验证 skill，就停下，指向 /create-formal-verification-skill。skill 没有记录同步提交时，用最后一次改动验证文件的提交，并说明你这么做了。
先照原样跑一遍。 改动任何东西之前，每条检查先跑一次，记录结果。这里的通过不说明代码正确，只说明旧的描述仍然成立。这里的失败可能是漂移，也可能是 bug。到第 5 步之前，不要判定是哪一种。
读完被覆盖代码的每一处改动。 从同步提交到当前提交，diff 被覆盖的文件，并读每一条提交说明。也要找搬走的代码：被覆盖的函数改了名、拆开或移到别的文件，仍是被覆盖的代码。还要找碰了检查所守护状态的新代码，比如一个写同样字段的新函数。对每一处改动，判断它属于哪一种：
- 没有影响。 改动没有改变验证描述的任何内容，比如格式、注释，或验证不覆盖的代码路径。判断要对照模型或 harness，不要对照提交说明。
- 验证不再描述代码。 原本不可分割的一步变成了两步，增加或删掉了分支，检查挪了位置，一条新路径到达被守护的状态，或某个值的范围变了。模型或 harness 必须改。
- 承诺是有意改的。 改动改变了代码的承诺，而改动里的证据说明这是有意为之：文档注释、测试、changelog 或提交说明。性质必须改，而且必须引用这份证据。
- 承诺可能被打破。 代码变了，没有证据说明承诺变了。随后出现的失败按疑似 bug 处理。
按代码更新，不按结果更新。 修改模型或 harness，让每个改过的部分重新指向审查者能打开的代码。代码里不可分割的一步，在验证里仍是一步。重跑之前先按代码写好更新，不要照着能让检查通过的样子去捏它。只有承诺是有意改的，才改性质。写下旧写法、新写法和证据。上界保持不变，除非改动让它不再成立。必须缩小上界时，在报告里说明。
重跑，逐个判断结果。
- 通过： 检查可能在一份已经失去失败能力的描述上通过。按性质防范的方式弄坏新代码，比如删掉一个新检查或调换新步骤的顺序，确认检查能抓住它。然后撤掉这个破坏。
- 失败： 对照真实代码，逐步重放反例。如果某一步在代码里不可能发生，就是验证错了。修好验证，并说明错在哪。如果每一步都可能发生，那就是 bug。指出引入它的提交，用代码自己的说法把反例讲成一串步骤，用一句话说明危害。如果针对真实代码的一次低成本测试或复现能展示这个 bug，把它作为证据加进报告。不要把它提交进产品代码。
更新验证 skill。 更新每条检查覆盖的代码、命令、上界、假设，以及同步提交。把同步提交设成你检查过的那个提交。blocked 的检查不要前移同步提交，并在报告里说明。然后像下一个 agent 那样，照验证 skill 走一遍，确认它的步骤仍然能跑。

报告

对每条检查，告诉用户：

结果，以及你读过的提交；
验证里改了什么、为什么，每处改动给一句简短理由：代码形状变了，或承诺是有意改的（附上证据）；
重跑结果，以及你用来证明更新后的检查仍能失败的那个破坏；
每个 bug，用大白话讲：用代码的说法写出的反例步骤、危害，以及引入它的提交；
验证仍然没有覆盖的内容，包括它应该覆盖却没覆盖的新代码。

直接说清哪些失败是验证里的漂移，哪些是代码里的 bug。一条检查在你更新之前通过、更新之后失败，就说明旧的通过建立在过时的描述上。

把验证的更新放进一个独立的改动，跟任何产品修复分开。