Companies like ASML and Philips Healthcare report 40% or greater reduction in costs and time-to-market using formal methods to deliver highly reliable software control products. [...]
NASA uses the Spin model checker to develop and verify Mars rover control software – google “mars code”. Toyota, after its debacle with Camry unintended acceleration, adopted the Altran SPARK formal-methods tools to develop reliable software (toyota ada spark).
From http://www.infoq.com/news/2015/05/provably-correct-software :