Skip to main content

Research Assistants and Junior Proof Engineers

seL4 call graph

If only there was a place where I could learn stuff, prove theorems for money, change the world, and have fun while doing it...

Sounds too good to be true?

In the Trustworthy Systems team, that's what we do for a living. We are the creators of seL4, the world's first fully formally verified operating system kernel with extreme performance and strong security & correctness proofs. Our highly international team is located on the UNSW campus in Sydney.

We are looking for entry-level research assistants and junior proof engineers who want to join our team, learn new things, move things forward, and have global impact. There are active projects around the world in

  • Automotive - because cars have been hacked enough
  • Aviation - for more security and safety for autonomous vehicles
  • Connected consumer devices - with security built in from the start
  • Spaceflight, autonomous and crewed - because awesome

To make these projects successful, we need to scale formal verification. You would learn to

  • work on industrial-scale formal proofs in Isabelle/HOL
  • help to extend and improve existing proofs or verify new features in seL4
  • contribute to improved proof automation and better reasoning techniques
  • apply formal proof to real-world systems and tools

To apply for this position, you should be an undergraduate student or fresh graduate in Computer Science or related discipline and possess a significant subset of the following skills.

  • functional programming in a language like Haskell, ML, or OCaml
  • first-order or higher-order formal logic
  • basic experience in C
  • ability and desire to quickly learn new techniques
  • ability and desire to work in a larger team

If you additionally have experience

  • in software verification with an interactive theorem prover such as Isabelle/HOL or Coq, and/or
  • with operating systems and microkernels

you should definitely apply!

If you have the right skills and background, we can provide training on the job. Continual learning is a central component of everything we do. You will work with a unique world-leading combination of OS and formal methods experts, students at undergraduate and PhD level, engineers, and researchers from 5 continents, speaking over 15 languages. Trustworthy Systems is a fun, creative, and welcoming workplace with flexible hours & work arrangements.

We value diversity in all forms and welcome applications from people of all ages, including people with a disability, and those who identify as LGBTIQ. See our diversity page for more information.

Apply by sending your CV, undergraduate transcript (if applicable), two references, and cover letter to Gerwin Klein, gerwin.klein and June Andronick, june.andronick

Served by Apache on Linux on seL4.