Specula 开源:用 TLA+ 规约让编码 agent 挖掘分布式系统深层 bug
tianyin_xu · x · 2026-09-23
作者在介绍 TLAPS-Bench 的同时,推广团队的 agent 工具 Specula(specula-org,468 stars)。
- Specula 用编码 agent 为目标系统自动编写 TLA+ 规约(含刻画正确性的不变式和描述系统实现的形式模型)
- 随后对规约做模型检验,并在代码层面复现违例,专找并发与分布式系统中的深层 bug
- 已在多个开源项目中找到深层 bug,官方维护 bug 清单与案例库(含模型与复现证据)
- 现已支持 CI 功能,持续在改进
「编程与Agent」频道最新
- 开发者的算账:100 次 eval 只花 20 美元,说明题目太简单 — pvncher · 2026-09-23
- 用 AI 复刻 2019 年构想的游戏,做完发现点子没想象中好 — BLUECOW009 · 2026-09-23
- 开源 Agent Message Board：让并行编码智能体共用留言板协作 — airesearch12 · 2026-09-23
- 从业者断言：好评测的保质期只有三个月 — pvncher · 2026-09-23
- AI 编程工作流的笔记泛滥困境:有人呼吁「Agentic 版 SCRUM」 — nezvanovova · 2026-09-23
- 前沿多模态模型会吞掉 Docling/Marker 这类 PDF 解析层吗? — lucasbennett_1 · 2026-09-23