Ran across this paper today about a pretty cool new browser, Quark:

Quark, a browser whose kernel has been implemented and verified in the Coq proof assistant. We give a specification of our kernel, show that the implementation satisfies the specification, and finally show that the specification implies several security properties, including tab non-interference, cookie integrity and confidentiality, and address bar integrity.

Let’s put this into more simple terms. Unlike standard programming practice with unit tests, which essentially test cases that the developer defines, these go one step further and prove that the base kernel of the system will do precisely what is specified and nothing else, if all of the assumptions are valid about the OS-base, etc.

This is to programming what mathematical proofs are to mathematics. A unit test suite is similar to doing scientific experiments and deducing your system matches the specs perfectly, a proof in programming is precisely the same as a proof in mathematics. It stops being a theory and starting being absolute fact.

This is pretty cool, especially since the code is all there to work with; proven (literally), and entirely open for review. Perhaps this will inspire some security types to do the same with cryptographic kernels.