Ive read a lot of industrial use of formal methods. If the method is easy, then almost all of them say what you said about the coding phase. I'll add that competing methods have code generators: Abstract, State Machines and B Method. ASM's look a lot like PlusCal with usability for about anything. Asmeta is one of tools with code generator. I think most doing it for B commercially use Atelier B and ProB. ProB does TLA+, too.

Now, far as TLA+-like stuff, tell them to check out SPIN model checker. It's seen more commercial use than most tools. Outperformed TLA+ in one paper but dont know if that extrapolates. Port some of your stuff to it to see what happens.