It can be very costly to verify program after the fact, 250 lines of code per man-year is expensive. Program derivation is another way to do it, but it's also slow and significantly more complex process. Type systems, compilers and linters perform 'verification lite', they check statically for some easy to catch problems.
seL4 microkernel is formally verified, see: Comprehensive Formal Verification of an OS Microkernel, http://www.nicta.com.au/pub?doc=7371
It can be very costly to verify program after the fact, 250 lines of code per man-year is expensive. Program derivation is another way to do it, but it's also slow and significantly more complex process. Type systems, compilers and linters perform 'verification lite', they check statically for some easy to catch problems.