All of TLA+ (except the proof language), how all the symbols are typed, and all of the standard modules can be found on this cheatsheet: https://lamport.azurewe

All of TLA+ (except the proof language), how all the symbols are typed, and all of the standard modules can be found on this cheatsheet: https://lamport.azurewebsites.net/tla/summary-standalone.pdf https://lamport.azurewebsites.net/tla/summary-standalone.pdf While some people prefer writing PlusCal, I don't think it's the majority. Most people I know just write TLA+. PlusCal is more suitable for "code-level" problems, like specifying low-level operations on concurrent data structures. As to your point about TLC's sometimes surprising behaviour, I agree, but "mysteriousness" is common in software tools. These are things that are learned through experience. One way to estimate how things are going, even with no experience, is to look at the graphs of newly discovered states that the Toolbox draws. If they're trending down, you're in the process of converging; if they're still going up -- you're not.