seL4
/ ess-ee-ELL-four /
Operating-system kernels are notoriously bug-prone, yet they are the one program everything else trusts utterly - a kernel bug can crash or compromise the whole machine. seL4 is a microkernel that answers this with the strongest assurance available: it is the first general-purpose OS kernel to have a machine-checked mathematical proof that its C implementation matches its specification, and that the specification enforces key security properties. It is small on purpose - a few thousand lines - because verification only scales to small, carefully designed code.
Concretely, seL4 is a microkernel, so it keeps almost everything out of the kernel: it provides a minimal core - threads, address spaces, inter-process communication, and capability-based access control - and pushes drivers, filesystems, and services out into ordinary user processes. On top of that small core sits the proof. The verification establishes a refinement: every behavior the C code can exhibit is a behavior the abstract specification allows, so the implementation has no behavior the spec forbids. From that, further proofs derive properties like integrity (the kernel never lets a thread modify memory it has no capability for) and confidentiality, and even that the binary the compiler produced corresponds to the verified C. Authority in seL4 flows only through capabilities - unforgeable tokens - so 'who can do what' is explicit and provable rather than ambient.
It matters as the existence proof that a real, usable OS kernel can be formally verified, and it is deployed where the cost is justified: avionics, defense, automotive, and other safety- or security-critical systems. But hold onto the caveats. The guarantees are about the kernel only, under stated assumptions - the proof assumes the hardware behaves as modeled, does not cover timing or power side-channels unless separately addressed, and says nothing about the correctness of the user-level software you build on top. seL4 gives you a trustworthy foundation; it does not make the system above it correct, and 'verified' is a precise claim about specific properties, not a blanket promise of perfection.
seL4 core (verified): threads, address spaces, IPC, capability access-control (~10k lines) proof: C implementation refines the spec; spec enforces integrity + confidentiality user space (NOT verified by this proof): drivers, filesystems, your application => a trustworthy kernel, but the software on top can still be wrong
seL4 verifies a tiny capability-based microkernel; everything above it - drivers, services, your app - is outside the proof and must be trusted or verified separately.
seL4's guarantees cover the kernel only, under explicit assumptions (hardware as modeled; no timing/power side-channel claims unless separately proven). It does not make user-level software above it correct. 'Verified' is a precise statement about specific properties of a small kernel, not a promise that the whole system is bug-free.