The seL4 Microkernel

Security is no excuse for poor performance!

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

Find out more

Check our FAQ an our development and verification Roadmap.

Read the white paper, Mathematically Verified Software Kernels: Raising the Bar for High Assurance Implementations.

Read the Brochure.

To stay informed, sign up for the Announcements mailing list. To participate in discussions, ask technical questions etc, sign up for the Developers mailing list.

Meanwhile, if you're interested in learning more about seL4, please check out about seL4, or the NICTA seL4 project site. More generally, you can find out about NICTA's trustworthy systems activities.

If you would like to learn how to build a system on seL4, you might want to follow the lectures and especially the seL4-based project of UNSW's Advanced Operating Systems course.


If you need professional support for your seL4-based project, NICTA and General Dynamics will be happy to provide this. Please contact us with an indication of your needs.