Public release of seL4

Gernot Heiser gernot at cse.unsw.edu.au
Wed Feb 2 07:09:11 CET 2011


NICTA and Open Kernel Labs have jointly released seL4. For those not aware of seL4, it is an L4 microkernel which is formally verified (meaning that the implementation is mathematically proven to conform to the specification). It is the world's first (and only) OS kernel that is formally verified in this strict sense.

The public release includes the formal specification of the kernel (ARM version), kernel binaries for x86 and ARM, and a para-virtualized Linux running on top of seL4/x86.

More about seL4: http://ertos.nicta.com.au/research/sel4/
NICTA download site: http://ertos.nicta.com.au/software/seL4/home.pyl

Gernot





More information about the l4-hackers mailing list