[IsThisObvious]

The code generator we use (at my job; not crypto) was written in Coq and formally verified to generate code with certain properties, given properties of the input.

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.

[foobarqux]

I think in many regulated industries Coq itself would also need to be certified.

What industry is this?

[IsThisObvious]

Pressure equipment, specifically sort of mid-scale items for laboratory and small-batch use.

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.