TLAPS-Bench and agentic AI surface a read-consistency bug in SlateDB's WAL spec
tianyin_xu · x · 2026-11-05
Discussion around TLAPS-Bench, a benchmark that uses agentic AI to build machine-checked proofs for real-world TLA+ specs. In the attached screenshot, Confluent's Jack Vanlightly reports that TLAPS-Bench, running with Astra Max and 4 competing writers, exposed a read-consistency bug in his TLA+ spec of SlateDB's WAL protocol (a 3-writer model check never showed the violation); SlateDB itself may share the bug, likely from GC complicating put-if-absent, and a simple fix was validated.
tianyinxu adds nuance: TLAPS-Bench only tests spec correctness, not conformance between the abstract model and the actual implementation — which he argues is the harder, more authentic challenge, admitting his own Specula project 'abused' TLA+ to describe implementation.
Related event: TLAPS-Bench uses agentic AI to uncover SlateDB WAL consistency bug(2 posts)→
More from coding & agent
- Levels decompiles Battlefield 1942 with Claude Code, ports it to browser with working multiplayer — huangyun_122 · 2026-11-05
- Kubernetes promotes AI Conformance to permanent SIG Architecture subproject — TerryTangYuan · 2026-11-05
- quiet.md goes open source: Rust+GPUI editor, Feishu-compatible, ~5ms frames on 1M-char docs — dotey · 2026-11-05
- A background agent that auto-structures messy scientist Excel data, day 17 of agent series — nlarusstone · 2026-11-05
- Code mode isn't about MCP: it's about whether tool results go to context or program variables — ritakozlov · 2026-11-05
- Agent Arena: frontier models show 55-minute gap on long-horizon agent tasks — arena · 2026-11-05