seL4
More info
- Creator
- NICTA (now CSIRO Data61)
- Released
- Type
- Microkernel
- License
- GPLv2
- Website
- sel4.systems
A microkernel from the L4 family with a machine-checked proof that its C code does exactly what the specification says.
The team at Australia's NICTA published the proof in 2009: roughly 8,700 lines of C, verified in the Isabelle/HOL proof assistant against a formal specification. It took around 20 person-years — about twenty times the effort of writing the code. Later proofs showed that the compiled binary matches the source and that the kernel enforces isolation between components.
The kernel itself does almost nothing — threads, address spaces, IPC and capabilities — and everything else runs as isolated user-level processes. That suits systems where a bug costs more than the verification: in DARPA's HACMS programme it flew in an unmanned helicopter that a red team failed to take over. The code was open-sourced in 2014.