[TYPES/announce] Data61 seeking Proof Engineers

[Gerwin.Klein at data61.csiro.au]

Data61 Seeking Proof Engineers
==============================

We are are hiring again!

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

Sounds too good to exist?

In the Trustworthy Systems team at Data61 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, close to the beautiful beaches of sunny Sydney,
Australia, one of the world's most liveable cities.

We are looking for multiple motivated proof engineers who want to join
our team in Sydney, move things forward, and have global impact. You
would

  - work on industrial-scale formal proofs in Isabelle/HOL
  - develop formally verified infrastructure for building secure systems
    on top of seL4
  - contribute to improved proof automation and reasoning techniques
  - apply formal proof to real-world systems and tools

To apply for this position, you should 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
  - undergraduate degree in Computer Science, Mathematics, or similar
  - ability and desire to work in a larger team

We are hiring at two levels, so if you are more qualified or
experienced than the above would suggest, you can come in as a senior
proof engineer.

If you additionally have experience

  - in software verification with an interactive theorem prover such as
    Isabelle/HOL, HOL4, 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 disabilities, and those who identify as
LGBTIQ. See https://ts.data61.csiro.au/diversity/ for more information.

Salary ranges, in AUD (plus superannuation):
- Junior Proof Engineer: 73k-93k
- Senior Proof Engineer: 97k-105k
depending on experience and qualifications.

Apply online at the following link for the Proof Engineer positions:
 - https://jobs.csiro.au/job/Sydney%2C-NSW-Proof-Engineer/518443000/
 - https://jobs.csiro.au/job/Sydney%2C-NSW-DATA-61/518441000/

Your application should include a cover letter, CV, undergraduate
transcript (if applicable), and contact information for two references.

This round of applications closes on 17 December 2018.

For any questions on these positions, please contact
Rafal.Kolanski at data61.csiro.au or June.Andronick at data61.csiro.au

The seL4 code and proof are open source. Check them out at https://seL4.systems

More information about Data61's Trustworthy Systems team at
https://ts.data61.csiro.au

There are additional proof engineering positions available on the
Cogent project. Cogent is a language we designed to ease the
verification of systems components around seL4. For expressions of
interest, see contact details on
https://ts.data61.csiro.au/projects/TS/cogent.pml

Looking to do a PhD?
Data61 and UNSW (https://www.unsw.edu.au/) offer scholarships!
See https://ts.data61.csiro.au/students/research.pml for details.