Association for Computing Machinery
Complete formal verification is the only known way to guarantee that a system is free of programming errors. The authors present their experience in performing the formal, machine-checked verification of the seL4 microkernel from an abstract specification down to its C implementation. They assume correctness of compiler, assembly code, and hardware and they used a unique design approach that fuses formal and operating systems techniques. To their knowledge, this is the first formal proof of functional correctness of a complete, general-purpose operating-system kernel.