Teaser text

A recognised world leader in the formal verification of systems software and developer of the first operating-system kernel with an implementation correctness proof.

Body Text

Competitive advantage

  • Unique capability in the design, implementation and formal verification of security-critical software systems


  • Truly trustworthy (unhackable) software systems with provable security properties

Successful applications

  • Cyber-retrofit of Boeing autonomous helicopter (ULB) under the DARPA HACMS program
  • Secure communication device (AltaCrypt) built by Australian company Penten and deployed in multiple defence forces
  • German company HENSOLDT Cyber developing secure solutions based on seL4

Capabilities and facilities

  • Verification of real-world software systems

Our partners

  • Boeing
  • Rockwell Aerospace
  • HENSOLDT Cyber