Formalising the L4 microkernel API

Rafal Kolanski and Gerwin Klein


This paper gives an overview of a pilot project on the specification and verification of the L4 high-performance microkernel. Of the three aspects examined in the project, we describe one in more detail: the formalisation of the kernel's Application Programming Interface using the B Method. We conclude that machine-supported formal verification of software is at a turning point; that it is now feasible, and desirable, to formally verify production-quality operating systems.

Online Copy

Available as [PDF]

Bibtex entry

  author =    {Rafal Kolanski and Gerwin Klein},
  title =     {Formalising the {L4} microkernel {API}},
  booktitle = {Computing: The Australasian Theory Symposium (CATS 06)},
  year =      {2006},
  editor =    {Barry Jay and Joachim Gudmundsson},
  address =   {Hobart, Australia},
  month =     Jan,
  pages =     {53--68},
  series =    {Conferences in Research and Practice in Information Technology},
  volume =    {51}
Gerwin Klein
2006-07-14 09:43:18