There is nothing magical about TLA+ as a language. Leslie Lamport is a well-known
opponent of the trend of "thinking in languages" ("Thinking is not the ability to manipulate language; it’s the ability to manipulate concepts. Computer science should be about concepts, not languages."). TLA+ just has clear, well-understood and relatively standard mathematical semantics, and is a tool for rigorously reasoning about what programs do. Putting something like TLA+ into the Ethereum language for execution at runtime wouldn't currently make much sense for complexity reasons. Writing Ethereum specs in a language with built-in verification tools is a whole other matter, but as what is executed is bytecode anyway, you have no assurance that the code you're executing is the code you verified.
But yes, use TLA+ in addition to Ethereum code. A TLA+ spec is a verifiable blueprint; the code itself is the building. It is much more than a sanity-check, though. It is a verification of your design.
In addition to verifying contract design in general, TLA+ can model the Ethereum VM itself, and could be used to verify compiled Ethereum contracts. The Ethereum VM seems to be pretty thoroughly specified and is not too big, so a formal TLA+ spec seems like a very feasible and worthwhile goal. But that's a somewhat different use of the tool, although some combination of the two may be interesting as well.
The real challenge is figuring out what safety properties you'd want to verify for a contract. That is a job for the Ethereum domain experts, economists, lawyers etc..
Ron