01
seL4 and the Machine-Checked Proof of a General-Purpose Microkernel
seL4 connected a high-performance microkernel implementation to a formal specification with machine-checked proofs, pushing software verification into the privileged operating-system core.
↗