Note
There aren’t a whole lot of examples uploaded yet. I’ll be writing more as I continue to work on the site. In the meantime, here are some good examples from around the web!
TLA+ Example Repository: The official repo, mostly abstract algorithms and protocols.
The Tortoise and Hare in TLA+: That finding cycles in a linked list algorithm question, formally modeled.
Message Queues: Pubsub implementations with topics readers subscribe to.
Thread Bounded Queue: finding a deadlock in a bounded queue, where writers trying to write a full queue are temporarily put to sleep.
Adversarial Modeling: A short example of splitting a spec into “machine” and “world” components, where the world acts as an adversary against the machine.
Batch uploader: The first spec I wrote in production!
Payment Handler: Like the wire example in the conceptual overview, except in real life.
See also Introduction to Formal Pragmatic Modeling, which is an in-depth discussion of three large production-level specifications.