Skip to main content


Provably trustworthy systems


Gerwin Klein, June Andronick, Gabriele Keller, Daniel Matichuk and Toby Murray



We present recent work on building trustworthy systems with formal proof from the ground up, including the operating system kernel, at the level binary machine code. In particular, we give a brief overview of the seL4 microkernel verification and how it can be used to build verified systems. We show two complementary techniques for scaling these methods to larger systems: proof engineering, and code/proof co-generation.

BibTeX Entry

    publisher        = {The Royal Society Publishing},
    doi              = {10.1098/rsta.2015.0404},
    journal          = {Philosophical Transactions of the Royal SocietyA},
    author           = {Klein, Gerwin and Andronick, June and Keller, Gabriele and Matichuk, Daniel and Murray, Toby},
    month            = sep,
    volume           = {375},
    keywords         = {sel4, proof engineering, code/proof co-generation, cogent, isabelle/hol},
    year             = {2017},
    date             = {2017-9-4},
    title            = {Provably Trustworthy Systems},
    pages            = {1-23}


Served by Apache on Linux on seL4.