新工具让编程代理用TLA+验证并优化软件状态

一个用于编写状态可信的软件的 agent skill。它教会编码 agent 用 TLA+ 为整个程序建模，把每份 spec 放在其所描述代码旁边的 .tla 文件中，在每次构建时用 tla-ts 检查每份 spec，并借助模型和代码一起让两者都变得更简单。

Agent 会犯状态错误：在一个锁区段里设置标志、在另一个锁区段里读取，Stop 在队列排空之前就返回，把按钮展示给无法按下它的人。测试只走一条调度路径，很少能发现这些问题。模型检查器会在其边界内走遍每一种交错、崩溃点和重启，并返回通往每条被破坏规则的最短路径。这个 skill 让这项检查成为日常工作的一部分，而不是特殊场合才做的事。

它需要 Node 20 或更高版本，或者 Bun。它不需要 Java 或 TLC。

为整个程序建模。每个持有状态的组件都有一份描述其真实步骤的 spec，外加一份更小的接口 spec，描述调用者能看到什么。实现会被检查是否精化了其接口，每份 spec 都建立在它下面的接口之上，根节点处的程序 spec 则端到端地检查人们所依赖的承诺。一份覆盖清单会为每个有状态组件列出 spec，或者给出它不需要 spec 的书面理由。

让每份 spec 紧邻其代码。worker.go 和 Worker.tla 共享同一个目录，并在同一个 commit 中变更。构建会检查 spec，因此与代码脱节的 spec 会让造成脱节的那次变更失败。

把 spec 和代码放在一起简化。agent 按代码现状建模，在模型中找到状态更少的设计，针对同样的承诺检查它，确认真实的原语能够强制每一步，构建它，并删除它取代的东西。然后进行下一轮。

证明每个守卫都是必要的。代码依赖的每个 check、recheck、signal 或 lock 都会得到一个 mutant：去掉该守卫的 spec，它必须破坏一条规则。存活下来的 mutant 意味着要么 spec 漏掉了某些东西，要么该守卫是死代码。

对照源码阅读每一个反例。trace 是对代码的一项断言。当代码能够走完每一步时，trace 就是复现，并成为回归测试。当它不能时，就是 spec 错了。

里面有什么 skills/tla/ SKILL.md agent 遵循的工作流 references/ whole-program.md spec 树、精化、覆盖、屏幕 modeling-code.md 忠实地为代码建模：调用者、步骤、平台语义 simplification.md spec 与代码的联合简化流程 defects-and-mutants.md 通过 spec 处理一个 bug；mutants 文件 tools/ tla 入口点；首次运行时安装固定版本的 tla-ts check.mjs 查找并检查每个模型和 mutant package.json、package-lock.json update-tla-ts.sh 将固定版本更新到最新的 tla-ts modules/Surface.tla 屏幕 spec 的共享规则 example/worker/ worker.go 一个 Go 任务队列 Worker.tla、Worker.cfg 紧邻它的 spec 和默认模型 WorkerApi.tla Worker 所精化的接口 Worker.mutants.json 四个守卫，每个都被证明是必要的 安装 Claude Code /plugin marketplace add paralin/tla-skill /plugin install tla@tla-skill Claude Code 会给插件 skill 加前缀，因此该 skill 是 /tla:tla。当任务匹配该 skill 的描述时，agent 也会自行加载它。

该仓库也是一个 Cursor 插件：.cursor-plugin/plugin.json 指向 skills/。或者把 skills/tla 复制到你项目的 .cursor/skills/。

把该文件夹复制到你的 agent 读取 skills 的目录： git clone https://github.com/paralin/tla-skill cp -r tla-skill/skills/tla ~/.claude/skills/tla # 或你的 agent 的 skills 目录 该 skill 是一个自包含的文件夹。不需要它之外的任何东西。 skills/tla/tools/tla skills/tla/example 首次运行会用 npm ci 安装固定版本的 tla-ts。然后： pass 580 states 16 deep 103 ms example/worker/Worker.cfg kill 189 states 6 deep 37 ms example/worker/Worker.tla mutant "take checks the queue and stops in two lock sections" [][Next]_vars (WorkerApi line 52) kill 13 states 3 deep 21 ms example/worker/Worker.tla mutant "Submit accepts after Stop" [][Next]_vars (WorkerApi line 52) kill 478 states 16 deep 55 ms example/worker/Worker.tla mutant "Submit does not signal" AcceptedRuns kill 266 states 7 deep 20 ms example/worker/Worker.tla mutant "Stop does not signal" deadlock 1 model(s), 0 failure(s) Worker 的 spec 通过了其安全性、活性和精化检查，每个 mutant 都破坏了它应当破坏的规则。用 TLA_MUTANT_TRACES=1 运行以查看每个反例。第一个就是 worker.go 中的单个锁区段所防止的 bug：

1. Init: lpc = "take", phase = "running", queue = <<>>, ...
2. Take: lpc = "check"
3. Submit(j1): sub = (j1 :> "signal" @@ j2 :> "idle"), queue = <<j1>>
4. StopMark: spc = "signal", phase = "draining"
5. CheckStop: lpc = "close", phase = "stopped"
6. CloseDone: lpc = "exited", done = TRUE 循环看到队列为空，一个任务被接受，Stop 被调用，而循环退出时已接受的任务仍在队列中。

然后让你的 agent 做实际工作，例如： 在 pool.go 旁边用 TLA+ 为我们的连接池建模，然后找一个更简单的设计 这个上传在重连后有时会完成两次。通过一份 spec 来处理它 为 internal/ 下每个持有状态的包添加 TLA+ 覆盖

检查器 tools/tla 接受目录、.tla 文件或 .cfg 文件，未给定任何参数时检查工作目录。

要在你自己的仓库中运行它，把 skills/tla/tools/ 复制到诸如 tools/tla/ 的路径，忽略其 node_modules/，并添加一个检查： { "scripts": { "check:tla": "tools/tla/tla src" } } 在 CI 中以及与你构建相同的本地循环中运行该检查。

tools/package.json 固定了 tla-ts，使每台机器用相同版本检查。tools/update-tla-ts.sh 把固定版本更新到最新发布版并刷新 lockfile；之后重新运行你的模型。

tla-ts 由 Aiden Bai 开发，是模型检查器，一个与 TLC 兼容的 TLA+ 检查的 TypeScript 实现，采用 MIT 许可。TLA+ 是 Leslie Lamport 的。