Skip to main content


Automated verification of a component platform


Matthew Fernandez, June Andronick, Gerwin Klein and Ihor Kuz




This document outlines various criteria defining the correctness of a component platform, and describes a process for automatic verification of some of these criteria for the CAmkES component platform. Generated proofs are provided for a sample system as an example of the output artefacts and their relationship to both hand written formal reasoning and generated code. Our correctness properties depend upon an interactive theorem prover and some straightforward translation tools. We consider our assumptions and resulting trusted computing base to be acceptable in a high assurance software environment.

This report is an extension to previous reports on the formalisation of the CAmkES component platform and a familiarity with these previous documents is assumed.

BibTeX Entry

    author           = {Fernandez, Matthew and Andronick, June and Klein, Gerwin and Kuz, Ihor},
    issn             = {1833-9646-9034},
    month            = aug,
    year             = {2015},
    keywords         = {camkes, sel4, autocorres},
    title            = {Automated Verification of a Component Platform},
    institution      = {NICTA and UNSW},
    address          = {Sydney, Australia}


Served by Apache on Linux on seL4.