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

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

"Velvet: A Foundational Multi-Modal Verifier for Imperative Programs in Lean."