Hello!

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). Over the course of the project, I reported the plurality of all-time bugs in the proof-assistant Coq because proof assistants are systematically slow when you apply them to real world problems. If we want verified security at scale, we need significantly more performant ways of generating and checking formal proofs!

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