I recently completed my PhD at Princeton University, advised by Andrew Appel. In August 2025, I will be joining the AWS Automated Reasoning Group as an Applied Scientist.

My research interests include formal verification, proof assistants, algorithms, and functional programming. I am especially interested in ways of combining automated and interactive proof methods to make program verification easier without sacrificing foundational guarantees.

In my thesis, I developed a verified compiler for the Why3 intermediate verification language. Previously, I verified a real-world error-correction system for network packets written in C using Coq and the Verified Software Toolchain.

From 2022-2025, I was an intern at Sandia National Labs, where I formalized the semantics of Why3 in Coq.

In summer 2021, I was an Applied Scientist Intern in the AWS Identity Automated Reasoning Group, where I used Dafny to verify parts of the IAM policy evaluator.