Real-world engagement
We collaborate with government and commercial partners to deploy our technology outside the lab. We apply our formal methods and verified software stack to solve real-world problems, with verified guarantees that are unprecedented in the industry.
Get in touch if you are interested in working with us.
Cyberattack-proof autonomous vehicles
We have an ongoing partnership with the US Defense Advanced Research Projects Agency (DARPA). In the SMACCM and HACMS projects, we demonstrated that formally verified software effectively prevents cyberattacks on embedded computers in autonomous drones, helicopters, land robots and trucks.
Cyber Assured Systems Engineering
Our current DARPA collaboration is Cyber Assured Systems Engineering (CASE). We are developing reusable design, analysis and verification tools that allow software engineers to design-in cyber resiliency when building embedded computing systems from scratch.
Secure display of classified information
We showcased seL4's verified isolation and information security capabilities in the Cross Domain Desktop Compositor (CDDC), developed with the Australian Department of Defence.
The CDDC is a device that enables military intelligence of different classification levels, located on separate computers, to be securely displayed on one screen without compromising the source networks.
Next generation hardware-software stack
We have partnered with the German company Hensoldt Cyber to build a secure computing stack on top of seL4.
Building on the open RISC-V hardware architecture, this project will strengthen the verified guarantees of seL4-based computer systems by developing them on a truly trustworthy hardware platform.
Securing self-driving vehicles
Modern cars depend heavily on internal computers. In self-driving cars, it will be even more important to guard against software crashes and cyberattacks. Having proven that verified software protects military autonomous vehicles from cyberattack, our technologies are also relevant for commercial manufacturers of autonomous cars.
We are working with organisations in this area to develop car-driving computers with the necessary functional reliability and security properties.
Aerospace
We are developing ways to retrofit seL4 to existing embedded systems, such as those in used in commercial aerospace. This will enable existing aerospace systems to benefit from our extensive formal verification, as well as upcoming support for affordable hardware resilience and advanced real-time scheduling.
seL4 in space
seL4 has flown with the QB50 project, a fleet of satellites built with commodity off-the-shelf (COTS) components.