formal-verification — 测试够不着的地方，用穷举兜住

测试只检查有人想到的情况。形式化验证在声明的范围内检查每一种情况：模型里每种步骤顺序、界内每个输入，或全部输入。它比测试贵，所以只用在一处：代码做出的某个承诺，坏了会伤到用户，而坏掉的那种情况测试又很少走到。

两种用法：

• 创建：选目标、验证一个性质、生成项目本地的 verify skill。按本文做。
• 维护：代码在没复查验证的情况下变了（合并、重构、绕过 verify skill 的改动），验证可能照样通过，描述的却是已经不存在的代码。读 references/maintain.md。

结果要让用户不学验证语言也能信任并据此行动；生成的 verify skill 写给中途冷启动、从没见过这次工作的下一个 agent。

选目标

从代码里回答，只问用户看不到的；用户点名了区域或 bug 就从那里开始。好目标是这样一个承诺：坏了会伤到用户，测试又很少走到坏掉的那种情况——两次重试重叠、锁在写到一半时过期、状态变化乱序到达、某个输入让解析器越界。选仓库里最强的那个目标，不是最容易验证的那个。

让问题选工具

挑以最低代价回答这个问题的工具：

• 事件会不会以坏的顺序发生：在设计的小模型上跑模型检查器，任何语言都默认用 TLA+。
• 代码本身是否对每个输入成立（内存安全、溢出、数据结构不变量）：用直接跑在代码上的验证器。
• 这门语言没有能跑在代码上的验证器：说明这一点，用生成的输入去测真实代码（基于属性的测试），不要给函数手写一个模型来验。
• 性质必须在任意规模下成立、有界不够：可能需要证明。

优先用仓库开发者装得上、跑得动的工具，并告诉用户为什么选它。

好的验证

• 忠于代码：模型或证明的每一部分都指向评审者能打开的代码；验证里当成一个不可分步骤的，在代码里也是一个不可分步骤；名字来自这个仓库。
• 能失败：没见过失败的检查什么也证明不了。对每个性质，在它守护的代码上造一个坏变体（删掉一个检查、调换两步），看它失败。
• 发现就是发现：当前代码违反性质时，用代码的语言给出反例并报告。不要削弱性质或模型直到它通过；用户没要求就不改产品代码。
• 范围诚实：写明验证了什么、在什么界和假设下、什么没覆盖。通过只覆盖模型或界，不覆盖整个系统。
• 不懂工具也能读：性质和危害各用一句大白话；反例讲成代码里的一串步骤。
• 重跑便宜：一条命令、可复现的工具版本、短到下一个 agent 每次相关改动都愿意跑。
• 跟代码同步：记录每个检查覆盖哪些文件和函数，以及最后一次确认验证与代码相符的 commit（同步点）。覆盖的代码在同步点之后变了，下一个 agent 就知道要再看一眼。

生成 verify skill

写一个项目本地 skill，放在当前 agent 会自动加载的项目 skill 目录（项目里已有 skill 目录就放在一起），名字带上验证的区域（如 verify-<app>-<区域>）：同一项目可能已有 app-verification 生成的 verify-<app>，同名会互相覆盖。frontmatter 写明验证的区域和什么时候用——没有 frontmatter 就不会被识别。仓库里只放能重跑出结果的东西（模型、harness、verify skill）；这一次的运行输出和反例日志写进交接，不提交，代码一变它们就过期。下一个 agent 只读这份 skill 就要能：判断一个改动是否碰到被验证的代码；运行检查；分清真 bug 和建模错误；改动是有意的时候更新验证。覆盖记录和同步点写在 skill 里，并告诉下一个 agent：确认验证描述的是新 commit 的代码之后，才把同步点往前挪。用这个仓库真实的命令、路径和名词，不留占位符。

交付前跑一遍

像下一个 agent 那样照着生成的 skill 做一遍：在真实代码上做一个破坏该性质的临时改动，检查必须抓到它。然后撤掉临时改动，确认检查回到原来的状态——通过，或只在你要报告的发现上失败。抓不到或某步跑不通，就修 skill 或验证本身，不要去改那个临时改动。没跑过的 verify skill 只是草稿。

交付

告诉用户：验证了什么，用的什么工具、为什么，界和假设，检查发现了什么（大白话），怎么运行，不覆盖什么。附近有很接近的第二个目标才提一句。之后代码变动绕过了这份验证时，按 references/maintain.md 让它跟上。