How to Write TLA+
A step-by-step introduction to TLA+ syntax, data structures, and model checking.
BlockingQueue Tutorial
A guided walkthrough of a real-world TLA+ specification: modeling a bounded blocking queue with producers and consumers.
Based on lemmy/BlockingQueue by Markus Kuppe.
Community Specifications
Beginner-friendly TLA+ specifications from the community. Browse the source, read the explanation, and explore the models.
CarTalkPuzzle
Leslie Lamport
CoffeeCan
Andrew Helwer
DieHard
Leslie Lamport
DiningPhilosophers
Jeff Hemphill
LearnProofs
Andrew Helwer
LoopInvariance
Leslie Lamport
Majority
Stephan Merz
MissionariesAndCannibals
Leslie Lamport
Moving Cat Puzzle
Florian Schanda
N Queens
Stephan Merz
Prisoners
Leslie Lamport
Prisoners Single Switch
Florian Schanda
SpecifyingSystems
Leslie Lamport
Stones
Leslie Lamport
TeachingConcurrency
Leslie Lamport
ewd687a
Leslie Lamport, Markus Kuppe, Stephan Merz
sums even
Martin Riener
tower of hanoi
Alexander Niederbühl, Markus Kuppe