TLA+ can specify unambiguously the full contract terms, their pre- and post-conditions, the bytecode VM and anything else you may want to know about Ethereum code. What it cannot do is implement any of it, because it's not a programming language... To a total newbie, I'd say think about TLA+ as a software simulation system, where you can simulate both your code and anything about the environment at any level of detail as you care to know. But instead of only running specific simulations, you can ask questions like "is this property always preserved?", "can this ever happen?"
But you can't compile the simulation nor have the simulation interact with the outside world. It is a design and investigation tool that helps you build and understand software. This is why it can be especially suitable for Ethereum -- not as a replacement to anything, but precisely because everything is already built. TLA+ helps you write and understand programs regardless of the implementation language you choose.
Ron