Nat KarmiosHe/They
Research Engineer

Hi there! I'm Nat, a research engineer in the Verified Software group at Imperial College London.

I'm currently working on Gillian, a symbolic execution platform that's parametric across target languages. My primary goal is to improve the accessibility and user experience of the Gillian platform in order broaden its user base, in the pursuit of real-world viability.

After serving multiple positions in traditional software engineering, my journey in verified software began in the final year of my undergraduate studies — I completed my final project under Prof. Philippa Gardner, introducing a visual debugger for symbolic execution and state matching in Gillian. After earning a first class MEng degree, I accepted the invitation to continue working on the Gillian platform as a research engineer.

In my free time, I love to explore the artform of video games.

Core Skills

Symbolic verification

Since early 2022, I've been immersed in the world of symbolic verification via my work on Gillian. Creating a symbolic debugger required me to step deep into this concept, both in picking apart the process of execution and state matching, and formulating clear and concise ways of communicating execution traces to a user.

Hoare & Separation Logic

My undergraduate studies involved specialist courses on Hoare Logic — including big- and small-step semantics — and Separation Logic for scalable program verification. My work frequently calls upon these principles, both in theoretical and practical contexts.

OCaml proficiency

The history of formal methods is entwined with that of OCaml. I've grown a deep appreciation for the language while working in this field, arming me with a natural understanding of advanced techniques, including the monadic programming style, and abstracting via modules and functors.


As a self-taught hobbyist, turned software engineer, turned research engineer, my experience ranges over many language paradigms — from C and Rust to Haskell and OCaml; from Java and Kotlin to Python and JavaScript. A prime example is how my symbolic debugger, introduced a second language (TypeScript) Gillian's codebase.

Full stack

In my numerous engineering roles, I've worked on applications at all levels — frontend, backend, and databases — from development to deployment, and maintaining servers thereafter. I'm well-versed in collaboration via Git and GitHub, and I'm comfortable in various development environments, whether it be Windows, Linux, WSL or Docker.

Achievements, Experience & Education

2022 - present
Research Engineer, Imperial College London
2018 - 2022
MEng Computing, Imperial College London
First class honours; transcript available upon request
Software Engineer, Netcraft
6-month placement
Software Engineer, AFS Technologies
3-month internship
Software Engineer, Bossa Studios
Freelance contract
Software Engineer, Exceedra Software
3-month internship
Oracle Certified Associate, Java SE 8 Programmer
For more information, see my CV or my LinkedIn profile.

Contact me

I can most easily be contacted at:

  • My personal e-mail, .
  • ...or failing that, my Imperial College email, .

You're more than welcome to reach out via LinkedIn, however I check it exceedingly rarely.

Special thanks to Philippa Gardner, Petar Maksimović and Sacha Ayoun for helping to form the foundation of my career in research.