Senior Research Fellow on Agentic AI and Verification

The University of Surrey is looking to recruit two Senior Research Associates for a new project on formal verification, seL4 security and AI-assisted theorem proving, funded by the Advanced Research + Invention Agency (ARIA).

The project is joint with Andrei Popescu at the University of Sheffield and Toby Murray at the University of Melbourne, and has two closely connected aims. First, the project 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. Second, the project will investigate the use of modern AI techniques to accelerate large-scale formal verification, including AI proof agents for maintaining, extending and refactoring the seL4 Isabelle/HOL proof base.

The Surrey positions are full-time fixed-term until November 2027, with a start date as soon as possible. Substantial funding is available for access to state-of-the-art AI models and computing infrastructure.

About you:
We are interested in candidates with expertise in one or more of the following areas: interactive theorem proving, formal verification, information-flow security, seL4, neurosymbolic AI, and AI-assisted reasoning. Candidates do not need to cover all these areas, as researchers can focus on different parts of the project according to their expertise.

Particular preference will be given to candidates with strong Isabelle/HOL expertise (or substantial experience with related interactive theorem provers), and to candidates who are available to start as soon as possible. Excellent Isabelle researchers who may be at an earlier career stage than would normally be expected for a Senior Researcher position are also encouraged to apply.