Research positions in seL4, formal verification and AI-assisted theorem proving for agentic security at the University of Melbourne
The University of Melbourne is recruiting Postdoctoral Research Fellows / Research Fellows / Senior Research Fellows to work on the Agentic-seL4 project (https://agentic-sel4.github.io), an international collaboration with the Universities of Surrey and Sheffield. The project is developing formally verified mechanisms on top of seL4 for securely containing AI agents, together with AI-assisted verification techniques and proof agents for maintaining and extending large-scale Isabelle/HOL developments. We are interested in candidates with expertise in one or more of interactive theorem proving, formal verification, seL4, information-flow/security foundations, automated reasoning, or AI-assisted theorem proving. Experience with Isabelle/HOL is particularly relevant, but substantial experience with other proof assistants is also welcome. The positions are based at the University of Melbourne, Australia, and may be appointed at Levels A, B or C. They are fixed-term until November 2027. Visa sponsorship is possible, but preference will be given to candidates who are able to start promptly. Applications close Saturday 24 October 2026, 11:55pm Melbourne time. Full details and application: https://unimelb.wd105.myworkdayjobs.com/UoM_External_Career/job/Parkville/Postdoctoral-Research-Fellow---Research-Fellow---Senior-Research-Fellow_JR-018549 -- Dr Toby Murray, DPhil (Oxon) Professor, School of Computing and Information Systems University of Melbourne https://people.eng.unimelb.edu.au/tobym
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
