dqlite Escapes 16‑Year SQLite WAL Bug Thanks to TLA+ Verification
A 16‑year‑old SQLite WAL checkpoint bug that can corrupt databases was finally fixed. Using TLA+ the dqlite team modeled both SQLite and their own wrapper to confirm the bug cannot trigger in dqlite, avoiding costly data loss. The exercise shows formal methods can safely validate complex storage stacks.