[isabelle] seL4 specification released

It took some time, but NICTA and Open Kernel Labs have now released the formal Isabelle/HOL specification of the seL4 microkernel. The C code of the kernel is verified (in Isabelle) to implement this specification. The release includes ARM and x86 binaries of the kernel, documentation, user-level libraries and examples, and a paravirtualised Linux that runs on top of seL4/x86:


The specification works with Isabelle2009-2, and the release contains all files and libraries necessary to process it in Isabelle.

Please note that the release is for non-commercial only. Educational and academic research use is explicitly allowed. 


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.