It's been going on in safety-critical field with groups like Rockwell-Collins and Eschersoft extracting to Ada/SPARK. Rockwell also compiles formally-verified CPU, the AAMP7G. My proposal was to extract to SPARK, Rust, C, and Java simultaneously since all the best static verifiers are for those. What one misses other will likely catch.
I work outside defense industry on purpose. No discomfort at all. ;) The remains of high-assurance safety and security fields are mostly used for defense (esp guards), aerospace, trains, private high-security, some industrial control (esp energy), some space, some medical, and plenty academics. Far as this conversation, here's an example of what I was talking about that mentions many others:
Specware from Kesterel Institute, like lots of their stuff, is pretty cool but I think efficiency dictates manual derivation of code. Gets you close to it, though.
Note: There's also been hardware synthesis from PVS and HOL specs. Most cool stuff like that is hard to get legally due to ACM/IEEE/Spring BS. I mention it so you know it's been done. I even saw one manual, formal verification of standard cells themselves. Getting close to the bottom. If my brain was whole, I'd be pulling out solid-state, physics books & doing HOL models of process nodes' molecules to get a jump on their asses lol.
