I know people who write crypto software that must conform to formal verification of the algorithm, requires detailed design documentation before a single line of code, etc.
I assume that the crypto group I know, who developed most of the code generator I use, takes similar measures to make sure that their verified "theorems" translate correctly to code.
The unverified stage is actually the hardware, which is an open problem.
What industry is this?
Our low level code (ie, directly controlling machines) is written in the SPARK environment. This code tends not to get updated often, and has a high level of verification to it. It's what actually handles the pressure cut-offs (ie, hard limits on the machine), turning vales, etc.
Our middleware code is based on a specially developed VM that gets code generated for it in Coq, to ensure that it doesn't choke or become unresponsive. However, it's not directly responsible for safety control and has somewhat laxer restrictions.
Coq is useful for demonstrating that the middleware analytics will complete in a given time profile and not crash out the server on erroneous input.