I'll let Gernot/Gerwin provide a definitive answer here, but just point out that several (but certainly not all) aspects of the verification work have already been released under a 3-clause BSD license, including a bit-vector library, the memory model and separation logic embedding, see:
http://ertos.nicta.com.au/research/l4.verified/kmalloc.pml A future release is planned of the the later with improved support for C's structure types in the near future. Cheers, Harvey On Mon, June 11, 2007 01:39, Jonathan S. Shapiro wrote: > On Sat, 2007-06-09 at 16:38 +1000, Gernot Heiser wrote: > >> As to the future status of seL4: We have every intention of providing >> an open-source implementation of seL4, when it's ready. Whether we'll >> release a prototype or wait until we have a production version is a >> management/business decision that will be taken some time in the future. >> >> >> A release of the Haskell prototype is overdue. >> > > What are the release plans for the verification tool chain, if any? > > > > Jonathan > > > > > _______________________________________________ > L4-hurd mailing list > [email protected] > http://lists.gnu.org/mailman/listinfo/l4-hurd > > _______________________________________________ L4-hurd mailing list [email protected] http://lists.gnu.org/mailman/listinfo/l4-hurd
