VeriBench asks whether AI coding agents can turn Python programs into Lean 4 code, specifications, and proofs that capture what the program is supposed to do. Simon Obstbaum is a co-author of this research.
In plain language: passing tests only checks selected examples. A formal proof can establish that a program satisfies a stated requirement across all inputs covered by that requirement. But the requirement itself must be right: proving an incomplete or trivial claim does not establish that the software does its job.
The project finds that current agents are better at producing code that compiles than at stating the full set of properties needed to verify its behavior. VeriBench measures this gap to help researchers build more trustworthy coding agents. Some assessments use a human-audited AI judge, so the benchmark score is not itself a mathematical guarantee of correctness.
