"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 includes all of the kernel's source code, all the proofs, plus other code and proofs useful for building highly trustworthy systems. All is under standard open-source licensing terms — either GPL version 2, or the 2-clause BSD licence.
When is it happening?
The release happened 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)."
EDIT: The original link should probably be updated to http://sel4.systems/ as it has the link to the Github page prominently displayed there.
From http://sel4.systems/ :
"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 includes all of the kernel's source code, all the proofs, plus other code and proofs useful for building highly trustworthy systems. All is under standard open-source licensing terms — either GPL version 2, or the 2-clause BSD licence.
When is it happening?
The release happened 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)."
EDIT: The original link should probably be updated to http://sel4.systems/ as it has the link to the Github page prominently displayed there.