Chris,
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.
Also, the CQL specification has been rewritten and is published at <http://cjheath.github.com/activefacts-cql> in case anyone is wanting that.
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!
Clifford Heath.