seL4

About seL4

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.

For detailed explanations of these terms, see our FAQ.

NICTA and GDC4S are releasing seL4 as open source in the hope that this will help everyone to build more dependable (safe, secure, reliable) computer systems.

seL4 was developed by many people over many years. There is a list of people who contributed on the website.

General Dynamics C4 Systems NICTA