[Caml-list] Research Fellow positions in the Isabelle development and verification of an "Agentic seL4" system -- application deadline 27 September 2026

[Caml-list] Research Fellow positions in the Isabelle development and verification of an "Agentic seL4" system -- application deadline 27 September 2026

[Andrei Popescu]

Dear Colleagues,

We are looking to recruit a Research Fellow at the University of
Sheffield, UK, for a new project on formal verification with Isabelle,
funded by the Advanced Research + Invention Agency (ARIA).

The project, jointly undertaken with the University of Surrey and the
University of Melbourne, will develop a formally verified reference
monitor on top of seL4 for the secure containment of AI agents,
including mechanisms for dynamically controlling agents’ capabilities
and information flows. It will also use AI techniques to accelerate
large-scale formal verification, trained on the seL4 proof base.

The position is at Grade 8 (UK Lecturer level), with a salary of
£53,301–£58,225, and is initially for 14 months. We have substantial
funding for access to state-of-the-art AI models and computing
infrastructure. We are interested in candidates with expertise in
interactive theorem proving, formal verification, information-flow
security, seL4, and optionally neurosymbolic AI and AI-assisted
reasoning. Candidates do not need to cover all these areas. Particular
preference will be given to candidates with strong Isabelle expertise
(or substantial experience with related interactive theorem provers),
and to candidates who are available to start as soon as possible. We
would also be very interested in hearing from excellent Isabelle
researchers who may be at an earlier career stage than would normally
be expected for a Grade 8 position.

The formal Sheffield advert and application link are available here:
https://jobsite.sheffield.ac.uk/job/Research-Fellow-in-AI-Assisted-Formal-Verification/3142-en_GB/

The application deadline is on 27/09/2026. If you are potentially
interested in the position and have any questions, please feel free to
contact me at a.popescu@sheffield.ac.uk .

There are also closely related positions at our partner institutions.
For opportunities at the University of Surrey, please contact Brijesh
Dongol (b.dongol@surrey.ac.uk); for opportunities at the University of
Melbourne, please contact Toby Murray (toby.murray@unimelb.edu.au).

Best wishes,
Andrei