seL4

The world’s first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement is available as open source.

Features

  • seL4 is a high-assurance, high-performance microkernel developed, maintained and formally verified by NICTA (now the Trustworthy Systems Group at Data61) and owned by General Dynamics C4 Systems. It is a member of the L4 family of microkernels, and is the world’s most advanced, highest-assured operating-system microkernel.
  • seL4’s implementation is formally (mathematically) proved correct (bug-free) against its specification, is proved to enforce strong security properties, and its operations have proved save upper bounds on their worst-case execution times.

Website: http://sel4.systems/

Source code: https://github.com/seL4/seL4

License: GPL v2


seL4 Platforms

  • ARM
  • x86
  • RISC-V

seL4 Components

  • None