Formal specifications have been used successfully. I'm reminded of this article I read: http://cacm.acm.org/magazines/2010/6/92498-sel4-formal-verification-of-

Formal specifications have been used successfully. I'm reminded of this article I read: http://cacm.acm.org/magazines/2010/6/92498-sel4-formal-verification-of-an-operating-system-kernel/abstract http://cacm.acm.org/magazines/2010/6/92498-sel4-formal-verif... Unfortunately it's not freely available, but here is one paragraph from the introduction: "Here, we report on the full formal verification of a critical system from a high-level model down to very low-level C code. We do not pretend that this solves all of the software complexity or error problems. We do think that our approach will work for similar systems. The main message we wish to convey is that a formally verified commercial-grade, general-purpose microkernel now exists, and that formal verification is possible and feasible on code sizes of about 10,000 lines of C. It is not cheap; we spent significant effort on the verification, but it appears cost-effective and more affordable than other methods that achieve lower degrees of trustworthiness." It was an interesting article and the process they use is not typical. If I remember correctly, they use theorem proving tools, prototype in haskell, and ultimately convert that to C. They claim that Haskell seemed to save them time and their man-hours ultimately were similar to other more traditional micro-kernel efforts. Edit: That said, if it is indeed practical to do this, it is only on a small subset of programming work, at least at this time. Edit 2: I found a version that is freely available: http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf I'm not sure if it is exactly the same as the ACM piece, but it is very close.