In a relative sense, we’ve only covered a small portion of TLA+. I tried to keep this condensed to the parts I personally find most useful, which meant most of TLA+ was left out. After all, we spent more time on functions than all of temporal logic. And we haven’t even touched entire topics, like interface refinement, or the proof system, or even what ‘temporal logic’ means!
To be honest, I don’t think I’m the right person to teach those things. I still consider myself a beginner: if you read everything in this guide, you probably now know as much as I do. If you want to learn more, you’ll have to dive in. So let’s talk about what to read next.
There’s four sources you should probably start with.
Specifying Systems: I recommended that you download a copy in the introduction, for checking things that aren’t clear in this guide. Specifying Systems is a (near) complete reference the core TLA+. There’s also the TLA+ Hyperbook, which is a work in progress but more comprehensive it what it currently covers.
TLA+2: Since Specifying Systems came out Lamport updated the TLA+ language, adding lambda functions and a proof system. This document provides an overview of those changes.
PlusCal Manual: Contains a complete specification of PlusCal, including some corners I did not talk about. Note there are two syntaxes for PlusCal: p-syntax, which we’ve been using, and c-syntax, which overloads {} to replace “do” and “end”.
TLA+ Proof System: If you’re interested in TLA+ proofs, this is the most comprehensive source.
TLA+ in Distributed Systems Class: Murat uses TLA+ as a teaching tool and has some discussions on some of his experiences with that. He has several posts on TLA+ and they’re all solid.
Lamport’s TLA+ for Spec Testing (and why you’re not using it): Real-world use case of ensuring trading bots don’t do bad things.