I work in Microsoft Research’s RiSE group. I am broadly interested in formal proofs for large systems via AI techniques. My past work was in the denotational semantics of programming languages and program logics, as well as zero-knowledge proofs and cryptographic compilers.