CV

Education

Galois, Inc., Principal Scientist, 2017 - Present
- Leads research projects in safety- and security-critical domains, with a particular focus on static analysis in industry, logic-based verification, concurrency verification, and software/hardware reasoning. Galois is a research company whose tools are used by NASA, AWS, and the US Department of Defense.
University of York, Anniversary Research Lecturer, 2012 - 2017
- Conducted a research-focused lectureship—roughly equivalent to an Associate Professor in the United States (see the Awards section below).
University of Cambridge, Research Associate, 2008 - 2012
- Worked on EPSRC-funded research projects with Dr. M. Parkinson and Prof. P. Sewell.

Scientific lead on multiple research programs and commercial engagements in formal verification, security, and AI-driven reasoning:

Verified cryptographic systems (AWS). Led formal verification of core components of Amazon’s s2n-TLS and AWS-LibCrypto libraries—among the first deployments of formally verified cryptography in production at scale—using SAW, Galois’s cryptographic verification tool.
Verification tooling (Apple). Led Galois’s work building Isabelle support for SAW to support Apple’s formal verification of corecrypto.
AI benchmarking (UK ARIA). Led development of FV-Spec, an AI benchmark for the UK Advanced Research and Invention Agency, consisting of 5,000+ formal verification challenge problems synthesised from real-world use cases.
Usable verification tools (DARPA PROVERS). Led an 8-organisation industry-academic collaboration building formal verification tools for national security applications. Hardened and scaled CN, a verification tool for C, with the University of Cambridge.
C-to-Rust translation (DARPA TRACTOR/ALLSTAR). Led Galois’s work translating C codebases to secure idiomatic Rust, extending Galois’s c2rust transpiler to AI-driven translation workflows.
AI-driven formal methods (DARPA PEARLS). Led development of early AI-driven formal verification tools, including a reinforcement-learning proof synthesiser for SAW.
Safe parsing (DARPA SafeDocs). Led development of Daedalus, a language for building secure data parsers, highlighted by DARPA as a high-priority tool in their formal verification research spotlight.

Royal Society Industry Fellowship, 2015. Permanent membership of the Royal Society college of Industry Fellows, and two years of funding to collaborate with Microsoft Research Cambridge.
York Anniversary Research Lectureship, 2012. Twenty such lectureships were created at the University of York in 2012, awarded competitively across all subjects.
Imperial College Junior Research Fellowship, 2012. Ranked first among Engineering faculty applicants (declined in favour of the York lectureship).
Facebook Secure the Internet grant, 2018. Research grant: “Verified C++ Cryptography with SAW and Cryptol”.
Microsoft Research PhD Scholarship, 2016. Fully-funded PhD scholarship: “Lightweight concurrency modeling”.
London Mathematical Society grant, 2014. Collaboration grant: “A theory of correctness for weakly-ordered algorithms.”

Specifications Don’t Exist (2025). Argues that specification, not proof, is the bottleneck for scalable formal verification.
Claude Can (Sometimes) Prove It (2025). Evaluates frontier AI models on real formal verification tasks.
o3, Frontier Math, and the Future of Mathematics (2025). Analyses the implications of AI mathematical reasoning for formal methods.
Formally Verifying Industry Cryptography, IEEE Security & Privacy (2022). Describes Galois’s approach to deploying formal verification in production cryptographic systems.