TLA+ is a specification language. Its goal is to say exactly what the algorithm is, because an informal description in English or even pseudo-code is usually t

TLA+ is a specification language. Its goal is to say exactly what the algorithm is, because an informal description in English or even pseudo-code is usually too ambiguous and not amenable to mechanical proofs. TLA+ by itself does not prove anything. You can write incorrect algorithms in TLA+, in the same way that you can write incorrect C programs. Once you have a TLA+ specification, lazy people like me run the specification through a tool called TLC that exhaustively explores all possible behaviors of the algorithm in a finite search space. For example, the specification may say that a property is valid for all N, but TLC checks it for N=1, 2, and 3. This step is not a "proof" (it's more like a test suite), but people like me say "good enough" and ship at this point. Lamport and colleagues have a tool called TLAPS where you can write a proof yourself (e.g., valid for all N), and the tool checks that the proof proves what it claims to prove. The next step, which is what this paper is all about, is to derive the proof automatically.