"Certified Program Synthesis with a Multi-Modal Verifier." ASE, 2026. Joint first author.

"Velvet: A Foundational Multi-Modal Verifier for Imperative Programs in Lean." CAV, 2026 (Distinguished Paper Award).

"A Mechanically Verified Garbage Collector for OCaml." Journal of Automated Reasoning, 2025.