You translate it yourself ;) you're a programmer, go program! More seriously, the main classes of bugs TLA+ defends against are logic hole bugs and concurrency

You translate it yourself ;) you're a programmer, go program! More seriously, the main classes of bugs TLA+ defends against are logic hole bugs and concurrency bugs - spec/design bugs, the most insidious kind! That's what AWS used it for; there is no machine-enforced correspondence with the code. People get really hung up on this, but after they try to formally verify something they see the wisdom of the separation. Proving code correct is extremely time-intensive. In contrast TLA+ gives you great bang for your buck. And to repeat - translating a TLA+ spec to code is not an error-prone process and is well, well within the grasp of software engineers.