Stream: Announcements

Topic: Research positions on Isabelle verification of Agentic seL4


view this post on Zulip Andrei Popescu (Sep 21 2026 at 20:37):

Dear Colleagues,

We are looking to recruit a Research Fellow at the University of Sheffield 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


Last updated: Sep 30 2026 at 04:36 UTC