In 2009, the L4.verified project delivered a machine-checked, formal proof that the C code of the seL4 microkernel correctly implements its abstract specification. This proof measured roughly 200,00 lines of proof script in the interactive theorem prover Isabelle/HOL. In the years since then, the kernel has been publicly released for evaluation and teaching, has undergone API evolution, and has been even more deeply analyzed, including:
