Depot Registry rebuilt its garbage collector using TLA+ model checking, which uncovered a real bug missed by tests and code reviews. The article explains how TLA+ models systems as states and transitions, with TLC exploring all possible interleavings to verify invariants. A key design insight: the registry stores immutable, content-addressed blobs and relies on S3 bucket versioning.
Background
Depot is a container registry platform. This article describes their practical adoption of formal methods (TLA+) to catch concurrency bugs in distributed systems that traditional testing cannot reliably detect.
- Source
- Lobsters
- Published
- Aug 15, 2026 at 01:12 PM
- Score
- 7.0 / 10