You are asking the wrong question. While there are various ways to check conformance to the spec, none of them guarantees it. In fact, no one knows how to do that using any tool whatsoever. People sometimes refer to end-to-end verification successes (verifying all the way from the spec to the code or even machine code) like seL4, but forget how tiny that codebase is, how long it took specialized experts to write and verify it, and what concessions had to be made to make that possible.

So let me ask you this: how do you guarantee that your tests cover all possible case? You can't (and they probably don't). So why do you use tests at all? Because the question isn't how to guarantee the software is perfect -- something we can't do, at least not currently -- but how to make it better. And just like tests can make your software better even if it's not perfect, a TLA+ specification can, too.

How do you go from a blueprint to the program? The same way you go from an algorithm in a book to a program. You can make the specification as detailed or as high-level as you like, and focus on whatever you think is the most important parts. Going from spec to code is the easy part.