'Back in 2009, OKLabs/NICTA announced the first formally verified
microkernel, seL4 (a member of the L4 family). Alas, it was
proprietary software. Today, that's no longer the case: seL4 has been
released under the GPLv2 (only, no "or later versions clause"
An anonymous reader writes
OSnews is reporting that the formally verified sel4 microkernel is now
open source: "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."
Source is over at Github. It supports ARM and x86 (including the
popular Beaglebone ARM board). If you have an x86 with the VT-x and
Extended Page Table extensions you can even run Linux atop seL4 (and
the seL4 website is served by Linux on seL4).'
-- source: http://developers.slashdot.org/story/14/07/29/1913259
Peter Reutemann, Dept. of Computer Science, University of Waikato, NZ
Ph. +64 (7) 858-5174