NICTA and Open Kernel Labs have jointly released seL4. For those not aware of seL4, it is an L4 microkernel which is formally verified (meaning that the implementation is mathematically proven to conform to the specification). It is the world's first (and only) OS kernel that is formally verified in this strict sense. The public release includes the formal specification of the kernel (ARM version), kernel binaries for x86 and ARM, and a para-virtualized Linux running on top of seL4/x86. More about seL4: http://ertos.nicta.com.au/research/sel4/ NICTA download site: http://ertos.nicta.com.au/software/seL4/home.pyl Gernot