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.

The fundamental issue is that, IMhO, security classification needs to be attached to the data at the lowest level -- OS level is simply to coarse. Take for example an encrypted channel. At the OS level the channel is treated opaquely whereas at the programming language level, after decryption the authenticated data can be assigned both a different level of secrecy and trust, and it can be data dependent. Strong type systems can ensure that secret data is never accidentally leaked, nor untrusted data used in a trusted context. (For a real-life simple subset of this, see tperl).

It may be possible to build such a system on top of seL4, but seL4 isn't sufficient.

I do intend on working on this eventually. Incidentally, D. J. Bernstein recently shared a similar complaint about the state of security - the models we use have practically not advanced since the 1950es.

There was hardly any computer security in the 1950s: it was before time sharing and networking. Your cynicism is over-done.