> Besides that, they use formal proof tools, which are probably much > more complex than the code thay are trying to verify and thus have > bugs of their own. > > While formal proofs have their utility (by some accident I studied > with Peter van Emde Boas. The above famous quote comes from a letter > by Don Knuth to Peter) I don't think formal proofs have a lot of > significance when trying to verify a whole OS.
+1. Academics who produce tools which really help in the trenches and remain free to use are rare and to be treasured. It takes lots of time for those kind of formal verification systems and they are for the most part used to beef up the resume. For daily use something like LLVM warnings/errors is much more approachable, and the OpenBSD way of using such stuff daily, and sweeping the codebase for similar bugs. http://blog.llvm.org/2011/05/c-at-google-here-be-dragons.html and how LLVM is designed http://www.aosabook.org/en/llvm.html
