# Research positions on Isabelle verification of Agentic seL4

**URL:** <https://discourse.rocq-prover.org/t/research-positions-on-isabelle-verification-of-agentic-sel4/3122>\
**Category:** Announcements\
**Tags:** jobs\
**Created:** [September 29, 2026, 11:22am UTC](https://discourse.rocq-prover.org/t/research-positions-on-isabelle-verification-of-agentic-sel4/3122 "2026-09-29T11:22:30Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![andrei](https://avatars.discourse-cdn.com/v4/letter/a/9fc29f/32.png) [@andrei](https://discourse.rocq-prover.org/u/andrei)\
**Post date:** [September 29, 2026, 11:22am UTC](https://discourse.rocq-prover.org/t/research-positions-on-isabelle-verification-of-agentic-sel4/3122/1 "2026-09-29T11:22:30Z")

</div>

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:

> **[Jobs at University of Sheffield](https://jobsite.sheffield.ac.uk/job/Research-Fellow-in-AI-Assisted-Formal-Verification/3142-en_GB/)**
>
> Explore job opportunities with University of Sheffield

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](mailto: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](mailto:b.dongol@surrey.ac.uk)); for opportunities at the University of  
Melbourne, please contact Toby Murray ([toby.murray@unimelb.edu.au](mailto:toby.murray@unimelb.edu.au)).

Best wishes,  
Andrei