Although TLA+ can't, that is used extensively in some other tools like the B method, Circus for concurrency, Eshersoft's Perfect, and some provers (Isabelle/Coq

Although TLA+ can't, that is used extensively in some other tools like the B method, Circus for concurrency, Eshersoft's Perfect, and some provers (Isabelle/Coq). That's a good thing in my book for critical software given it knocks out errors people introduce in implementations. The only drawback is it creates simplistic code that might not be what you're wanting in performance, readability, or even security (eg side channels). Even with those drawbacks, it can become a reference implementation to equivalence check/test your hand-coded implementation against. In security, one might also mix verified/hardened implementations for untrusted input and optimized ones for trusted inputs if they come from separate, authenticated places. Lots of tradeoffs one can make with spec-to-code generation. TLA+ just isn't in that game for most languages yet. Fortunately, it's straight-forward to convert TLA+ specs to code. Thinking about how to model or fix your algorithm is where the trouble will be. ;)