Note

Welcome to Learn TLA+! This is still a work in progress, please see What’s New for updates and please raise any questions or concerns at the github repo. I’d love to hear your feedback!

(In the meantime, you can find the old version at old.learntla.com.)

Learn TLA+

Most software flaws come from one of two places. A code bug is when the code doesn’t match our design— for example, an off-by-one error, or a null dereference. We have lots of techniques for finding code bugs. But what about design flaws? When it comes to bugs in our designs, we’re just taught to “think about it really hard”.

TLA+ is a “formal specification language”, a means of designing systems that lets you directly test those designs. Developed by the Turing award-winner Leslie Lamport, TLA+ has been endorsed by companies like AWS, Microsoft, and CrowdStrike. TLA+ doesn’t replace our engineering skill but augments it. With TLA+ we can design systems faster and more confidently. Check out the Conceptual Overview to see an example of this in practice.

About this guide

This is a free online resource for learning TLA+. To help both beginners and experienced users, the guide is divided into three parts:

  • The Core: a linear introduction to all of the TLA+ language. It starts with basic operators and gradually progresses all the way to advanced topics. The core is intended to be read linearly: people new to TLA+ should start with the conceptual overview and then work forward from there. People comfortable with TLA+ should skim until they find new material.

  • Topics: “Optional” advanced material. Any individual lesson will be useful to many but not all TLA+ users. Unlike the core, these are designed to be mostly independent of each other. If topics have dependencies on other topics, I will call them out.

  • Examples: Applications of TLA+ to specs, showing both how to write and understand specs.

This guide is still under development, check What’s New to see most recent updates and the roadmap to see what I’m currently working on.

About Me

I’m Hillel. I’m part of the TLA+ foundation and the author of the book Practical TLA+. I wrote this because I want TLA+ to be as accessible as possible and didn’t like that my book cost money. I have a blog and a weekly newsletter.

(Full disclosure, I’m also a professional TLA+ consultant and <plug>run workshops</plug>.)