TLAPS-Bench 用 AI 形式化验证发现 SlateDB WAL 读一致性 bug
tianyin_xu · x · 2026-11-07
TLA+ 专家 Marc van Loo 介绍新论文 TLAPS-Bench：一个面向真实系统 TLA+ 规范、用 agentic AI 构建机器校验证明的基准与执行框架。
一个直接成果：作者为 SlateDB 的 WAL 协议写的 TLA+ 规范，经 TLAPS-Bench 配合 Astra Max 验证后暴露出一个读一致性 bug——SlateDB 本身很可能也存在同样问题（触发条件极苛刻，尚需确认），根源又是 GC 让 put-if-absent 变复杂。作者已验证了一个简单的修复方案。
值得注意的是：作者此前用模型检查器跑了 3 个并发写入者都未发现违例，而 TLAPS-Bench 用 4 个并发写入者就找到了问题，展示了 agentic AI 驱动的形式化验证在分布式系统正确性上的实用价值。
「编程与Agent」频道最新
- LoRA Loom:Windows 桌面端一键本地训练 LoRA,自动筛图配文 — Abject-Ad1903 · 2026-11-07
- Agent 调了哪个工具查不清?Reddit 热帖探讨 agent 身份与日志可信问题 — fred_pcp · 2026-11-07
- Computer-Using World Model：让 GUI 智能体在执行前预演行动后果 — burkov · 2026-11-07
- opentel-mcp v0.18 发布:SHA-256 哈希检测 MCP 工具「rug pull」攻击 — Thirumalaiboobathi · 2026-11-07
- Uncle Bob 用覆盖率与变异测试给编码智能体上枷锁 — bibryam · 2026-11-07
- “是不会还是不想？”：用户质问 agent 后它当场认怂 — StewartalsopIII · 2026-11-07