Skip to main content

From a verified kernel towards verified systems


Gerwin Klein



Invited extended abstract.


The L4.verified project has produced a formal, machine-checked Isabelle/HOL proof that the C code of the seL4 OS microkernel correctly implements its abstract implementation. This paper briefly summarises the proof, its main implications and assumptions, reports on the experience in conducting such a large-scale verification, and finally lays out a vision how this formally verified kernel may be used for gaining formal, code-level assurance about safety and security properties of systems on the order of a million lines of code.

BibTeX Entry

    author           = {Klein, Gerwin},
    editor           = {{Kazunori Ueda}},
    month            = nov,
    series           = {Lecture Notes in Computer Science},
    year             = {2010},
    keywords         = {sel4, isabelle, os verification},
    address          = {Shanghai, China},
    title            = {From a Verified Kernel Towards Verified Systems},
    pages            = {21--33},
    volume           = {6461},
    booktitle        = {Asian Symposium on Programming Languages and Systems (APLAS)},
    paperurl         = {},
    publisher        = {Springer},
    isbn             = {3-642-17163-X}


Served by Apache on Linux on seL4.