Skip to main content


Formal verification at scale


Gerwin Klein, June Andronick, Ihor Kuz, Toby Murray, Gernot Heiser and Matthew Fernandez




We present a method for building specific classes of provably trustworthy systems with minimal proof effort. The method concentrates proof effort at the architecture level, providing security and correctness theorems at the binary level. We illustrate how this method can be applied not only to building new systems but also to retrofitting existing systems, such as the mission computer of an autonomous helicopter. We build on the verified seL4 microkernel, exploit its strong security mechanisms to enforce software component boundaries, and use a component-based approach with automatic code/proof co-generation to enforce system-level security and correct kernel configuration. After the initial investment into kernel verification and component framework verification, the proofs for such systems can be almost entirely automatic.

BibTeX Entry

    publisher        = {ACM},
    author           = {Klein, Gerwin and Andronick, June and Kuz, Ihor and Murray, Toby and Heiser, Gernot and Fernandez,
    year             = {To appear},
    title            = {Formal Verification at Scale},
    journal          = {Communications of the ACM}


Served by Apache on Linux on seL4.