We’re going open source!

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

Time until release:

Sign up to sel4-announce     Sign up to sel4-devel

General Dynamics C4 Systems NICTA


General Dynamics C4 Systems and NICTA are pleased to announce the open sourcing of seL4, the world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement. It is still the world's most highly-assured OS.

What's being released?

It will include all of the kernel's source code, all the proofs, plus other code and proofs useful for building highly trustworthy systems. All will be under standard open-source licensing terms. More details will be posted here closer to the release date.

When is it happening?

The release will happen at noon of Tuesday, 29 July 2014 AEST (UTC+10), in celebration of International Proof Day (the fifth aniversary of the completion of seL4's functional correctness proof).

Find out more

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 more about the construction of trusted systems using kernels related to seL4, find out about the widely-deployed OKL4 Microvisor.

If you can't wait and would like to talk to the experts about using seL4 and associated technology to construct trusted systems, please contact GD.