Actually, the high-assurance field that does such things is very small. A tiny niche of the overall industry. Most people doing embedded systems do things like the parent described. The few doing formal usually are trying to achieve a certification that wants to see (a) specific activities performed or (b) no errors. Failures mean expensive recertifications. Examples include EAL5+, esp DO-178B or DO-178C, SIL, and so on. Industries include aerospace, railways, defense, automotive, supposedly medical but I don't remember a specific one. CompSci people try formal methods on both toy, industrial, and FOSS designs all the time with some of their work benefiting stuff in the field. There's barely any uptake despite proven benefits, though. :(
For your pleasure, I did dig up a case study on using formal methods on a pacemaker since I think someone mentioned it upthread.
For your pleasure, I did dig up a case study on using formal methods on a pacemaker since I think someone mentioned it upthread.
http://www.comp.nus.edu.sg/~pat/publications/ssiri10_pacemak...
David Wheeler has the best page on tools available:
https://www.dwheeler.com/essays/high-assurance-floss.html
Here's a work-in-progress of my list of all categories of methods for improving correctness from high-assurance security that were also field-proven:
https://lobste.rs/s/mhqf7p/static_typing_will_not_save_us_fr...