seL4 will go open source on 29 July

Sartakov A. Vasily sartakov at
Thu Jun 5 06:23:45 CEST 2014


This is a really great news. Will you publish the haskell model and proof? 

> … via the portal This site will start accumulating info through the next few weeks, please check there for updates (or subscribe to the mailing list).
> For those who haven’t heard about seL4: 
> - it’s the latest L4 microkernel developed by NICTA. 
> - according to the performance figures on, it’s the fastest L4 kernel around (let me know if you have performance data to contribute)
> - it’s the world’s first and only OS kernel with a formal security proof, extending from high-level statements of confidentiality and integrity enforcement all the way down to the binary
> - it’s proved functionally correct (i.e. bug-free implementation of the spec)
> - it’s the first and only protected-mode OS with a complete and sound timing analysis, and as such the only credible platform on which to do hard real-time in protected mode
> - it’s the foundation for DARPA’s high-assurance UAV project (
> … and it will soon be free!

Sartakov A. Vasily
sartakov at

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 842 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <>

More information about the l4-hackers mailing list