TLA+ is fear driven development. If you have any fears that your TLA+ model or proofs might have been written wrong, your job is to encode those fears as furth

TLA+ is fear driven development. If you have any fears that your TLA+ model or proofs might have been written wrong, your job is to encode those fears as further TLA+ proofs. The last TLA+ specification I wrote was only about two pages long. The actual model was a handful of lines. A handful of definitions. And then a page and a half of proofs and proof proofs. So it's easy to look over your spec exhaustively. And if there's any part of it you aren't sure about, or think you might have written wrong, then write more proofs that show that it you can't have written it wrong that way. The IDE provides lots of feedback and ways to debug. So like learning any language, you'll spend your formative time just trying out different parts of the TLA+ semantics and introspecting the outputs to make sure the models are behaving the way you expect them to. TLA+ is very much like doing math. If you do it wrong, you get answers that don't make sense. And it's easy to check if you're doing it wrong, by doing something you _know_ is wrong. If you get a "right" answer, you know you are making a mistake or don't understand a semantic correctly. The joy is that TLA+ allows you to write out these proof proofs and have them checked every time along with the rest of your spec. > how do I decide if the most plausible cause is a bug in my code, or a bug in the spec ? Your implementation and your TLA+ model share the same state data structures (though the TLA+ model might have a simplified representation of those states, eliding unimportant details). If you suspect your spec, you just copy the broken state sequence your implementation is encountering into your TLA+ model. If the model displays the same behavior you know your spec is wrong. If it doesn't, you know your implementation is wrong.