TLA+, Time Capsules, and the Limits of Mathematical Perfection

I feel like I need to keep a boilerplate response handy for this. Over the last week, my feed has been completely saturated with people pointing to a recent Hacker News thread about Canonical using a 20-state TLA+ model to hunt down a 16-year-old WAL checkpointing bug in SQLite. The prevailing narrative treats formal methods like a magical metal detector that renders software bulletproof. Finding a concurrency bug from 2008 is an incredible feat. Conceded. But let's look at why it survived that long, and what actually happens when perfectly verified math hits the thermal noise of hyperscale production.

To understand the gap between theory and the trenches, we have to look at the missing temporal coordination Canonical identified. In their dqlite blog post, they explain the structural failure lurking inside the Write-Ahead Logging (WAL) protocol. The engineers mapped out an edge case where an active read query misses the verification step for a header's salt value. Should a background checkpoint truncate the WAL at that precise microsecond, a subsequent write can trample the memory frame, marooning the original query in a totally inconsistent version of the database.

This is exactly the kind of temporal nuance that imperative code hides. C code is an instruction set for moving bytes around physical memory. When you read a C implementation of a WAL checkpoint, you see mutexes, pointers, and while-loops, but you cannot easily see the socio-technical intent. The language simply cannot express the internal monologue of the system (I am assuming these concurrent readers will eventually drain so I can safely lock this frame...).

Let's simulate the variable that dictates this system's survival: concurrent readers, which we will define as $R$. The intended coordination dictates that any thread flushing the log back to disk must first guarantee that no active queries are touching the target pages. In a theoretical model with a strictly bounded $R$, this is an $O(R)$ waiting problem that resolves safely. But in the trenches, traffic doesn't arrive in polite, bounded batches; it arrives as a relentless distribution of Poisson arrivals, retry storms, and noisy neighbors.

The system enters a state of checkpoint starvation, severely degrading performance and breaking the illusion of linearizability.[^1] To an academic, this is a fascinating unhandled state transition. To a frustrated human operator begging for help on the SQLite forum, this mathematical flaw manifests as an infinitely expanding WAL file that devours disk space while readers are served wildly inconsistent states. When the concurrent read volume pushes the system past its structural limits, the resulting bottleneck cascades directly onto an engineer desperately trying to figure out why a database that usually ticks along nicely refuses to checkpoint.

This exposes the true value of formal modeling. Beyond acting as a bug-finder, TLA+ functions as a vital time capsule. It preserves authorial intent and concurrency invariants for the next human who inherits the system, explicitly documenting the temporal coordination that C code inherently forgets.

But that time capsule only survives up to a hard limit: the Physics Boundary.

TLA+ assumes the underlying hardware operates deterministically (i.e. any design that assumes $\epsilon == 0$). By the time your database scales to hyperscale cloud infrastructure, that assumption evaporates. Google's empirical research on silent data corruptions violently establishes this reality, demonstrating that CPUs entirely cleared by factory diagnostics will routinely botch basic arithmetic in a live environment. These defective cores might crunch billions of operations perfectly until an esoteric blend of thermal shifts, voltage fluctuations, and instruction density provokes a silent math error.

Oof.

Once we cross this line, perfectly logical software is routinely bypassed by the physical universe. Because these corruptions avoid machine checks or OS panics, the bad data silently commits to memory, poisoning the application state.

Think about the blast radius of that physical reality. Your TLA+ model mathematically proves that your 20-state WAL protocol prevents dirty reads. But when a cosmic ray flips a bit in the memory controller, or an SDC hallucinates a completely invalid pointer offset, your pristine logic executes garbage anyway. Physical hardware laughs at your formal methods.

Let’s do the math on this at scale. If an SDC occurs at a rate of $10^{-12}$ per instruction, and your fleet is executing $10^{18}$ instructions per second, you are facing a steady, predictable background radiation of absolute nonsense injected directly into your tightly coupled state machines.

This brings us to the pragmatic engineering heuristic. If formal proofs cannot protect us from the chaotic physics of the datacenter, why eat our broccoli and write them at all?

Writing TLA+ cleanly separates our logical coordination bugs from our physical hardware failures, shrinking the operational confusion when things inevitably break. When the database corrupts itself under heavy load, the time capsule of formal methods spares the operator from debugging a cosmic ray as if it were a missing lock.

Ultimately, we explicitly map these states to bound the logic we force tired operators to hold in their heads. A formal proof doesn’t protect your system from the physical universe. It protects your system's temporal intent from the humans who come next.

[^1]: Linearizability requires that operations appear to execute instantaneously at exactly one point in time, a mathematical guarantee that demands extensive, often hidden, coordination to maintain.