[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