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},
    issue            = {2104},
    journal          = {Philosophical Transactions of the Royal Society A},
    author           = {Klein, Gerwin and Andronick, June and Keller, Gabi 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.