Specula 团队在 SIGOPS 博客发布了 SysMoBench。这个评测集用 11 个真实并发和分布式系统，测试主流 LLM 能不能从代码里生成 TLA+ 规格。
这里最有意思的地方，不是模型会不会写 TLA+。
更尖锐的问题是：它写出来的规格，和 Etcd、ZooKeeper、RedisRaft 这类真实系统的代码行为是不是一致。
这件事把“AI 会形式化方法”拉回了代码现场。会编译、能跑 TLC，只能说明模型掌握了语法和一部分建模套路。对分布式系统团队来说，错的规格比没有规格更麻烦，因为它会制造一种“已经验证过”的错觉。
SysMoBench 真正测的是代码一致性
TLA+ 可以粗略理解成一种给并发和分布式系统写数学规格的语言。它常被用来描述状态、动作和不变量，再交给 TLC 这类工具检查模型有没有跑出坏状态。
但工程里的难点从来不只是“写出一个漂亮规格”。难点是把真实代码抽象成模型时，哪些状态能省，哪些动作不能合并，哪些实现细节必须保留。
SysMoBench 的评测路径比较直接。每个任务提供源码、trace 采集 harness 和 invariant 模板，让模型生成 TLA+ 规格后进入四阶段检查。
| 阶段 | 检查对象 | 回答的问题 |
|---|---|---|
| syntax | TLA+ 是否能解析编译 | 模型会不会写对语法 |
| runtime | TLC 是否能运行 | 模型是否写出可执行模型 |
| conformance | trace 与规格动作是否一致 | 模型是否贴合真实代码行为 |
| invariant | 关键性质是否成立 | 模型是否保住系统性质 |
结果分化很明显。
主流 LLM 在 syntax 上接近满分。也就是说，TLA+ 的表层形式已经不是最大问题。runtime 开始拉开差距，但真正的断层在后两项：conformance 平均约 46%，invariant 平均约 41%。
这组数字不该被写成永久排名。原文也说明，模型更新很快，leaderboard 会滚动变化。
但它至少说明一件事：今天很多模型可以写出“像 TLA+ 的东西”，却还不能稳定写出“像这份代码的 TLA+ 规格”。
这也是评估 AI 工具时容易踩的坑。只看 syntax 和 runtime，会得到偏乐观的结论；把 conformance 和 invariant 放进来，问题才露出来。
教科书协议和真实实现之间，差一个 recvset
SysMoBench 里最能说明问题的例子，来自 ZooKeeper Fast Leader Election。
真实 ZooKeeper 代码里，每个 server 的 recvset 是一个按 sender 做 key 的 map。同一个 peer 在新 round 发来新的 vote，旧 vote 会被覆盖。
Claude Sonnet 生成的规格却把它写成集合累加：recvVotes' = recvVotes \cup {newVote}。
这个写法很像教材里的“累积投票证据”。问题是，它不符合 ZooKeeper 的实现。规格会同时保留同一个 sender 的新旧 vote，后续 quorum 计数就可能进入真实代码不会出现的状态。
还有一类错误更隐蔽：把多步代码合并成一个原子 guard。
ZooKeeper 收到更高 electionEpoch 的消息时，真实代码会先提升本地 logicalClock，再处理消息。LLM 生成的 HandleNotification 却用 guard 直接禁掉这类消息。
模型看上去写得更简洁，实际删掉了选举轮次里必经的中间状态。
这就是“会背协议”和“会贴实现”的差别。
Raft 论文附录里的 TLA+ 规格可以解释协议思想，但不能自动等同于 Etcd 的实现规格。Etcd 怎么拆动作，ZooKeeper 怎么更新结构，RedisRaft 怎么落状态，这些细节才是工程建模的硬骨头。
对形式化方法工程师来说，这个差别很实际。评审模型输出时，不能只问“这是不是 Raft/Zab/FLE 的合理抽象”，还要追问“这是不是当前仓库这段代码的抽象”。
失之毫厘，谬以千里。形式化规格里的一个 map 被写成 set，就足够把验证带到另一条路上。
对工程团队：看 trace，不只看 demo
SysMoBench 对两类人最有用。
一类是分布式系统和形式化方法工程师。它给出的动作建议很具体：把模型输出放到 trace 里验，不要停在“能编译、能跑 TLC”。如果某个 action 在真实执行窗口里对不上，就先修模型抽象，而不是急着讨论 invariant 是否漂亮。
另一类是评估 LLM 或代码 agent 的技术负责人。采购或内部选型时，可以把 conformance、invariant、trace replay 能力放进验收项。短期内，不必因为一个模型能生成 TLA+ demo 就迁移流程；更合理的做法，是先在团队已有系统上跑小规模 harness，看它能不能反复读代码、跑 trace、修规格。
SysMoBench 的 Transition Validation 方法也很务实：从真实运行采集 trace，把 trace 切成 pre_state / action / post_state 窗口，再让 TLC 逐动作验证规格能否完成同样转移。
这比“模块能不能跑”更接近工程问题。它可以直接指出：哪个 action、在哪个状态窗口、和真实代码失配。
但 SysMoBench 不是全自动判官。
| 现实约束 | 影响 |
|---|---|
| trace 覆盖不足 | 没跑到的路径无法评估 |
| 状态抽象有损 | 例如把 log 简化成 logLen 和 logLastTerm 后，中间 entry term 的检查会变难 |
| 新系统接入要人工工作 | 仍需写 harness、invariant 模板和 Transition Validation 模块 |
所以它更像高质量工程评测框架，不是“一键把仓库变成形式化规格”的流水线。
原文还提到一个重要边界：Claude Code、Codex 等代码 agent 在当前任务上表现更强，Specula 自身也声称在现有 SysMoBench 任务上达到完整 conformance 和 invariant 分数。
这不能推出“LLM 注定不能建模”。更准确的判断是：单次提示生成规格还不够。能读仓库、跑 trace、修规格、再验证的 agent，才更接近工程可用形态。
接下来要看的也不是谁短期登顶。
更关键的变量有三个：新系统接入成本能不能降下来，trace 覆盖能不能系统化扩展，agent 的高分能不能迁移到没见过的大型代码库。
如果这三点没有改善，榜单再好看，也只能说明模型更会解当前这套试卷。对工程团队来说，真正该买账的是可迁移的建模闭环，不是一次漂亮生成。