I recently completed my PhD at Princeton University, advised by Andrew Appel. In Summer 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, with the eventual goal of a foundationally verified, SMT-based C program verifier. Previously, I have worked on verifying an error-correction system for network packets written in C using Coq and the Verified Software Toolchain, as well as briefly on verified numerical methods as part of the VeriNum project.

I received my BA in math and computer science and my MSE in computer science from the University of Pennsylvania in 2020. During my undergrad, I worked with Stephanie Weirich on verifying Haskell code in Coq using hs-to-coq and with Sanjeev Khanna on distributed graph algorithms.

Since summer 2022, I have interned at Sandia National Labs, where I have worked on a formalization of the Why3 intermediate verification language in Coq.

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