List of TLA+ Examples

People always tell me that the hardest part of learning TLA+ is finding good examples. This makes sense to me: most of the main ones out there are either toy problems or immensely complex algorithms. It’s sort of the nature of TLA+: if you’re using it, you’re trying to design something complicated, and that’s usually because you’re trying to sell something complicated.

Also, the community is tiny. You could probably fit all of the TLA+ experts in the world in a small coffee shop.¹ Not a whole lot of people producing examples + most examples being proprietary = not enough to learn from.

I assembled all of the available ‘industrial’ examples I knew about. They’re all beginner to moderate in complexity. This excludes the ones in Specifying Systems or the Hyperbook. Ones marked with (H) are ones I made, ones marked with (T) use pure TLA+ instead of a mix of TLA+ and PlusCal.

Batch Installer (H)

Sending async batches of commands.

Redux (H)

Redux reducers with verifying a temporal property.

Zero Downtime Deployments (H)

A simple model of a deploying new code to servers where at least one server is always available to clients, and all available servers show the same code version.

Trading Algorithm

Trading boths executing trades in a simulated market, showing how it’s susceptible to flash crashes.

Detecting Linked-List Cycles

Finding cycles in linked lists.

Replicated Storage

Replicated storage system with a quorum.

Rate Limiter (H)

Independent workers hitting a rate-limited API.

Thread Pool (T)

Multiple reader and writer threads sharing a bounded queue, discovering deadlocks.

Bank Transfer (H)

Specifying a bank transfer with overdraft protection.

Finding bugs in systems through formalization

Ensuring distributed jobs go from “pending” to “completed”.

Voldemort

A spec of the Voldemort replicated storage system. Author has detailed explanations here and here.

Using TLA+ to Understand Xen VChan

Writing a TLA+ spec for an existing Vchan protocol, proving it with TLAPS, and using it to find a bug in existing code.

I’ll be adding to this list as I find and/or make more.