Learn TLA+ — Learn TLA+

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!

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.

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

Leave a Comment