The spec might not even contain the level of detail necessary for that to be possible. That possibility is what makes modeling easier than implementing the spec.
Through a process of manual refinement, you can derive an implementation from the spec and check every step with the checker, but that's is more work than implementing the formal spec manually and is an most likely an overkill in practice.
People that can write proofs in Coq and Isabelle might prefer that over the TLC approach of exhaustively checking all the possible states allowed by a TLA+ spec. But writing proofs in Coq/Isabelle/Lean/HOL is a more sophisticated skill and requires even more training on the multiple theories available in these provers. The brute force approach of TLA+/TLC is more dependable as part of an engineering process. Some specs can be really hard to prove, but easy to exhaustively check.
Start looking for small opportunities to do something different and bold. Do that before you're asked to do it. Sooner or later you will get "hired" for the kind of job where you get to do the things you described here. That's how everyone else did it.
Check Regel. It's very flexible and allows you to generate code for different programming languages. It can also work with binary data. Its main application is generation of optimized network protocol scanners.
They are. I avoided introducing an explanation of Curry-Howard isomorphism because I think that would not be very intuitive to many people because the most commonly used type systems have very little power to express logical properties about the program.
I don't think it's common for programmers to have in depth opinions about type systems. And most of the ones who do may not really know what they're talking about.
Through a process of manual refinement, you can derive an implementation from the spec and check every step with the checker, but that's is more work than implementing the formal spec manually and is an most likely an overkill in practice.