0.15.28：形式化验证补上维护
更新于 2026-10-20
0.15.28 新增 /maintain-formal-verification-skill：代码变了、形式化验证没跟着变时，用它把验证拉回与代码一致。/create-formal-verification-skill 生成的 verify skill 现在会记下覆盖范围和同步提交；事件顺序类问题默认用 TLA+，语言上没有验证器时要明说再退到生成输入测真实代码。
英文对照的一头一尾：f9be7aa（0.15.27）、d457567（0.15.28）。0.15.27 的译文和指南留在历史版本。
形式化验证补上了「维护」这一半
Section titled “形式化验证补上了「维护」这一半”0.15.27 那轮新增的 /create-formal-verification-skill 解决了「建」。这次 #716 解决「养」。提交说明说，项目本地的 verify skill 管的是 agent 用着它时做的改动；这个新 skill 管的是绕过它的改动：合并、没用 skill 的直接编辑，以及跨多次提交积累起来的漂移。
新 skill 的开头解释了为什么需要它。原文：
When the code changes and the verification does not, the check can keep passing while it describes code that no longer exists. That pass is the dangerous case, because it looks like a proof.
代码变了、验证没变，检查可能还在通过，但它描述的代码已经不存在了。这种通过最危险，因为它看起来像一份证明。
用法是跑一遍维护循环：从记录的同步提交（sync commit）到现在，读完所有动过被覆盖代码的提交；对照代码更新模型、harness 或性质；重跑；再用一个会破坏性质的临时改动，证明更新后的检查仍然能发现失败。最后给每项检查一个结论：in sync（一致）、updated（已更新）、bug（代码的真问题）、blocked（拉不齐，写明原因）。
几处值得注意的规则：
- 只改验证一侧（模型、harness、性质文件、verify skill 本身），不碰产品代码，除非用户要求。性质在当前代码上失败时，不许放宽性质或模型来求通过。
- blocked 的检查不推进同步提交。提交说明给出的原因是，blocked 的检查没有确认过能描述代码，推进同步提交会把漂移藏起来，让下一轮看不见。
- 找 verify skill 不靠名字，靠它是干什么的：在项目里跑模型检查器、证明器或代码级验证器的 skill。
配合地，/create-formal-verification-skill 生成的 verify skill 现在会写入两样东西：每项检查覆盖哪些文件和函数，以及最近一次确认验证与代码一致时的提交。这样后来的 agent 能看出被覆盖的代码在那之后有没有变。交付时它也会把用户指向 /maintain-formal-verification-skill。验证与交付指南同步补了一段说明。
以后怎么做：合并或重构动过被验证的代码之后，跑一次 /maintain-formal-verification-skill。看到 bug 结论时，它报的是代码问题，不是验证漂移，两者会在报告里分开写。
事件顺序问题默认用 TLA+，没有验证器就明说
Section titled “事件顺序问题默认用 TLA+，没有验证器就明说”#721 改了 /create-formal-verification-skill 里选工具的那段。事件能不能按错误顺序发生，这类问题现在在「任何语言」里都默认用 TLA+；原来那句「并发和分布式设计通常从 TLA+ 开始」删掉了。
另一处新增：所用语言上没有能跑的验证器时，agent 要明说这一点，然后用生成的输入去测真实代码，而不是手写一份函数模型来测。
提交说明给出的理由是，新段落是一个预先登记的评测（preregistered eval）测过的原文。#724 把验证与交付指南第 6 页的选工具段落同步成同样的说法，因为指南还留着旧措辞。
以后怎么做：让 agent 验证事件顺序类性质时，预期它默认拿 TLA+，除非它说明换工具的理由。你的语言没有验证器时，预期它告诉你，再退到用生成的输入测真实代码。
指南、README 和帮助页同步到位
Section titled “指南、README 和帮助页同步到位”#716 和 #724 把新 skill 补进了所有已经覆盖形式化验证的地方：
- README 的命令表加了一行：被形式化验证覆盖的代码在上次检查之后变了，就用
/maintain-formal-verification-skill。 - 定制指南第 9 页的「两个特殊情况」句子现在同时指向 create 和 maintain 两个 skill，链接也改指验证与交付指南里的形式化验证一节。
/poteto-help的状态检查多了一条：项目里有形式化验证 skill，而它覆盖的代码在记录的同步提交之后变过，问题又涉及这些代码时，就提/maintain-formal-verification-skill。路由表和做法参考（recipes）也加了对应条目，做法参考里写的是：那片代码合并或重构之后，跑/maintain-formal-verification-skill。
这些都是入口和指路的更新，不改已有命令的用法。
没有中文对照的文件
Section titled “没有中文对照的文件”只改版本号的提交（0.15.28 bump），以及面向机器的 plugin.json（两处），都不做中文翻译，所以没有对应中文页。Claude Code harness 的拷贝是重新生成的，也不另译。
三笔提交都在北京时间 2026-10-19，作者栏均为 Cursor Agent，其中 #716 和 #724 与 lauren 共同署名。