Publications

[1] Certifying the Judge: Falsifiable Properties for LLM-Based Evaluation of Formal Code

Ethan S Hersch, Brando Miranda, Elyas Obbad, Srivatsava Daruru, Kirill Acharya, Zixiao Jolene Wang, Steven Dillmann, Yegor Denisov-Blanch, Sanmi Koyejo

Under review at ICML 2026 Workshop on Deep Learning for Code, 2026

First-author paper on falsifiable properties for LLM-based evaluation of formal code.

Recommended citation: Ethan S Hersch, Brando Miranda, Elyas Obbad, Srivatsava Daruru, Kirill Acharya, Zixiao Jolene Wang, Steven Dillmann, Yegor Denisov-Blanch, Sanmi Koyejo. "Certifying the Judge: Falsifiable Properties for LLM-Based Evaluation of Formal Code." Under review at the ICML 2026 Workshop on Deep Learning for Code.

[2] VeriBench: End-to-End Formal Verification Benchmark for AI Coding Agents in Lean 4

Brando Miranda, Srivatsava Daruru, Ethan S Hersch, Zhanke Zhou, Allen Nie, Daneshvar Amrollahi, Leni Aniva, Iddah Mlauzi, Kirill Acharya, Elyas Obbad, Dilara Soylu, Weston Kirk, Zixiao Jolene Wang, Kai Fronsdal, Ying Li, Donald Poindexter Jr, Rakshit Kaushik, Shurui Liu, Yegor Denisov-Blanch, Steven Dillmann, Simon Obstbaum, Santiago Cuellar, John Sarracino, Rylan Schaeffer, Mo Tiwari, Donghyun Lee, Bo Han, Sanmi Koyejo

Under review at NeurIPS 2026, 2026

Third-author paper on an end-to-end formal verification benchmark for AI coding agents in Lean 4.

Technical Blog Post

Recommended citation: Brando Miranda, Srivatsava Daruru, Ethan S Hersch, Zhanke Zhou, Allen Nie, Daneshvar Amrollahi, Leni Aniva, Iddah Mlauzi, Kirill Acharya, Elyas Obbad, Dilara Soylu, Weston Kirk, Zixiao Jolene Wang, Kai Fronsdal, Ying Li, Donald Poindexter Jr, Rakshit Kaushik, Shurui Liu, Yegor Denisov-Blanch, Steven Dillmann, Simon Obstbaum, Santiago Cuellar, John Sarracino, Rylan Schaeffer, Mo Tiwari, Donghyun Lee, Bo Han, Sanmi Koyejo. "VeriBench: End-to-End Formal Verification Benchmark for AI Coding Agents in Lean 4." Under review at NeurIPS 2026.