Exploring applications of TLA+.
- crdt-bug - A subtle problem and it's solution in a CRDT algorithm posted by Martin Kleppmann on Twitter.
- aiorwlock - Based on this talk, models a bug that existed at one point in aiorwlock.
- asyncio-lock - Same idea as in aiorwlock models several bugs that have been present at some point in Python's standard library.
- dual-writes - Explores ways to create visualizations of a simple race condition.
- paxos-from-the-ground-up - WIP: Idea is to create one spec for each step in a tutorial which builds up paxos by refining a simple but wrong protocol step by step.
- tic-tac-toe - A game of tic-tac-toe of two players with different strategies. Contains ideas from other specs.
- tower-of-hanoi - Simple, heavily commented specification of a classic puzzle.
- rate-limiter - Race condition described in the redis documentation.