Practical TLA+ Now Available

Update 2024-08-28: I’ve since released a free online book, Learn TLA+, that supersedes Practical TLA+. You can read the motivation and differences here.

I am delighted to announce that my book, Practical TLA+, is now available! When I stumbled into TLA+ in 2016 I had no idea it would so define my passions, my values, and my career. I definitely didn’t think I’d be writing a book. But 11 months and 220 pages later, here we are! This is the largest project I’ve ever done and I’m incredibly excited to share it with you all.

If this is your first time hearing about TLA+ (hello new reader!), it’s a formal specification language you can use to write blueprints of your system. By writing and testing the specification you can find complex bugs in your system in minutes as opposed to days or weeks without it. TLA+ is especially good for dealing with concurrency, easily handling everything from threads to globally distributed databases. It’s one of the most revolutionary tools I’ve ever encountered, but people assume something so powerful must be hard to learn and use.

I mean to change that. Practical TLA+ is designed to take you from a complete outsider in formal methods to a happy user at your day-to-day job. The first six chapters cover most of the syntax and semantics, which by itself would be a solid introduction to TLA+. But part two is where the book really shines: it’s all about using TLA+. It covers all sorts of different approaches, techniques, and pitfalls to writing specs. Everything from fleshing out abstract specs to modeling adversarial agents to why you always want a TypeInvariant.

The book is also designed to be accessible. My technical editor and I went through the book together, line by line, making sure every explanation was clear and every step was explained. On average, we spent a half hour on each page. I honestly believe this is the best introduction to TLA+ available.

That’s enough from me. Thank you so much for reading, and I hope you enjoy the book.

I also run workshops on TLA+ and Alloy and am currently looking for clients. If you’re interested please contact me for more details.