Formal methods is the use of formal mathematical logic to specify and prove the correctness of software systems.
We are developing mathematical models, software tools and engineering processes that can verify large, interconnected systems at all levels, from the overall design down to the executable code. Our group has demonstrated that the full formal verification of software for complex real-world domains, once thought to be practically impossible, can be achieved in reasonable time and cost.
Our goal is to build verified systems from the ground up; this begins with our formal verification of the seL4 microkernel.
We have proved that seL4's code correctly implements its functional specification, as well as important security properties—both world-first achievements. Today, we continue to extend the proofs to support new seL4 features and hardware platforms.
These are our major developments in progress (also see our seL4 roadmap).
In addition to proving the correctness of seL4's source code, we also verify that it is compiled correctly to ARM and RISC-V machine code.
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.
Using seL4 as a trustworthy base, we are building large-scale software systems with unprecedented reliability and security guarantees. We are developing new programming languages to achieve this goal.
We do research on formal models of concurrency and distributed systems. We also use these models to specify, analyse and verify concurrent software and network protocols.
Browse our FM research publications.