I wasn't aware that TLA+ made this part possible. How do you map from TLA+ to C++ (for example) with certainty?
... But you probably don't really want to do that. Code-level verification using any "deep specification" tool (TLA+, Coq, Isabelle, Lean, F* etc.) is extremely limited in scale compared to specifying in TLA+ at a higher level. Because there is no known way to directly verify programs larger than several thousand lines affordably, and because that's precisely the kinds of programs that most engineers need to verify most of the time, it's far more common to use TLA+ at a higher-than-code level.
However the goal isn't often to verify every single line of code. That would be prohibitively time consuming and expensive. The ideal use for this stuff is to verify the hard parts that are critical to get right. Verifying that a critical section of code will not lead to a deadlock or resource contention might be really important and so you could start with verifying that particular system.