Re: seL4 Availability

[Gernot Heiser]

>>>>> On Mon, 11 Jun 2007 10:28:37 +1000 (EST), address@hidden said:
h> I'll let Gernot/Gerwin provide a definitive answer here, but just point
h> out that several (but certainly not all) aspects of the verification work
h> have already been released under a 3-clause BSD license, including a
h> bit-vector library, the memory model and separation logic embedding, see:

h> http://ertos.nicta.com.au/research/l4.verified/kmalloc.pml

h> A future release is planned of the the later with improved support for C's
h> structure types in the near future.

Just to clarify: While I said that we intend to keep the kernel open
source, that doesn't mean we're committed to open-source the complete
verification. This is, again, a business decision which is heavily
dependent on factors that are simply not known at this time.

Gernot