We would like to acknowledge the help and support that we received from our research partners and collaborators during this project.

In particular, we thank the development team of the Isabelle theorem prover for their help and support. Isabelle is the main verification tool used in this project and without its maturity success would not have been possible.

We thank the folks at Galois Inc who have worked with us to develop an open source proof library and theory for fixed-size machine words (e.g. 32 bit integers).

We also would like to acknowledge the contribution of our friendly competition, the German Verisoft project with whom we share some verification technology. In particular we would like to thank Norbert Schirmer whose verification framework for imperative programs we instantiate to the C language.

On the kernel side, the OS hackers at Open Kernel Labs have kept us on track and in connection with real-world customer requirements.

Finally, we thank (and you don't see that often in a research institution) the NICTA executive team who saw through our strange formulas, believed in the project and supported it from the beginning.

Dramatis Personae (aka The Team)

The L4.verified team over time included the following persons (in alphabetical order).

  • June Andronick
    Software certification and C verification expert and our team spirit. Yes, we can!
  • Timothy Bourke
    Invaluable Isabelle tools, security proofs, and a true engineer.
  • Andrew Boyton
    PhD student, security models and proofs.
  • David Cock
    The ARM hardware model expert, hardware simulator generator generator, performance tuner, and Research Engineer gone PhD student.
  • Jeremy Dawson
    Proof libraries and word arithmetic. Proof automation.
  • Philip Derrin
    Kernel design, implementation, verification. You name it, he can do it.
  • Kai Engelhardt
    The man for refinement. Keeping us on the right track and preventing us from re-inventing too many wheels in strange shapes.
  • Kevin Elphinstone
    Senior kernel expert and lead designer. Chief OS hacker who had to bear with all the strange formulas on our whiteboards.
  • Gernot Heiser
    Chief visionary and our most demanding customer. Also NICTA ERTOS group leader, John Lion's Professor at UNSW, CTO and co-founder of Open Kernel Labs.
  • Gerwin Klein
    Project leader, management, leadership, proofs, and chief optimist.
  • Rafal Kolanski
    IPC modelling, Virtual Memory modelling, the man for Separation Logic.
  • Jia Meng
    The connection to the world of first-order and automated proof. Automated termination proofs.
  • Catherine Menon
    Refinement proofs and C state relation.
  • Michael Norrish
    The C expert. Making Isabelle read messy low-level C programs without disappearing in a cloud of logic.
  • Thomas Sewell
    Chief verification engineer. Haskell refinement framework. Tools, models, proofs, ideas, insight: ask Thomas.
  • David Tsai
    ARM11 machine and instruction model. Handwritten and generated.
  • Harvey Tuch
    The foundation. The C memory model on which everything rests. CISRA PhD prize winner.
  • Simon Winwood
    Kernel objects, Types and Retypes. C refinement framework. Who's afraid of an evil proof?