Below are a couple of links to a paper and an article discussing the formal verification of safety-critical applications.
The first one is an article written by Boris Sedacca in the IET magazine “Verifying safety-critical aerospace and automotive applications” looking at how the current and upcoming Avionics and Automotive standards “aim to improve code verification”.
http://kn.theiet.org/magazine/issues/1013/verifying-safety-1013.cfm
The second one is a paper written by Xavier Leroy who is a member of the team at INRIA working on the CompCert project. “The paper reports on the development and formal verification (proof of semantic preservation) of CompCert, a compiler from Clight (a large subset of the C programming language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness.”
http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf