I'm Jamie Wright, a PhD student in the Security Of Advanced Systems/Foundations Of Logic group at the University of Sheffield. My primary research interests are formal methods for security and proof-theoretic approaches, particularly in Isabelle/HOL under the supervision of Dr. Andrei Popescu. I'm currently working on the COVERT project (alongside collaborators in Kent/Surrey), which aims to provide reusable models, tools and techniques that enable the verification of safety and security properties over a range of advanced architectures. Alongside this work, I am collaborating with Liron Cohen and Reuben Rowe on formalising Infinite Descent, with long-term plans to develop an object logic/Sledgehammer-like tool for Isabelle that integrates this soundness principle. I'm grateful to have my studies fully funded by the EPSRC Doctoral Training Partnership (DTP).

Previously, I completed my BSc(Hons I) in Computer Science and Mathematics w/ Year in Industry at the University Of Sheffield. My dissertation involved abstracting a generic two-player game and characterising a general winning strategy - formalised in Isabelle/HOL - with potential for instantiation in games such as Chess. have also worked alongside Dr. James Cranch on utilising the SAGE Maths extension of Python to solve Olympiad maths questions in the context of Euclidean Geometry, under the SURE research scheme.

Beyond my research, I am also a passionate teacher, with over 5 years of formal experience, delivering seminars up to a Master's level in Computer Science, and undergraduate in Mathematics. My teaching interests (in part) cover Logic, Programming Languages, Algebra and Piano.

Outside of work, I am a passionate musician, having achieved Grade 5 in both music theory and practical piano, alongside being an avid climber.

News

04/25

MGS Co-organiser

In April 2025, I helped co-organise the Midlands Graduate School which took place in Sheffield.

02/25

Research Visit To Cornell

From January to February 2025, I was honoured to be invited to Cornell to work with Dr. Liron Cohen on formalising Infinite Descent.

09/24

ITP/Isabelle Workshop 2024 presenter

In September 2024, I was proud to be accepted as a presenter for the Isabelle Workshop associated with ITP in Tblisi, Georgia. I presented my work on a formalised programming language with speculative execution

08/24

VeTSS Summer School

I was accepted to and attended the VeTSS summer school which took place in Bristol

07/24

CSF 2024 presenter

In July 2024, I was in attendance at CSF 2024, presenting work on Relative Security

2022-25

Development Of Secure Software TA

For the past 3 spring terms I have been leading seminars for the COM6105 Development of Secure Software module.

24/25

Logic In Computer Science TA

For the 24/25 spring term I have been a teaching assistant for COM2107 Logic in Computer Science module, running seminars each week.

Recreational Achievements

07/22

Captained University Chess Team to Division title

In 2022, I proudly captained the University B team to win the Division 4 League (Sheffield & District Chess Association)

06/25

Charity Cup Win

In June 2025, I was a winner with the Music Culture Society for a one day charity cup.

05/25

Quarter Finals of knockout cup reached/3rd Place

In 2025, I was the goalkeeper for the Music Culture Society, where we reached the Quarter Final stage of a football knockout tournament alongside finishing 3rd in the league.