create-formal-verification-skill

更新于 2026-10-19

创建形式化验证 skill

测试只检查有人想到并写下来的用例。形式化验证检查明确范围内的所有用例：模型中步骤的每一种顺序、某个上界内的每一个输入，或者所有输入。这个 skill 会找出仓库中最需要这样做的部分，验证它的一条性质，并留下一个项目本地 skill。下一个 agent 可以用它检查改动是否仍满足这条性质。写给这样的 agent：它在改动做到一半时毫无背景地读这份 skill，也从未见过你的工作。用户必须能信任结果并据此行动，不需要学会验证语言。

从代码中选择目标

从代码库里找答案，只有观察不到的才问用户。如果用户指定了某个部分或 bug，就从那里开始。

好目标是代码的一项承诺：一旦违背就会伤害用户，而测试很少覆盖会导致违背的用例。在仓库里选最重要的这种目标，不要选最容易验证的。

让问题决定工具

选择能以最低成本回答问题的工具：模型检查器、证明助手、基于 SMT 的验证器，或其他工具。要判断事件是否会按错误顺序发生，通常适合用模型检查器检查设计的小模型。要判断代码本身是否对所有输入都正确，比如内存安全、溢出或数据结构不变量，通常适合直接在代码上运行的验证器。如果一条性质必须在任意规模下成立，限定上界还不够，就可能需要证明。对于并发和分布式设计，TLA+ 往往是最有用的起点。优先选择仓库开发者能安装和运行的工具，并告诉用户你为什么选它。

好结果的标准

忠实于代码。 模型或证明的每个部分，都要能指向审查者可以打开的代码。验证中视为不可分割的一步，在代码里也必须是不可分割的一步。名称使用这个仓库里的叫法。
能够失败。 从未见过失败的检查什么也证明不了。让每条性质都在它所保护代码的损坏版本上失败一次，比如删掉一个检查或调换步骤顺序。
finding 仍然是 finding。 finding 就是验证发现的问题。当前代码违反性质时，用代码里的概念报告问题和反例。不要为了让检查通过而弱化性质或模型。除非用户要求，否则不要修改产品代码。
如实说明范围。 说明验证了什么，在哪些上界和假设下验证，以及哪些内容没有覆盖。检查通过只覆盖当前模型或设定的上界，不代表整个系统都正确。
不用工具也能读懂。 分别用一句直白的话说明性质和危害。把反例按代码里的说法讲成一串简短步骤。
重复运行成本低。 用一条命令运行，工具版本可复现。运行时间要足够短，让下一个 agent 愿意在每次相关改动后都跑一遍。
与代码同步。 已验证的代码变化时，要有机制提醒下一个 agent 重新审视这项验证。

生成验证 skill

写一个项目本地 skill。front matter 要写明针对的部分和何时使用。没有 front matter，skill 就不会注册。只读这份 skill，下一个 agent 必须能判断改动是否触及已验证的代码、运行检查、区分真实 bug 和建模错误，并在改动确属预期时更新验证。使用仓库里真实的命令、路径和名词，不留占位符。

交付前先证明它能用

像下一个 agent 那样，在真实代码里做一个会让它违反这条性质的临时改动，再照着生成的 skill 做一遍。检查必须发现这个问题。然后丢弃临时改动，确认检查恢复原状：要么通过，要么只因你准备报告的 finding 而失败。从未运行过的验证 skill 只是草稿。如果 skill 没发现这个问题，或者某个步骤跑不起来，就修 skill 或验证本身，不要修临时改动。

交付

告诉用户你验证了什么、用了哪个工具以及为什么、验证的上界、如何运行、没有覆盖什么，并用直白的话说明检查发现了什么。只有已经发现了另一个相近目标，才提出建议。