Looking back at this I wish it had not taken me so long to understand it. Having now played with TLA+, I think everything you've said is spot-on.
However I think that for designing and implementing real systems, a more humanised approach than TLA+ is needed to defining operations. I've written to you privately about the "decision/action" extensions to CQL, which I think others here might wish to enquire about. I won't dump my thoughts into this old thread, but just mention that I'm still thinking about this problem. Rather than merely verifying the code, the specification could be generated to a guaranteed-correct implementation. With the operations defined in the syntax of the model, any error scenarios that TLA+ finds could also be verbalised. In other words, it could explain in English why your code is wrong and how it will fail.
Further, on verbalisation, I have now received a copy of the PhD thesis by Shin Huey where she developed ORMv2 verbalisations for Mandarin and Malay. It was a more difficult problem even than Terry Halpin expected, but it is done!