南大 Specula 用 Claude Code 自动生成 TLA+，已挖出 382 个深层并发 bug
jiqizhixin · x · 2026-09-03
南京大学发布 Specula，把编码 agent（Claude Code、Codex、Copilot CLI）变成形式化验证工程师，破解形式化验证长期被少数专家垄断的困局。
工作原理
- agent 阅读目标系统的代码、文档、测试与提交历史
- 自动生成 TLA+ 模型与正确性不变量
- 运行模型检测（model checking），再将每个反例带回真实代码复现，并打包成测试用例
- 全流程自动化，无需 TLA+ 专业知识
成果：截至 2026 年 8 月，Specula 已在 67 个开源系统中发现 382 个深层并发 bug，并被多家公司与社区的开发者采用。原本需要专家数月才能完成的规范构建，如今缩短到小时级。
形式化验证擅长捕捉最深层的并发 bug，但为一个复杂系统构建可用规范往往需要专家投入数月——Specula 把这一瓶颈交给了 AI agent。
「编程与Agent」频道最新
- 把密码交给云端浏览器安全吗？实测对比四款 AI 个人 Agent 隐私政策 — petergyang · 2026-09-03
- LoopArena 论文：Agent 循环控制器才是瓶颈，最强模型成功率仅 24.7% — rohanpaul_ai · 2026-09-03
- 开发者实测:Fable 5.1 搭配 Sonnet 子智能体体验出色,甩开 Claude Code — tobowers · 2026-09-03
- Obsidian 新玩法：QuickAdd 一条命令随手捕获待办任务 — dSebastien · 2026-09-03
- Sergey Karayev:Fable 5.1 是我用过最好的编程模型,快且不怕长会话 — sergeykarayev · 2026-09-03
- Software World:用智能体运营的「GitHub」,多 agent 协作优化 Python 依赖链 — ZimingLiu11 · 2026-09-03