Improving system safety with Temporal Logic of Actions (TLA+)

The hardest bugs to find in distributed systems don't occur in a single operation. Two processes may each perform correctly, but in an order nobody anticipated, resulting in data disappearing. Tests typically run the interleavings the developers envision, while the bug may reside in an unconsidered one. At the scale of Depot Registry, this is no longer theoretical.

Once a system reaches a certain request volume, an improbable interleaving can become reality and occur on an uncontrollable schedule. When rebuilding the garbage collector for Depot Registry, the team employed model checking with TLA+. This approach uncovered a bug that tests and reviews had missed. Moreover, it emphasized the necessity of precise design decisions, such as storing immutable, content-addressed blobs that rely on S3 bucket versioning.

TLA+ is a language that describes systems as states and transitions. TLC is a model checker that examines every reachable state and every possible interleaving, then confirms whether invariants hold in all of them. The implementation is not written in TLA+. Instead, a simplified model that is small enough for TLC to explore exhaustively is created, closely approximating the real system.

If a bug is found in the model, it points to a bug in the actual system. A simple example is two clients withdrawing from a shared wallet, each executing a read-then-write without locking. Each action is a transition: Check(c) reads the balance, Withdraw(c) subtracts 8 if the client perceives sufficient funds. The symbols /\ (and) and \/ (or) denote logical conjunction and disjunction.

The primed variable balance represents the value in the subsequent state, while NoOverdraft is the invariant that should hold universally. TLC resolves this scenario in four steps: client A checks and observes a balance of 10, client B checks and sees 10, both perform withdrawals, and the balance becomes -6. This is the classic check-then-act race, identified mechanically through a step-by-step trace demonstrating how to reproduce it.

No test run yielded an oversight. The checker simply explores all possible orderings. The wallet example is a simplified representation. A similar concept applies to the real invariant from the registry garbage collector model. The invariant roughly translates to the following pseudocode: The final clause may appear overly permissive, stating only that an S3 version exists, not that the correct blob exists.

This is deliberate. The model incorporates a single blob digest because the race concern revolves around the garbage collector's ability to delete that blob while a manifest still requires it. In a model with multiple digests, the invariant would need to be indexed by digest: s3Versions[manifestDigest[p]] /= {}. Reviewing a model involves questioning whether decisions like this preserve the question at hand.

Modeling the moving components (uploads, database transactions, garbage collector workers), defining what must always be true, and allowing the checker to test your design against actual production traffic is essential. TLA+ has been available for decades, yet it carries a reputation issue: while everyone acknowledges its power, very few allocate the weeks required to write and maintain a precise model alongside a moving implementation.

This was the team's perspective as well. Prior to this year, a specification for their garbage collector would have lost priority every time. What changed was that they no longer write the model manually. An agent reads the implementation, translating Go transactions, SQL, and S3 calls into a specification. They then review the remainder: do the invariants accurately convey the intended meaning, and does the model abstract the necessary aspects?

Writing TLA+ represents the costly part. Defining what must always be true has always been inexpensive and remains the human responsibility. Consequently, a specification of the registry's three-tier garbage collector, encompassing concurrent pushers, two garbage collector domains, a counter reconciler, and injected counter drift—all interleaved—is now available.

It is rooted in the real implementation, transaction by transaction. TLC explores 14,290,224 distinct states in approximately 21 minutes and proves 10 safety invariants and 2 liveness properties. The most crucial invariant is the first one: a committed manifest never loses its blob data. The team now utilizes artificial intelligence to accelerate software releases, similar to other organizations, but also applies it to develop systems that are more reliable than previously verifiable implementations.

OCI registries are content-addressable. Within Depot Registry, blobs reside at blobs/sha256/digest, and the digest represents the hash of the content. Uploading the same blob twice results in byte-identical data at the same key. Nothing ever changes in place. Under this model, S3 bucket versioning seems unnecessary: every version of an object would be identical.

Garbage collection must remove blobs that no longer reference anything. The garbage collector worker marks a blob with zero references, waits for a grace period, re-verifies, and subsequently deletes it. However, the references exist in MySQL, while the bytes reside in S3, and there is no transaction spanning both systems. This creates a gap: every individual step is correct.

Yet the interleaving can delete live data. Notably, a client re-uploading a blob as it becomes garbage is not extraordinary; it occurs when a popular base image becomes inactive and is subsequently reintroduced. One could attempt to address this issue using locks or additional verification, but it is impossible to re-check S3 and delete in a single atomic step.

Instead, they made the deletion process precise. The S3 bucket is configured with versioning enabled: when a blob is re-uploaded with the same key, it becomes a new version rather than overwriting the existing one. When the garbage collector marks a blob, it records the specific S3 version ID it observed. During deletion, only that version is removed: we do not use versioning to maintain history.

Every version of a blob is byte-for-byte identical, so there is no history to preserve. Instead, versioning serves as a delete fence, transforming "delete this key" into "delete exactly the bytes I inspected," ensuring a safe race against writes. This is the solution to the puzzle in the title of this section and highlights a useful pattern for any content-addressable store that employs garbage collection: versioning, not immutable content, enables safe deletion.