0.15.26–0.15.27：形式化验证，Claude Code 进入这一版

0.15.26 到 0.15.27 新增 /create-formal-verification-skill，让 agent 为测试难以覆盖、出错代价又高的一项代码性质做形式化验证，并留下可重复运行的项目 skill。/ketchup 改为把每件等你决定的事单列出来。10 月 17 日还没有版本号的 Claude Code 支持，这一版写进正式发布。

英文对照的一头一尾：6ce45c5（0.15.25）、f9be7aa（0.15.27 的版本号提交 0148b78 之后，plugin.json 仍是 0.15.27）。作者是 lauren（站外常称 poteto）。0.15.25 的译文和指南留在历史版本。

各小版本一句话

版本	一句话	代表提交
0.15.26	新增形式化验证 skill，Claude Code 可以安装 pstack，/ketchup 也会完整列出等你决定的事。	0b8e952（#710，北京时间 2026-10-18 15:31）
0.15.27	/sharpen 删掉「不要交回改写后的提示词」这条禁令。	0148b78（#713，北京时间 2026-10-19 04:18）
0.15.27 之后	/setup-pstack 结尾会询问是否创建形式化验证 skill，帮助和指南同步补齐。	f9be7aa（#715，北京时间 2026-10-19 05:58）

两个版本号提交本身只改版本号，上表那句话写的是该版本包含的前一批改动。#715 已包含在这次译文里，但会随下一个版本号发布。提交记录的作者均为 lauren；北京时间由 UTC 加 8 小时得到。

用形式化验证补上测试难到的地方

#709 新增 /create-formal-verification-skill。它从代码中选择一项重要性质来验证。你也可以指定区域或 bug，让它从那里开始。

测试检查有人想到的用例。形式化验证检查声明范围内的所有情况，例如模型里的所有步骤顺序、某个边界内的所有输入，或全部输入。它会按问题选择模型检查器、证明助手、基于 SMT 的验证器或其他工具，不固定只用一种。

这对并发、重试、状态机、解析器和 unsafe 代码尤其相关，因为这类代码可能测试很难碰到出错路径。通过后也要看清范围：通过的是模型或边界，不是整个系统。

交付前，agent 要用一个会破坏性质的临时改动，证明检查确实能发现失败。当前代码如果已经违反性质，它会报告反例。它不能放宽性质或模型来求通过，也不会擅自修改产品代码。

以后可以直接运行 /create-formal-verification-skill，或在命令后写明模块和要证明的性质。生成的是项目本地 skill，之后的 agent 可以用它复查相关改动。完整流程见验证与交付指南。

#715 把这个选择接到 /setup-pstack 末尾。项目还没有形式化验证 skill 时，它会问一次。回答 yes 就运行生成命令，回答 no 就继续。见安装指南。这笔提交在 0.15.27 之后，已纳入本次译文，但会随下一个版本号发布。

/ketchup 不再为短而漏项

#692 和 #708 改了 /ketchup 的回复格式。

旧的 150 词上限和每项写两行的格式，会让模型把多个 PR 折成一个数量，再把其余决定放进链接文件。现在，每个等你决定的事项都要单列，写清对用户的变化、推荐及依据、风险。涉及的 PR、issue 或 agent 要给编号或链接，低风险也要写。选项之间的决定，则要写出各选项的收益和代价。

经过的事控制在 100 词以内，每个事项约 30 词。两个事项的完整回复仍应远少于 150 词，但事项多时可以更长。#708 又明确了一点：不能为了凑字数删除或压缩事项，也不能用数量或链接代替清单。

你离开聊天后再回来，仍然运行 /ketchup。现在应当只看回复就能做决定，不必再打开另一个文件才能看全。大批量待决事项会让回复变长，这是新格式明确允许的结果。它仍然只读，也不会把状态清单或待决事项画成图。夜间任务后的用法见夜间工作指南。

在 Claude Code 里安装和运行

#637 把 pstack 打包成 Claude Code 插件。10 月 17 日合并时没有版本号，译文和代码解读在无版本号更新：pstack 支持 Claude Code，站长的说明在pstack 官方支持 Claude Code 了。0.15.26 起，这件事进入编号版本。#705 补上模型配置、Cursor 独有功能和本地文档三处缺口。#702 修正 skill 命名。安装方法见安装指南和插件说明。

在 Claude Code 里，依次运行 /plugin marketplace add cursor/plugins 和 /plugin install pstack@cursor-plugins。命令要带 pstack: 前缀，例如 /pstack:poteto-mode。

/pstack:setup-pstack 现在把模型选择写到 ~/.claude/rules/pstack-models.md。此前 Claude Code 不读 pstack-models.mdc，setup 会停下，而且什么也没有写入。

需要 Cursor Automations、Bugbot 或 Cursor cloud agent 的步骤，会留下一行跳过说明，再继续。后续步骤需要它的输出时，会留下命名的占位符。README 和指南也随插件安装，帮助页可以读取本地文件，不必再为这些内容请求 WebFetch 权限。

所有 skill 的 frontmatter name 现在都必须与文件夹一致。实际改名的是 Poteto Mode 和 Make Bot UI，它们改成 poteto-mode 和 make-bot-ui。旧的带空格名称在 Claude Code 里会形成无法运行的命令，Cursor 也会警告。以后在 Claude Code 里使用 /pstack:poteto-mode 和 /pstack:make-bot-ui。

四条原则改成判断方法

#633 重写四条原则，并同步更新原则指南和 /poteto-mode 的摘要。

• 测试行为，而非实现：做两个想象中的修改。行为坏了，测试应该失败。只改内部实现，测试应该继续通过。断言是否合适由外部可观察的约定决定，不由断言形式决定。/correct 的测试步骤也同步改了。
• 修复根因：先找系统最早出错的位置。触发问题的状态如果合法，在这里处理它就是修复。这个状态如果不该存在，就要去找产生它的位置，而不是加检查把问题藏起来。
• 质疑前提：把多个失败修复共同依赖的前提写下来，找一个能直接检验它的观察，再决定下一步。旧文规定的执行者清点不再是固定步骤。
• 让操作幂等：读取当前状态，与目标比较，只补差异。上次运行留下的锁、临时文件或任务，也要能凭证据判断是否过期。旧文不再把 PID 锁等具体机制写成固定做法。

提交说明说，旧文把具体机制规定得过死。新文要 agent 根据理由推出当前情境的做法。你以后引用这些原则时，也应让它检查行为、寻找最早出错点、直接验证前提、从现存状态推导步骤，而不是机械套用某个机制。

TypeScript 的 brand 不再靠 as

#700 修正 typescript-best-practices 的 branded types 示例。旧示例用 as 构造 brand，与同一 skill 的「不要用 as 转换」相冲突。

现在，parseAgentId 先通过 isAgentId 类型守卫收窄，再直接返回输入。规则也写明，brand 要来自会验证的类型守卫，不能来自 as。

你写 TypeScript 时，可以在边界验证一次，再用 input is AgentId 这样的类型守卫保留验证结果，不要靠类型断言补上编译器没有验证的事实。

四个 skill 删掉可省去的段落

#634 从 interrogate 的评审判断参考、swarm、type-system-discipline 和 migrate-callers-then-delete-legacy-apis 中删段。提交说明给出的理由是，没有这些文字，agent 也能同样遵守。

interrogate 删掉开头说明和结论校准，筛选原则保留。swarm 删掉开头摘要、设置 N 的一步和 Phase C 的一句结果格式要求，但最后报告仍要有表格、问题、缺口和退出者。两个原则 skill 也删掉多段具体规则。

用户不用改命令或配置。变化在 agent 读到的指令更短，不是新增一套操作流程。保留下来的步骤没有随这次删段消失。

指南和帮助页对齐现有行为

#704 修正 README 和指南里关于 autopilot、custom mode 和 harness 的过时说法，并清理措辞。提交说明明确说，措辞清理不改变主张。#715 又把已经发布的 skill 和用法补进 /poteto-help 与指南。

例如，夜间工作指南现在写明，autopilot-full 会先由 swarm 检查 code-ready head。之后的 rebase 或小修复由一个 fresh verifier 检查。只有新行为或大型新 diff 才再次调用完整 swarm。这是文档修正，不是本轮新增的 autopilot 行为。

指南还补了已有命令的入口和示例：只要复述目标时用 /in-your-own-words，开工前校准任务时用 /sharpen，快速补进度时用 /ketchup。见任务流程指南和用法与常见问题。这些页面是帮你找到已有能力，不代表它们都在本轮才新增。

/sharpen 删除一句禁令

#712 是 0.15.27 的唯一内容改动。它从 /sharpen 删掉「不要交回改写后的提示词」这句话，其他要求不变。

/sharpen 仍然先检查专家会怎么做、你真正要什么、任务是否规定得过死或不够，再保留一项外部检查并完成工作。新文本只是不再禁止交回改写后的提示词，不等于它必须交回。提交说明没有给出删除原因。

以后仍可把 /sharpen 放在任务前使用，但不要再用旧文本断言它绝不能返回改写后的提示词。

没有中文对照的文件

只改版本号的提交（#710、#713），以及面向机器的 plugin.json、Claude Code harness 文档和生成、检查脚本，都不做中文翻译，所以没有对应中文页。Claude Code 的安装和用法已在上述指南译文中说明。

提交一览

• e5136d8：把四条规定过死的原则改成推理方法（#633）
• 99743e9：从四个 skill 删掉可省去的段落（#634）
• 182f2ce：从生成树安装 Claude Code 版 pstack（#637）
• 0317eb8：branded types 示例改用类型守卫，不再用 as（#700）
• a968159：所有 skill 的 name 与文件夹一致（#702）
• 019a6a2：刷新文档，并增加文档与 skill 树的一致性检查（#704）
• 1b80080：补齐 Claude Code 插件的模型规则、跳过逻辑和本地文档（#705）
• 16541c6：/ketchup 列出每个待决事项，让回复足以做决定（#692）
• bc14437：明确禁止 /ketchup 为凑字数删除事项（#708）
• 4382e68：新增 /create-formal-verification-skill（#709）
• 0b8e952：版本号升到 0.15.26（#710）
• 75fabac：/sharpen 删除改写提示词的禁令（#712）
• 0148b78：版本号升到 0.15.27（#713）
• f9be7aa：setup 提供形式化验证选项，同步帮助和指南；尚未进入编号版本（#715）