Case Studies
Bugs Laplace finds that production CI did not
Each study reproduces a real deadlock or liveness-violation pattern Laplace surfaced under DPOR verification — with the trace, the minimal repro, and the upstream notification status.
-
qdrant (vector database) • 2026-06-27
qdrant: ProxySegment recursive read-lock & snapshot unproxify lock order
A composition audit of qdrant's ProxySegment lock-order discipline. The shipped v1.18.2 design is deadlock-free, and the two historical defects it prevents (#724 recursive read-lock, #7178 unproxify inversion) are proven reachable as counterfactuals — both already fixed and documented upstream.
case-study qdrant ProxySegment rwlock -
surrealdb (multi-model database) • 2026-06-27
surrealdb: a live-query notification read guard held across the client send
An Axiom audit of surrealdb's RPC live-query notification fan-out. The shipped HEAD discipline is deadlock-free; the historical #3987 'read-held-across-send' shape is proven reachable as an AB-BA deadlock. All three investigated issues (#3987, #5068, #5594) are closed at our pin.
case-study surrealdb database live-query -
zellij (terminal multiplexer) • 2026-06-27
zellij: a read guard held across a blocking wait froze the server
An Axiom audit of zellij's per-client route thread. Holding the session_data RwLock read guard across a blocking action-completion wait freezes the server — a real zellij 0.44.2 regression (#5141). The shipped code (post-PR #5152) drops the guard first and is deadlock-free; the counterfactual that breaks it is proven reachable.
case-study zellij rwlock lock-order
Want to compare tools head-to-head?
See the same five scenarios run on Loom, Shuttle, Stateright, and madsim on the Benchmark Comparison page.