Skip to main content

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.

Photo by: Gareth Halfacree

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.

Served by Apache on Linux on seL4.