What I don't get about TLA+, as far as I understand, it'll "only" tell you whether or not some invariants can be violated, given the current design of your program.
While this does sound useful, it also sounds like now the problem is just shifted to coming up with proper invariants, isn't it?
For example, some sorting algorithms are very complex in the details of their implementation - but they all have the quality that given an input, the output should be the same set of elements, in order.
The invariant form would be something like: for any program state, there is eventually a state that will be reached that contains the ordered set containing input elements.
My phrasing is rough, but it is an invariant that can be expressed by TLA+
Aren't invariants essentially just a very specific "what do you want"? TLA+ doesn't know what you want the code to do. It can only tell you if it's doing it properly.
While this does sound useful, it also sounds like now the problem is just shifted to coming up with proper invariants, isn't it?