"We present our experience in performing the formal, machine-checked verification of the seL4 microkernel from an abstract specification down to its C implement

"We present our experience in performing the formal, machine-checked verification of the seL4 microkernel from an abstract specification down to its C implementation." http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf Of course they might have improved on that later, this paper is ~5 years old now.