The University of Melbourne invites applications for a Postdoctoral Research Fellow to join the Agentic seL4 project within the Faculty of Engineering and Information Technology. You will develop AI-assisted verification techniques and contribute to Isabelle/HOL proof engineering, while supervising students and collaborating with international partners.

Ideally, you hold a PhD in formal methods or automated reasoning, with a strong publication record and expertise in interactive theorem proving,