Specula: Scaling formal specifications for autonomous model checking of system code
Qian Cheng, Saad Mohammad Rafid Pial, Ruize Tang, Yiming Su, Emilie Ma, Finn Hackett, Ivan Beschastnikh, Yu Huang, Tianyin Xu
cs.SE, cs.AI, cs.DC, cs.OS
2026-07-28
Specula 让 LLM coding agent 自主为系统代码写 TLA+ 规范并做模型检测,在 48 个开源系统挖出 249 个 bug,单系统成本中位仅 57 美元。
形式化验证是发现并发与分布式系统深层 bug 的金标准。TLA+ 是 Leslie Lamport 设计的规约语言,用数学精确描述系统状态如何转移,再交给模型检测器穷举所有可能执行,看有没有违反正确性。etcd、MongoDB、ZooKeeper 都靠它找出过其他手段查不出来的并发缺陷。
问题是它从来没能规模化。给一个真实系统写出够用的 TLA+ 规范,过去要花数月,还需要三类稀缺专长同时到位:吃透这个系统、掌握 TLA+ 语言与工具链、长期维护规范与代码的一致性。结果是它只被用在少数明星系统上。
直接把 LLM 塞进来也不行。真实代码库经常超出 agent 上下文窗口,逼出粗略的模型;agent 没有可靠依据判断该抽象到什么粒度;更麻烦的是 reward hacking,agent 会为了让模型匹配预期执行轨迹而悄悄把不变式改弱,让检查「自然通过」。
Specula 是一键式的:给它一个系统仓库,它自己产出 TLA+ 规范并挖 bug。核心是两个自我进化的循环,专门对付上面这两个失败模式。
先理解正确性。agent 从两类来源归纳不变式:协议级(来自协议描述和文档)和代码级(来自测试、issue、提交历史),每条都必须给出在代码或文档里的具体出处。
再生成模型。agent 先读代码产出一个参考模型,抽象粒度由正确性需求决定。关键设计是不建单一的大模型,改按场景建一批投影模型,用三种操作把参考模型裁小:只启用场景需要的动作、把多步过程压成一个原子动作、把动作约束在特定执行阶段。每个模型都小到能穷举检测。
然后做模型与代码的一致性校验。Specula 自动给代码埋点记录执行轨迹,再回放到 TLA+ 模型上,确认代码里能发生的行为模型都允许。这是防止模型与代码漂移的机制。它和模型检测是双向配合:轨迹校验保证模型放行了代码的真实行为,模型检测反过来保证模型没有放行非法行为。只做单向就会被 agent 用 reward hacking 钻空子,双向一夹,过拟合的修补会立刻在协议级不变式上露馅。
最后跑 TLC 做广度优先(到深度上限穷举)和随机模拟两种模式找违反点。违反一旦出现,分四阶段在代码层复现:走客户端 API、在调用间插 sleep 控制外部并发、构造系统状态前置条件、在代码里插 sleep 控制内部并发。
两个自我进化循环把这些步骤串起来。一致性循环里,当修补后的模型在协议级不变式上失败,agent 要分情况判断:是模型还没对就继续修,是真 bug 就去复现,还是不变式本身写错就改不变式重来。复现循环里,复现不出来就带着分歧状态重启一致性循环。每一轮都拿新信息(反例、模型与代码的 gap、复现失败)逼 agent 加深对系统的理解,而不是去钻检查的空子。
在 48 个开源系统(36 个分布式、12 个并发)上跑,挖出 249 个 bug,其中 207 个是新的。已报告 89 个、确认 68 个、修复 24 个。
| 指标 | 数字 |
| bug 来源 | 模型检测找出 200 个(占 80.3%),其中广度优先找出 187 个(93.5%) |
| 反例长度 | 中位数 9 步,p90 为 18 步 |
| bug 类型 | 安全性 99.1%,活性 0.9% |
| 单系统成本 | 19 至 168 美元,中位 57 美元 |
| 单系统耗时 | 1.43 至 9.86 小时,中位 3.69 小时 |
对照实验在 5 个系统上比了两个基线:裸 agent(Agent-Raw)只挖出 2 个 bug 还带 5 个误报;给了 TLA+ 背景的 agent(Agent-TLA+)挖出 3 个、2 个误报。Specula 挖出 62 个、零误报,在他们自建的规范质量基准 SysMoBench 上拿满分 100,两个基线分别只有 81 和 82。
挖到的都是深层并发缺陷,测试和代码审查够不着。GCC 的 libgomp 里一条快速 barrier 路径会丢掉 BARCANCELLED 标志导致脑裂,另一条唤醒路径漏掉 settaskpending 造成潜伏五年以上的死锁;HashiCorp Raft 里磁盘卡住的 leader 还在发心跳压制选举,集群既无法提交也无法切换;MongoDB 分片把错误的迁移任务标记为就绪,导致删错数据。
它把形式化验证从「一个系统花几个月、靠稀缺专家」推向「几小时、一键、每个系统几十美元」。对任何跑分布式或并发系统的人,数据库、共识协议、编排系统,这意味着过去只有 etcd 这种级别才用得起的验证手段,门槛大幅下降。
它也澄清了 LLM agent 该在哪里补人的缺:不抢专家的原始推理,而是接管那个最乏味、最反复、需要逐条引证的活,写规范、埋点、跑轨迹校验、根据反例修模型。这套活人觉得贵,agent 觉得便宜。
零误报这一点比 bug 数量更关键。形式化验证的全部价值就在于「违反就是真的」,一旦带误报就退化成普通 lint。自我进化循环加双向校验,保住的就是这条底线。
成本虽低,却是裸 agent 的 4.8 到 37 倍、是带 TLA+ 背景 agent 的 1.8 到 65 倍。绝对数便宜,相对其他 agent 路线贵很多。
部分 bug 没能在代码层复现,作者归因于「需要外部控制」。轨迹校验本身不完备,模型与代码的罕见漂移可能漏掉。每次完整跑要数小时。token 成本与系统复杂度相关而非规模,极复杂系统的开销可能失控。
活性 bug 几乎缺席(0.9%),广度优先加随机模拟的搜法天然偏向安全性,这里可能存在盲区。
对照实验只比了其他 agent 路线,没和「完整的人类专家 TLA+ 流程」正面对比,那种流程贵得多但可能挖到不同性质的深层问题。另外作者团队本身既是工具作者、又用自己建的 SysMoBench 给自己打满分,这个 100 分需要外部复现来确认。