ABSTRACT:
In 2009, the L4.verified project completed the world's first verification of functional correctness for a general-purpose OS kernel [2], seL4. Functional correctness here was embodied by a formal theorem of refinement, which stated that the behavior of the C code that implemented the kernel accorded with an abstract specification of how the kernel was meant to function.
