Overview

seL4 is the first microkernel with a formal proof; the only known way to guarantee that a system is free of programming errors.