I'm excited about understanding and securing software systems. My current projects are in formally verifying transformer models and using mechanistic interpretability for anomaly detection.

Previously, I developed Fiat Cryptography which enables the majority of secure connections to the internet (the big prime numbers behind the https lock icon), reported the plurality of all-time bugs in the proof-assistant Coq (and joined the dev team to help handle them!), and contributed category theory to the Coq-HoTT library (hoorah for beautiful, unifying mathematics).

The compelling observation from these projects was that proof assistants are systematically slow, and if we expect verified security to scale as fast as we deploy software in critical infrastructure, we need to be engineering significantly more performant ways of generating and checking formal proofs. I wrote this up in a dense PhD thesis in 2020.

I live in the Bay Area, and I like to sail. Reach out if you want to chat, or do water sports!