TLAPS-Bench 用 Agentic AI 找出 SlateDB WAL 读一致性 bug

tianyin_xu · x · 2026-11-05

围绕 TLAPS-Bench（用 agentic AI 为真实系统的 TLA+ 规约构建机器可检证明的 benchmark）的讨论。截图里 Confluent 首席技术专家 Jack Vanlightly 称，TLAPS-Bench 用 Astra Max 以 4 个并发写者验证其 SlateDB WAL 协议规约，发现一个读一致性 bug（3 个写者的模型检验未暴露），疑为 GC 与 put-if-absent 交互所致，且 SlateDB 实现可能同样存在；修复方案简单且已被作者验证。

tianyinxu 补充观点：TLAPS-Bench 只关注规约本身的正确性，而非规约与系统实现的一致性——后者才是形式化验证的关键难点；他强调「先把 spec 做对」本身就非易事，并坦承他们在 Specula 项目里其实把 TLA+ 滥用到了描述实现层面。