Research Fellow in AI-Assisted Formal Verification

Overview

We are seeking an ambitious researcher to join a major new project funded by the Advanced Research and Invention Agency (ARIA), combining formal verification, cybersecurity and AI. The post offers an unusual opportunity to work at the intersection of Isabelle/HOL, the seL4-verified microkernel, information-flow security, and AI-assisted theorem proving.

The project aims to develop a formally verified reference monitor on top of seL4 for the secure containment of AI agents. We will develop new mechanisms for dynamically controlling agents’ capabilities and information flows, together with machine-checked security guarantees. In parallel, we will investigate how modern AI techniques can accelerate large-scale formal verification, developing AI proof agents that can maintain, extend and refactor the seL4 proof base in Isabelle/HOL.

You will join a highly collaborative international team spanning the Universities of Sheffield, Surrey and Melbourne, bringing together expertise in Isabelle/HOL, seL4, information-flow security, program logics, and neurosymbolic AI. The project is exceptionally well resourced, including substantial funding for access to state-of-the-art AI models and computing infrastructure.

We particularly welcome applicants with strong expertise in Isabelle/HOL or other interactive theorem provers, formal verification and security, or neurosymbolic AI and AI-assisted reasoning. Deep expertise in Isabelle/HOL will be especially valued, and we encourage outstanding Isabelle researchers to apply even if their career stage is less senior than might normally be expected for a Grade 8 research position.

For informal enquiries about the project or the position, please contact Professor Andrei Popescu at[email protected]

Main duties and responsibilities

• Conduct research of international standing in areas relevant to the project, including formal verification, information-flow security, interactive theorem proving, and AI-assisted reasoning.
• Independently develop and pursue technically ambitious research ideas, determining research objectives and selecting appropriate methods and approaches within the overall aims of the project.
• Take primary responsibility for substantial technical research tasks according to the postholder’s expertise, from their formulation and implementation through to evaluation and dissemination.
• Contribute to the development and formal verification of an agent-aware reference monitor on top of seL4, supporting dynamic control of the capabilities and information flows of AI agents.
• Develop and mechanise security models, program logics and information-flow properties in Isabelle/HOL, and contribute to the modernisation, extension and maintenance of the existing seL4 proof infrastructure.
• Develop and evaluate AI techniques for large-scale interactive theorem proving, potentially including supervised fine-tuning and reinforcement learning using formal verification feedback, and AI agents for proof generation, repair and refactoring.
• Contribute to the development of Isabelle infrastructure for AI-assisted theorem proving, including proof-data extraction, interaction with proof states, and integration of AI agents into Isabelle-based verification workflows.
• Work closely with researchers and research software engineers at Sheffield and with project partners at the Universities of Surrey and Melbourne, contributing to the integration of the project’s security, systems and AI components.
• Design and conduct rigorous evaluations of the resulting verification and AI techniques, including their effectiveness, robustness, scalability and maintainability on the seL4 proof base.
• Disseminate research findings through high-quality publications, presentations, software and formalisation artefacts, including presenting results at national and international conferences and project meetings.
• Contribute to the supervision and mentoring of students and junior researchers where appropriate.
• Carry out other duties, commensurate with the grade and remit of the post.

Person Specification  

Our diverse community of staff and students recognises the unique abilities, backgrounds, and beliefs of all. We foster a culture where everyone feels they belong and is respected. Even if your past experience doesn't match perfectly with this role's criteria, your contribution is valuable, and we encourage you to apply. Please ensure that you reference the application criteria in the application statement when you apply.

Criteria

Essential or desirable

Stage(s) assessed at

A PhD (or equivalent experience) in computer science or a closely related discipline. Applications from exceptional candidates who are close to completing a PhD will also be considered.

Essential

Application

Strong research expertise in at least one of the following areas: interactive theorem proving / formal verification; information-flow security / program logics; and/or AI for reasoning / neuro-symbolic AI.

Essential

Application/interview

Excellent programming and/or formalisation skills, appropriate to the candidate’s area of expertise

Essential

Application/interview

Evidence of the ability to conduct high-quality research and contribute to research publications

Essential

Application/interview

Ability to develop and pursue research ideas independently, while contributing effectively to a collaborative research programme

Essential

Application/interview

Ability to work effectively with researchers from different backgrounds, including formal methods, systems security and AI.

Essential

Application/interview

Excellent written and verbal communication skills, including the ability to communicate complex technical ideas clearly.

Essential

Application/interview

Substantial experience with Isabelle/HOL or another interactive theorem prover.

Desirable

Application/interview

Experience in one or more of seL4, information-flow security, AI-assisted theorem proving, machine learning for reasoning, or neurosymbolic AI.

Desirable

Application/interview

Further Information

Grade

Grade 8

Salary

£48,822 - £51,753

Work arrangement

Full-time

Duration

Until 30th November 2027

Line manager

Professor of Computing Foundations (project lead)

Direct reports

None

Right to work in the UK

If you do not currently hold the right to work in the UK, you can find more informationhere to help determine your visa eligibility.  Additional guidance is also available on theUK Visa & Immigration website .

For informal enquiries about this job please contact Professor Andrei Popescu, project lead, at [email protected]

Next steps in the recruitment process

It is anticipated that the selection process will take place in the week commencing 5th October. This will consist of an interview held online or in person. We plan to let candidates know if they have progressed to the selection stage on the week commencing 28th September. If you need any support, equipment or adjustments to enable you to participate in any element of the recruitment process you can contact[email protected]

Our vision and strategic plan

We are the University of Sheffield. This is our vision: sheffield.ac.uk/vision (opens in new window).

We are a Disability Confident Leader (opens in a new window). If you have a disability and meet the essential criteria for this job you will be invited to take part in the next stage of the selection process.