Mobile phones that can be hacked by SMS.
Cars that have more software problems than mechanical ones.
Medical implants that allow hackers to kill their hosts.
Computer viruses spreading through critical control systems and defense systems.
But it does not have to be that way.
In the seL4 verification project, we prove that our seL4 OS kernel implements its specifications correctly.
Building on state-of-the-art formal methods, our proofs provide mathematically sound, computer-checked evidence that seL4's code works correctly as described.
This makes seL4 the foundation of choice for building software systems with unprecedented security, safety, reliability and efficiency.
A detailed overview of these proof projects can be found in our journal article: Comprehensive formal verification of an OS microkernel.
We also have information on verification status for different hardware platforms.
As seL4 is continuously evolving to support new features and platforms (see the roadmap), our proofs also evolve with it.
We also work on strengthening some of the assumptions made in our proofs, especially assumptions involving hardware behaviour.
The long-term goal of our formal methods research is to formally verify programs and entire systems running on seL4, as in our trustworthy components projects. We are extending the seL4 proofs to support these projects, which are listed below.
Our Cogent language aims to simplify the verification of the device drivers and services that are needed in a modern operating system. Cogent has a formally verified toolchain, covering the entire compilation process from type-checking to low-level code output.
CakeML is a verified compiler for a high-level functional language, suitable for application-level software.
CakeML is a collaborative project by researchers at multiple institutions. Here at Trustworthy Systems, our work focuses on applying CakeML to systems programming, and verifying the behaviour of CakeML programs in the context of larger systems.
It is not enough to prove the correctness of individual components in a software system; the overall system configuration and connections also need to be correct. We are implementing automatic verification tools for our CAmkES component framework.
This is a project to verify the error-prone process of initially setting up the components of a system on seL4.
Our seL4 proofs contain nearly 1 million lines of proof steps, and continue to be expanded. To manage this complexity, we are developing a new systematic discipline of proof engineering.
As software engineering is for software, proof engineering systematically treats large-scale formal proofs, including their development, maintenance, deployment, and project management aspects.
Our work has also led to a number of additional verification tools and frameworks, mainly for the Isabelle proof assistant:
See our software page for a full list.
![]() |
![]() |
Gernot Heiser, Gerwin Klein and Toby Murray Can we prove time protection? Workshop on Hot Topics in Operating Systems (HotOS), pp. 23-29, Bertinoro, Italy, May, 2019 |
![]() |
![]() |
Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser Comprehensive formal verification of an OS microkernel ACM Transactions on Computer Systems, Volume 32, Number 1, pp. 2:1-2:70, February, 2014 |
![]() ![]() |
![]() |
Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein seL4: From general purpose to a proof of information flow enforcement IEEE Symposium on Security and Privacy, pp. 415–429, San Francisco, CA, May, 2013 |
![]() |
![]() |
Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein seL4 enforces integrity International Conference on Interactive Theorem Proving, pp. 325–340, Nijmegen, The Netherlands, August, 2011 |
![]() |
![]() |
Rafal Kolanski Verification of programs in virtual memory using separation logic PhD Thesis, UNSW, Sydney, Australia, July, 2011 |
![]() |
![]() |
Gerwin Klein From a verified kernel towards verified systems Asian Symposium on Programming Languages and Systems (APLAS), pp. 21–33, Shanghai, China, November, 2010 Invited extended abstract. |
![]() |
![]() |
Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood seL4: Formal verification of an operating-system kernel Communications of the ACM, Volume 53, Number 6, pp. 107–115, June, 2010 Research Highlights paper |
![]() ![]() |
![]() ![]() |
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood seL4: Formal verification of an OS kernel ACM Symposium on Operating Systems Principles, pp. 207–220, Big Sky, MT, USA, October, 2009 Best Paper Award Hall of Fame Award |
![]() |
![]() ![]() |
Gerwin Klein, Philip Derrin and Kevin Elphinstone Experience report: seL4 — formally verifying a high-performance microkernel Proceedings of the 14th International Conference on Functional Programming, pp. 91–96, Edinburgh, UK, August, 2009 |
![]() |
![]() |
Rafal Kolanski and Gerwin Klein Types, maps and separation logic International Conference on Theorem Proving in Higher Order Logics, pp. 276–292, Munich, Germany, August, 2009 |
![]() |
![]() |
Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock and Michael Norrish Mind the gap: A verification framework for low-level C International Conference on Theorem Proving in Higher Order Logics, pp. 500–515, Munich, Germany, August, 2009 |
![]() |
![]() |
Rafal Kolanski and Gerwin Klein Mapped separation logic Verified Software: Theories, Tools and Experiments, pp. 15–29, Toronto, Canada, October, 2008 |
![]() |
![]() |
Harvey Tuch Formal memory models for verifying C systems code PhD Thesis, UNSW, Sydney, Australia, August, 2008 |
![]() |
![]() |
Rafal Kolanski A logic for virtual memory Systems Software Verification, pp. 61–77, Sydney, Australia, July, 2008 |
![]() |
![]() |
Gernot Heiser Trusted ⇐ trustworthy ⇐ proof – Position paper Proceedings of the 2nd Conference on Future of Trust in Computing, pp. 55–59, Berlin, DE, May, 2008 |
![]() |
![]() |
Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein and Stefan M. Petters Towards trustworthy computing systems: Taking microkernels to the next level ACM Operating Systems Review, Volume 41, Number 4, pp. 3–11, December, 2007 |
![]() |
![]() |
Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe and Gernot Heiser Towards a practical, verified kernel Workshop on Hot Topics in Operating Systems (HotOS), pp. 6, San Diego, CA, USA, May, 2007 |
![]() |
![]() |
Gerwin Klein, Michael Norrish, Kevin Elphinstone and Gernot Heiser Verifying a high-performance micro-kernel 7th Annual High-Confidence Software and Systems Conference, Baltimore, MD, USA, May, 2007 |
![]() |
![]() |
Harvey Tuch, Gerwin Klein and Michael Norrish Types, bytes, and separation logic ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 97–108, Nice, France, January, 2007 |
![]() |
![]() |
Philip Derrin, Kevin Elphinstone, Gerwin Klein, David Cock and Manuel M. T. Chakravarty Running the manual: An approach to high-assurance microkernel development Proceedings of the ACM SIGPLAN Haskell Workshop, Portland, OR, USA, September, 2006 |
![]() |
![]() |
Kevin Elphinstone, Gerwin Klein and Rafal Kolanski Formalising a high-performance microkernel Verified Software: Theories, Tools and Experiments, pp. 1-7, Seattle, USA, August, 2006 |
![]() |
![]() |
Gerwin Klein and Rafal Kolanski Formalising the L4 microkernel API Computing: The Australasian Theory Symposium (CATS), pp. 53–68, Hobart, Australia, January, 2006 |
![]() |
![]() |
Harvey Tuch and Gerwin Klein A unified memory model for pointers Proceedings of the 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 474–488, Montego Bay, Jamaica, December, 2005 |
![]() |
![]() |
Kevin Elphinstone, Gernot Heiser, Ralf Huuck, Stefan M. Petters and Sergio Ruocco L4cars 3rd Embedded Security in Cars Conference (escar), Cologne, DE, November, 2005 |
![]() |
![]() |
Harvey Tuch, Gerwin Klein and Gernot Heiser OS verification — now! Proceedings of the 10th Workshop on Hot Topics in Operating Systems (HotOS), pp. 7–12, Santa Fe, NM, USA, June, 2005 |
![]() |
![]() |
Rafal Kolanski A formal model of the L4 micro-kernel API using the B method Technical Report Technical Report 05-00029-1, NICTA, 2005 |
![]() |
![]() |
Kevin Elphinstone Future directions in the evolution of the L4 microkernel Proceedings of the NICTA workshop on OS verification 2004, Technical Report 0401005T-1, Sydney, Australia, October, 2004 |
![]() |
![]() |
Harvey Tuch and Gerwin Klein Verifying the L4 virtual memory subsystem Proceedings of the NICTA workshop on OS verification 2004, Technical Report 0401005T-1, pp. 73–97, Sydney, Australia, October, 2004 |
![]() |
![]() |
Gerwin Klein and Harvey Tuch Towards verified virtual memory in L4 TPHOLs Emerging Trends '04, pp. 16 pages, Park City, Utah, USA, September, 2004 |