> 1. Given you have to learn the language, and, at first, you don't know it - how do you even trust that you're writing a proof right, and that you're not simpl

> 1. Given you have to learn the language, and, at first, you don't know it - how do you even trust that you're writing a proof right, and that you're not simply writing gibberish ? TDD has code execution as an "arbiter of peace". If, when calling a function, you get an unexpected result, then... you did something wrong. I write TLA+ specs in the same way I do TDD: first write an invariant or property I know I should half, then make it fail, then modify the spec to pass the invariant. > If my TLA+ set of rules holds, how do I get confidence that I wrote the right set of rules ? Ultimately, nothing can guarantee this for us, just as nothing can guarantee we wrote the right code. This is one reason why I'm a strong advocate of spec reviews. Getting another pair of eyes on the spec goes a long way. > 2. Once I've got a set of rule that I decided to trust, when I implement it and I get bugs (as demonstrated by executable code) ; how do I decide if the most plausible cause is a bug in my code, or a bug in the spec ? It depends. This has happened to me a couple of times before. In one case, it was because I forgot to include something in the spec. Adding that caused the spec to immediately fail, which corresponded to the executable bug. In another case, I was able to identify, assuming the spec was correct, where the spec-code mistmatch must have been to cause the bug. So I was able to identify the code issue much faster than without the spec. It helps that specs are usually much smaller than the corresponding codebase, so you can sweep it for issues much faster.