How often is formal correctness actually used in industry applications? Is this common outside of high risk things like aerospace?

Thanks a lot for sharing this, by the way

It's not common. The problem is a combination of user demand, vendor incentives, social issues, and no legal liability. User demand kept pushing for more features, faster, and cheaper price at all cost. Quality, security, and maintenance are the consistent costs. Vendors have been pushing broken stuff intentionally since early days to make immediate profit on cost savings then more as they supply patches. They also try to ship as fast as possible to get First Mover advantage even though medium assurance methods still work with that. They spend a little time upfront to knock out lots of debugging time. Gabriel's Worse is Better essay and how much people hold onto C are examples of the social aspect where something spreads like wildfire. They then justify its failings or keep them for convenience. Lastly, the areas most prone to high assurance have regulations, policies, or legal liabilities that encourage its use whereas most vendors immunize themselves against liability with EULA's. Worse, customers seeing unreliable, insecure systems everywhere are conditioned to think that's inevitable rather than artificial and subject to change.

Note: After a big recall, the hardware field is the one exception where they have all kinds of formal verification and testing. They're big on that stuff. Not same tools as software, though, for the most part.

Far as those using it, it helps to look at what products are available and who vendors say are their customers. Look at high-assurnace plus medium as many former customers of high-assurance do medium these days due to above reasons. Even most vendors in the niche are saying "F* it..." since demand is so low. So, you get especially high-security defense, a few in private security, some banking, aerospace, trains/railways, medical, critical industrial (esp factories or SCADA), firms protecting sensitive I.P., and some randoms. The suppliers are usually defense contractors (BAE's XTS-400, Rockwell-Collins AAMP7G); small teams in some big companies (eg IBM Caernarvon, Microsoft VerveOS); and small firms differentiating with quality & security (Altran/Praxis, Galois, Sentinel HYDRA, Secure64's SourceT).

Here's some examples. Some have marketing teams in overdrive. Just ignore it for use-cases, customers, and technical aspects. ;) Altran comes first as they focus on high quality or effectiveness for premium pay, with some high-assurance. Probably a model company for this sort of thing. AdaCore lists lots of examples which are actual customers. Esterel has a DSL with certified, code generator that has plenty uptake. INTEGRITY links show common industries & specific solutions that keep popping up on security side. NonStop is highly-assured for availability with reading materials probably having customer info. Last one is a railway showing B-method, most common in that domain, doing its job. Hope this list is helpful. I can't do much better in a hurry since the field is so scattered and with little self-reporting.

http://www.altran.com/

http://www.adacore.com/customers

http://www.esterel-technologies.com/success-stories/

http://integrityglobalsecurity.com/pages/commercial.html

http://integrityglobalsecurity.com/pages/otherSolutions.html

http://www8.hp.com/us/en/products/servers/integrity/nonstop/...

http://www.methode-b.com/wp-content/uploads/sites/7/dl/thier...

Will digest this tomorrow, thanks.