Formal-verification researcher at the University of Bristol.
I work on machine-checked proofs and theorem proving in Lean 4. I maintain the Lean library Batteries and contribute actively to Mathlib.
I apply these methods to cryptography, currently the verification of post-quantum schemes such as the hash-based signature scheme XMSS. I am also increasingly interested in how AI-assisted techniques can extend the reach of formal methods.
- verify-meaning gathers the code from my dissertation, "Finding meaning in cryptographic verification". controlbits and sike-cryptol are pieces of that work.
- xmss-jasmin is some work experimenting with the use of Claude Code to produce high-assurance Jasmin implementations.