pstack × TLA+ 深度学习包

目标：对 pstack 全流程，尤其是形式化验证部分，理解得比作者 poteto 更深。内容基于本地 pstack v0.15.36 源码、upstream main 和一次实跑 TLC。

本页来源：pstack README、statechart SKILL.md、TLC 命令行选项（current-tools）。

先说结论

已经能超过作者的一点

statechart 会把 TLC 的“危险警告”吞掉。PickWorker 带 SYMMETRY 查活性时，报告写“规则成立”，去掉 SYMMETRY 就是反例。这是实跑结果，upstream main 的报告至今相同。

1. 形式化验证在 pstack 里是一条旁路：setup-pstack 和 poteto-help 会提，poteto-mode 的路由表不会提。【已证实】
2. statechart 是“判定 + 投影”：TLC 判规则，view 决定读者看到什么。图只标不变量，活性反例只在文字报告里。【已证实 / 从代码推测】
3. 防漂移靠流程，不靠机器：sync commit、agent 读 diff、通过后故意改坏。没有代码到模型的自动映射。【已证实】
4. 公平性、refinement、SYMMETRY/VIEW 与活性的冲突，SKILL 都没讲。这些是你超过作者的切入口。【已证实】

学习路线与验收

“比作者更深”的意思：能回答作者文档没写的问题，并且能用一次运行证明。

1. L0 画出地图（半天）：不看资料，画出 setup-pstack 到三个 FV skill 的交接。验收：说清 setup 第 7、8 步各提什么，poteto-help 在什么条件下提 create 或 maintain。
2. L1 安全性（1 到 2 天）：自己写 Init、Next、INVARIANT，跑 TLC。验收：在 corpus 的 TwoPhase 上复现 TCConsistent 的 5 步反例，并说出种下的 bug。
3. L2 活性与公平（2 天）：读 CounterLoop 和 HiddenClock。验收：删掉 WF，预测并跑出结果。能写一个 WF 不够、必须 SF 的例子。
4. L3 statechart 内部（2 天）：读 run.ts 的 judge 和 ChartRun，以及 cfg.ts。验收：说清退出码 11、12、13，ChartMark 如何不停 TLC 也能标出坏状态，500 和 10 万两个阈值各管什么。
5. L4 用在自己的前端代码上（3 到 5 天）：挑一个重试队列或上传状态机，跑 create-formal-verification-skill。验收：生成的检查在一个临时改坏的版本上失败。改一次代码，跑 maintain，得到一个 sync commit。
6. L5 超过作者（持续）：找工具自己的盲区，并跑出证据，比如本页的 SYMMETRY 和 VIEW 实测。写出修复草案，例如报告透传 TLC 警告、有 PROPERTY 时拒绝 SYMMETRY，并加 corpus 测试。验收：一份可复现的 issue 草稿。要不要发出去，由你决定。

pstack 全流程地图

实线是 SKILL 文本里写明的交接。虚线是缺失的交接。

flowchart TD
  setup(["setup-pstack<br/><small>选模型，写 pstack-models 规则</small>"])
  mode["poteto-mode<br/><small>路由，23 个 playbook</small>"]
  pb["playbook<br/><small>Feature、Bug fix、Investigation…</small>"]
  arch["architect<br/><small>先画类型和签名</small>"]
  arena["arena / swarm<br/><small>并行候选与分片</small>"]
  inter["interrogate<br/><small>只认跑出来的发现</small>"]
  pr["opening-a-pr"]
  help["poteto-help<br/><small>按问题推荐 skill</small>"]
  cfv["create-formal-verification-skill<br/><small>生成项目的验证 skill</small>"]
  proj["项目 verify skill<br/><small>TLA+ 模型与检查</small>"]
  sc["statechart<br/><small>TLC 结果转成图和报告</small>"]
  mfv["maintain-formal-verification-skill<br/><small>代码变化后同步</small>"]

  setup --> mode
  setup -->|第 8 步提议| cfv
  mode --> pb
  pb -->|跨函数边界| arch
  arch --> arena
  arch -->|有争议的设计| inter
  pb --> pr
  pb -.->|无路由| cfv
  help -->|竞态、不变量| cfv
  help -->|被覆盖代码变了| mfv
  cfv --> proj
  proj -->|按名字调用| sc
  mfv --> proj

交接	触发条件	标记
setup-pstack 到 create-verification-skill	第 7 步，项目还没有时提一次	已证实
setup-pstack 到 create-formal-verification-skill	第 8 步，项目还没有时提一次	已证实
poteto-help 到 create 或 maintain	问题涉及竞态或不变量；被覆盖代码在 sync commit 之后变了	已证实
生成的 skill 到 statechart	每次读 TLA+ 结果，按名字调用	已证实
poteto-mode 到 architect、swarm、arena、interrogate	跨函数边界、并行、设计比拼、有争议	已证实
poteto-mode 到任何 FV skill	没有	已证实（缺口）

FAQ：TLA+ 与形式化验证

挑战者视角。每题：短答、机制、来源、标记。点开看机制。

全局（5）

形式化验证从哪里进入 pstack 的流程？ 【已证实】

短答：三个入口。setup-pstack 第 8 步提议一次。poteto-help 遇到竞态、不变量问题时提一次。用户直接调用。poteto-mode 的路由表不提它。

机制：setup-pstack 第 7 步提 create-verification-skill，第 8 步提 create-formal-verification-skill，各一次，只在项目里还没有时。对 poteto-mode 的 SKILL.md 和 23 个 playbook 搜 tla|formal|statechart，命中 0 次。

来源：setup-pstack、poteto-help、poteto-mode

什么时候选形式化验证，而不是测试？ 【已证实】

短答：选承诺最强、坏了会伤到用户、测试又很少走到的那一处。典型是事件顺序、重试、并发。

机制：create-formal-verification-skill 先从代码里挑目标，再按问题选工具。事件顺序用模型检查器，默认 TLA+。对所有输入成立的性质用代码级验证器。没有验证器就用生成输入的测试。任意规模都成立的性质用证明。

来源：create-formal-verification-skill

三个 FV 相关 skill 怎么分工？ 【已证实】

短答：create 生成项目自己的验证 skill 和检查套件。maintain 在代码变了之后把检查同步回来。statechart 读 TLC 结果，画成图并写报告。

机制：create 要求生成的 skill 按名字调用 /statechart，不复制它的命令和路径，因为这些会随版本和机器变。生成后要先在一个临时改坏的版本上跑一次，确认能抓住，再撤回改动。

来源：create-FV、maintain-FV

README 说“最好的 spec 是代码”，那写 TLA+ 不矛盾吗？ 【从代码推测】

短答：大体不矛盾。pstack 里的 TLA+ 不是事前的设计文档，是从现有代码抽出来、可以失败的检查。但作者没有正面回答过这个问题。

机制：create 的第一条质量标准是“忠于代码”：模型每一部分都能指回代码，模型里的一个原子步在代码里也必须是一个原子步，名字取自仓库。

来源：README、create-FV

作者用它真的找到过 bug 吗？ 【未知】

短答：作者说在团队代码上找到过几个，但没有公开具体是哪些。

机制：这条来自转述作者 X 帖子的二手摘要。原帖内容未能直接核对。

来源：MindPattern 摘要

statechart（6）

statechart 怎么把 TLA+ 变成 Mermaid 图？ 【已证实】

短答：四步。先用 TLC 判定每条规则。模型小的话再导出整张状态图。用你写的 view 把内部状态投影成读者能懂的状态。最后输出 chart.mmd 和 report.md。

机制：SANY 先解析 spec。judge 跑多轮 TLC，参数固定为 -workers 1 -fp 0 -lncheck final。distinct 状态不超过 500 时，生成 ChartRun 模块，用 -dump dot,actionlabels 导出 graph.dot。ChartMark 是一个不变量，用 PrintT 打印每条规则被破坏的状态，但不让 TLC 停下。之后是 walk、bugs（最短的排前）、project、lift、mermaidLines。超过 500 状态时只画反例路径，没有反例就不写 chart.mmd。

来源：run.ts、cfg.ts、ir.ts

一条规则坏了，其他规则还会检查吗？ 【已证实】

短答：会。去掉坏掉的规则再跑，直到没有规则坏。但第一次坏之后，每轮最多 10 万个 distinct 状态，没跑完的列在 “Rules not checked”。

机制：ir.ts 里 RERUN_STATES = 100_000。重跑时配置里加 CONSTRAINT ChartBound，即 TLCGet("distinct") < 100000。有多个时序性质待查时，会拆成每个性质一组分别跑。退出码 0 表示通过，11、12、13 表示违反，其他值算出错。

来源：run.ts、ir.ts

为什么只用 1 个 worker，还固定 -fp 0？ 【从代码推测】

短答：为了可重复。同样的输入每次给出同样的图和报告，测试才能逐字比对。

机制：corpus 测试断言生成的 report.md 和 chart.mmd 与仓库里提交的完全一致。多 worker 时反例不保证最短，顺序也不稳定。SKILL 没有写明这个动机。

来源：corpus.test.ts、TLC 选项

流程正常结束，为什么会报 deadlock？ 【已证实】

短答：TLC 把没有下一步的状态算作死锁，正确的终态也算。解决办法是在 Next 里加一个 Done 动作，只在终态为真，且什么都不改。

机制：judge 默认传 -deadlock，意思是不查死锁。只有包含死锁规则的那一组才查。

来源：statechart SKILL、run.ts

view 模块决定什么？ 【已证实】

短答：决定读者看到的状态和箭头上的字。图对不对，看的是 view 有没有说实话。

机制：state() 返回字符串得到平面图，返回数组得到父子状态，返回对象得到并行区域。step(action, from, to) 给箭头写用户视角的话，比如“你按了播放”，不写代码名。另有 group、colors、title。建议不超过 20 条箭头。隐藏步骤时，每个状态仍须可达，且至少保留一条出边。并行区域会撒谎时，退回父子状态。

来源：statechart SKILL、TwoPhase 示例

反例路径一定是真 bug 吗？ 【已证实】

短答：不一定。SKILL 要求把路径在真实代码上重放一遍，重放不出来就先假设模型错了。

机制：见下面“理论”组的 VIEW 实测。模型合并了状态时，反例可能是假的。

来源：statechart SKILL

理论（6）

safety 和 liveness 在 pstack 里怎么区分？ 【从代码推测】

短答：safety 说坏事永远不发生，写成 INVARIANT，反例是有限的一段路径。liveness 说好事终究会发生，写成 PROPERTY，反例是一个套索，最后在环里打转，或停在某处不动。

机制：report 把活性反例写成 “The run loops through …” 或 “The run stops in … forever”。图上的 breaks、mayBreak 标记来自 ChartMark，而 ChartMark 是一个不变量，所以只标安全性规则。-lncheck final 表示活性在整张图算完后才检查。

来源：report.ts、CounterLoop

公平性（WF / SF）在 pstack 里有指导吗？ 【已证实】

短答：没有。statechart SKILL 全文不提公平性。没有公平条件时，系统可以永远原地不动，几乎所有活性性质都会“坏”。所以写不写公平条件，全看写模型的 agent。

机制：在 statechart SKILL.md 里搜 fair，命中 0 次。corpus 的 spec 用了 WF_vars(Next)，差分测试会随机生成强、弱公平。工具能处理，但没有告诉人什么时候该加。

来源：statechart SKILL、differential.test.ts

状态爆炸怎么处理？代价是什么？ 【已证实】

短答：靠小模型：常量取小，再加 CONSTRAINT、SYMMETRY、VIEW。每一种都有代价。

机制：超出 CONSTRAINT 的状态只检查、不展开，那里的死锁会被藏起来，SKILL 自己写明了这点。CONSTRAINT 和活性一起用很微妙，不等于把约束合取进 Next。Merz 在邮件列表里引了 Specifying Systems 14.3.5。

来源：statechart SKILL、tlaplus 邮件列表

SYMMETRY / VIEW 碰上活性性质会怎样？ 【实测】

短答：会出错，而且 statechart 不提醒。我在 2026-10-29（新加坡时间）跑出了一次假通过和一次假违反。

机制：PickWorker：带 SYMMETRY 时 TLC 说 “No error”，报告写 PicksFirst 成立。去掉 SYMMETRY，TLC 立刻给出反例：选了 w2，之后一直不动。TLC 自己打印了 “Declaring symmetry during liveness checking is dangerous”，但 report.md 没有带上这句。何况 First = w1 是一个特殊元素，本来就不该声明对称。HiddenClock：带 VIEW 时报 EndsAtZero 被违反，去掉 VIEW 就没有错误。upstream main 上的 PickWorker 报告至今相同。

来源：PickWorker、HiddenClock、对称与活性（邮件列表）

refinement（细化）在 pstack 里出现过吗？ 【已证实】

短答：没有。三个 FV skill 都不提 refinement。TLA+ 的常规做法是用 INSTANCE 引入抽象规格，把 Abstract!Spec 当作 PROPERTY 检查。statechart 能不能正确处理这种性质，未测。

机制：在 create、maintain、statechart 三个 SKILL.md 里搜 refine，命中 0 次。

来源：Specifying Systems

模型和代码漂移了怎么办？ 【已证实】

短答：靠 maintain。它记录一个 sync commit，让 agent 逐条读改动并分类。没有自动的“代码到模型”映射。

机制：结论分四种：同步、已更新、发现 bug、受阻。“已更新”和“发现 bug”可以同时成立。每条改动分成四类：无影响、描述已过时、承诺被有意改变（要给证据）、承诺可能被打破。要按代码改模型，不能按结果改。重跑通过后，还要故意改坏代码，证明检查仍会失败。检查受阻时 sync commit 不动。原话：“The dangerous case is a pass on a stale description.”

来源：maintain-FV

局限（3）

什么情况下形式化验证帮不上忙？ 【从代码推测】

短答：模型只覆盖写进去的步骤和小常量。原子性抽错了，结论就全错。它证明的是模型，不是代码。性能、视觉、真实超时这类连续量问题都不适合。

机制：pstack 用“忠于代码”、“能失败”、“诚实的范围”三条标准来压这个风险，但这些靠 agent 自律，没有机器检查。

来源：create-FV

除了 TLC，还用别的工具吗？ 【已证实】

短答：SKILL 只点名 TLA+。作者的帖子里提过 Rust 的 Kani，这条是二手来源。Apalache（SMT，有界检查）和 TLAPS（定理证明）都没有提到。

机制：statechart 固定 tla2tools v1.7.4 并校验 sha256，Java 用 temurin-25，经 mise 安装。可以用 TLA2TOOLS、JAVA 环境变量覆盖。

来源：run.ts、Apalache

前端开发能用上吗？ 【从代码推测】

短答：能。重试队列、上传状态、多步表单、乐观更新、WebSocket 重连，都是事件顺序问题。

机制：principle-model-the-domain 本来就推荐用状态机代替零散的布尔值。状态机越明确，越容易逐个动作翻译成 TLA+。

来源：model-the-domain

访谈提纲

从浅到深。后两层专挑文档没写、或者与别的 skill 矛盾的地方。

话题	内容
话题 1	动机：为什么在 agent 时代押注形式化方法
话题 2	建模：原子步、抽象层次、前端异步怎么切
话题 3	工具：statechart 的确定性、阈值、view 的可信度
话题 4	理论缺口：公平性、refinement、对称与活性
话题 5	漂移：maintain 的流程，能不能自动化
话题 6	路由：为什么 poteto-mode 不触发 FV
话题 7	独立性：同一个 agent 写代码、模型、view 和判定

入门

1. 你什么时候开始觉得测试不够、需要 TLA+？是哪一个具体的 bug？
2. 一个前端开发第一次写 TLA+，最常犯的错是什么？
3. 为什么 statechart 输出 Mermaid，而不是直接给 TLC 原始输出？
4. create-formal-verification-skill 是“生成 skill 的 skill”。为什么不直接生成 spec？

进阶

1. -workers 1 -fp 0 是为了确定性吗？大模型上慢下来你怎么取舍？
2. 500 状态的图上限和 10 万状态的重跑上限，这两个数字怎么定的？
3. view 由 agent 写。如果 view 把两个本应分开的状态合并了，谁能发现？
4. “忠于代码”要求原子步一致。React 的批量更新、异步 effect，你怎么切原子步？
5. maintain 靠 agent 读 diff 来分类改动。有没有考虑过从代码自动抽出动作，再和模型比对？

挑战

1. README 说“不相信规划，最好的 spec 是代码”。TLA+ 模型算不算一种规划？
2. poteto-mode 的路由表从不触发形式化验证。这是有意的，还是遗漏？Feature 或 Bug fix 碰到并发时，该不该自动提？
3. statechart 的图只标不变量。活性反例只在文字报告里。读图的人会不会以为“图上没红就没事”？
4. SKILL 不讲公平性。agent 不加 WF，活性全坏；乱加 SF，又会把真 bug 藏起来。你怎么防？
5. 代码长出一个模型里没有的状态时，工具会报警，还是照样画？（社区里 @buildAgoat 问过，未见回答）
6. 失败的性质怎么对应到图上具体哪一条红箭头？（社区里 @jatingargiitk 问过）

可能难倒作者

1. 你的 corpus 里 PickWorker 声明了 SYMMETRY 又查活性。TLC 打印了危险警告，报告却写“PicksFirst 成立”。去掉 SYMMETRY 就是反例。这是不是 maintain 说的那种“最危险的通过”？
2. HiddenClock 在 VIEW 下报了一个假的活性违反。工具为什么不在有 PROPERTY 时拒绝或警告 VIEW 和 SYMMETRY？
3. First = w1 这种特殊元素让对称声明本身就是错的。工具能不能自动检测“对称集合里有被点名的元素”？
4. CONSTRAINT 加活性时语义并不等于把约束合取进 Next（Specifying Systems 14.3.5）。ChartBound 在重跑时也是 CONSTRAINT，它会不会改变活性结论？
5. refinement 是 TLA+ 最强的一招，为什么三个 skill 都不提？“代码细化模型”能不能当作对抗漂移的主机制？
6. 生成的验证 skill 要求“能失败”，只要求在一个改坏的版本上失败一次。怎么知道这个改坏版本有代表性，而不是挑软柿子？
7. 当 agent 同时写代码、写模型、写 view、判反例，四者出自同一个模型的同一个误解，哪一环是独立的？
8. 规则超出 10 万状态就列为“没检查”。在 CI 里，“没检查”算通过还是失败？

自测题

先自己答，再打开答案。

显示答案

1. INVARIANT 和 PROPERTY 的反例形状有什么不同？

前者是有限前缀。后者是套索：一段前缀加一个环，或者停在某处不动。

2. TwoPhase 里 TCConsistent 的最短反例是几步？种下的 bug 是什么？

5 步。管理者只要有一个资源管理者 prepared 就提交，而不是等全部 prepared。

3. 为什么正确的终态会触发 NoDeadlock？怎么修？

终态没有下一步。在 Next 里加一个只在终态为真、不改任何变量的 Done 动作。

4. statechart 传给 TLC 的固定参数是哪三组？

-workers 1、-fp 0、-lncheck final。

5. 图上 500、重跑 10 万这两个阈值分别控制什么？

500 决定画整张图，还是只画反例路径。10 万限制第一次违反之后每轮重跑的规模，超过的规则列为未检查。

6. ChartMark 怎样在不停下 TLC 的情况下标出坏状态？

它是一个不变量，对坏状态用 PrintT 打印带随机标记的行，并始终返回真。

7. CONSTRAINT 之外为什么会藏死锁？

那些状态只检查、不展开，所以看不到它们有没有后继。

8. PickWorker 为什么在 SYMMETRY 下“通过”？

对称把 {w1}、{w2} 合成一个代表，真实路径“选了 w2 再也不动”被吞掉了。而且 First = w1 让集合本来就不对称。

9. 去掉 HiddenClock 的公平条件 WF，结果会怎样？

可以一开始就永远原地不动，EndsAtZero 不再必然成立。（推论，没有实跑）

10. maintain 结论的四种结果是什么？哪两种能同时成立？

同步、已更新、发现 bug、受阻。已更新和发现 bug 可以同时成立。

11. 检查通过后，maintain 为什么还要故意改坏代码？

证明检查仍然能失败。否则可能是对过时描述的通过。

12. create 选工具的四个分支是什么？

事件顺序用模型检查（默认 TLA+）。所有输入用代码级验证器。没有验证器用生成输入的测试。任意规模用证明。

未证实与待查

事项	状态	怎么查
作者用 FV 找到的具体 bug	未知	访谈时直接问
Kani 出现在作者帖子里	二手来源	找作者 2026-10-18 的原帖
-workers 1 -fp 0 的动机	从代码推测	读 #741、#776 的 PR 描述
statechart 处理 refinement 性质是否正确	未测	写一个 Impl => Abstract!Spec 的小 spec，跑 statechart
重跑时的 ChartBound 约束是否影响活性结论	未测	构造一个超过 10 万状态、带 PROPERTY 的模型对比
删掉 WF 后 HiddenClock 的结果	推论	删掉 WF_vars(Next) 再跑 TLC
10 月 27 日“port the statechart compiler”（#977）改了什么	未读	读 #977 的 diff

实测环境：tla2tools v1.7.4（sha256 与 run.ts 里固定的值一致），Temurin 21 JRE，命令行直接跑 TLC，没有经过 mise 和 Java 25。时间是 2026-10-29 21:03（新加坡时间）。

资料

• pstack README：github.com/cursor/plugins
• statechart SKILL.md：github.com/cursor/plugins
• statechart 提交历史：github.com
• create-formal-verification-skill：github.com/cursor/plugins
• maintain-formal-verification-skill：github.com/cursor/plugins
• Add pstack plugin（PR #73）：github.com，2026-05-23
• poteto 关于 statechart 的帖子：x.com，2026-10-22
• TLC 命令行选项（current-tools）：github.com/tlaplus
• Specifying Systems（Lamport）：lamport.azurewebsites.net
• TLA+ 主页：lamport.azurewebsites.net
• Learn TLA+：learntla.com
• Apalache：apalache-mc.org