Mike He

Formal Methods for and with LLM Agents

I am a Ph.D. student at the Princeton Programming Languages Group advised by Prof. Aarti Gupta. I am broadly interested in programming languages, formal methods and compilers. My current research focuses on practical formal and semi-formal methods for distributed systems and agentic systems, and I am working with the P ecosystem for verifying and reasoning about distributed systems.

Before joining Princeton, I studied at the University of Washington, where I was privileged to work with Prof. Zachary Tatlock on equality saturation and its applications to machine learning compilers.

In my free time, I enjoy playing the violin (I've been playing it longer than coding). You can find my archived recordings here.

Curriculum vitae Scholar GitHub Twitter LinkedIn

λ-Mail

Don't see it? Try running it.

Awards & honors

2026: AI for Math Fund
Organized by Renaissance Philanthropy; funded by XTX Markets.
2022: CRA Outstanding Undergraduate Researcher Award, Honorable Mention
2020: Lynn Conway Research Award (DTR Team)
2019: JASSO Scholarship, Waseda University
2018 → 2022: Annual Dean's List, University of Washington
2016: NOIp 2nd Prize, Beijing Regional

Selected Publications

Full list →

Formal Methods for Systems/LLMs

Specy: Learning Specifications for Distributed Systems from Event Traces

Mike He, Ankush Desai, Aishwarya Jagarapu, Doug Terry, Sharad Malik, Aarti Gupta

Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) · 2026

Paper Code

Soteria: Formally Verified Planning with Runtime Enforcement for Safe LLM Agents

Mike He, Ankush Desai, Sharad Malik, Aarti Gupta

Neural Information Processing Systems (NeurIPS), To Appear · 2026 Oral

crush: Extensible Proof Automation for Lean

Mike He, Dexin Zhang, Aarti Gupta

Preprint, in submission · 2026

Paper Code

LLMs for Formal Methods

Göedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification

Zenan Li*, Ziran Yang*, Deyuan He, Haoyu Zhao, Andrew Zhao, Shange Tang, Kaiyu Yang, Aarti Gupta, Zhendong Su, Chi Jin

Conference on Language Modeling (COLM) · 2026

Project Paper Code

AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms

Haoyu Zhao*, Ziran Yang*, Jiawei Li*, Deyuan He*, Zenan Li*, Chi Jin, Venugopal V. Veeravalli, Aarti Gupta, Sanjeev Arora

International Conference on Machine Learning (ICML) · 2026 Spotlight

Paper Code

Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases

Marcus Min, Mike He, Zhaoyu Li, Zixuan Yi, Sharad Malik, Aarti Gupta, Xujie Si, Osbert Bastani

International Conference on Machine Learning (ICML), Position Track · 2026 Spotlight

Paper

* denotes a core contributor.

Recent Talks

All talks →

October 2026

From Specifications to Formal Guarantees

Invited Talk @ ChipAgent

October 2026

Specy: Learning Specifications for Distributed Systems from Event Traces

OOPSLA'26

Slides

July 2026

AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms

ICML'26

Poster

Background

Full CV ↗

Education

Princeton University

2022 – est. 2027 · Princeton, NJ

Ph.D. in Computer Science
M.A. in Computer Science

Advisor: Prof. Aarti Gupta

Co-advisor: Prof. Sharad Malik

University of Washington

2018 – 2022 · Seattle, WA

B.S. in Computer Science

Advisor: Prof. Zachary Tatlock

Experience

Amazon Web Services

May 2026 – Aug 2026
Boston, MA

Applied Scientist Intern
Agentic Automated Reasoning
Mentor: Dr. Siva Somayyajula
May 2025 – Aug 2025
Santa Clara, CA

Applied Scientist Intern
Automated Reasoning Group
Mentor: Dr. Ankush Desai
May 2024 – Aug 2024
Santa Clara, CA

Applied Scientist Intern
Database System Lab
Mentor: Dr. Ankush Desai

Taichi Graphics (Now Meshy.AI)

June 2022 – Sep 2022
Remote and Beijing, China

Compiler R&D Intern
Mentor: Zhanlue Yang, Yi Xu

Strategic CAD Lab (Intel Labs)

Mar 2022 – June 2022
Remote and Hillsboro, OR

Formal Verification Research Intern
Mentor: Dr. Zhenkun Yang

Programming Language and Software Engineering Lab

Oct 2019 – June 2022
Seattle, WA

Research Assistant
Mentor: Dr. Steven Lybomirsky

Professional activities

Reviewer: NeurIPS, IEEE TMC, AAE@KDD, SciPy
Artifact Evaluation: POPL, PLDI, MLSys, MICRO

Beyond research

Violin recordings

A little more about me

I love classical music and enjoy playing the violin. I've been playing the violin for about 20 years. I received the Lv.9 certification issued by the Central Conservatory of Music when I was in middle school. You can find some of my recordings here. Some video recordings are available @ Bilibili (the website is in Chinese).
I was a part-time translator / proofreading editor in Gawr Gura's Chinese fansub team. Gura, now graduated, was a virtual streamer at YouTube affiliated with Hololive Production.
My Erdős number is 3: Mike He [3] → Sanjeev Arora [2] → László Babai [1] → Paul Erdős [0]

Friends & colleagues

In alphabetical order of last name.

Visitors from around the world

The logo of this website was designed by my friend, Melina.