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.Polyglot
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
First class honours; transcript available upon request
6-month placement
3-month internship
Freelance contract
3-month internship
Contact me
I can most easily be contacted at:
- My personal e-mail, nat [at] karmios [dot] com .
- ...or failing that, my Imperial College email, n.karmios [at] ic [dot] ac [dot] uk .
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.