Lacerta-Bench: Evaluating Provably Correct and Efficient Binary Generation

Code-generation benchmarks typically evaluate programs using finite test suites, while formal-verification benchmarks usually prove properties of source code. We study the joint evaluation of executable efficiency and machine-checked correctness of the emitted binary. We introduce Lacerta, a Lean 4 framework for reasoning about binary programs, alongside Lacerta-Bench, a benchmark built on Lacerta for evaluating binary generation from high-level specifications. Lacerta-Bench comprises 400 tasks derived from competitive-programming problems, each with a formal specification; batch tasks use a target-independent byte-stream interface. Models generate a binary program together with a machine-checked proof of its correctness, while deterministic gas ranks programs on their efficiency. We evaluate six language models on 100 problems under a 30-minute budget: only one system produces any accepted proof, on 20 problems. On ten of these problems with five eight-hour attempts each, 98% of attempts pass the public samples but only 55% yield a proved, scoreable artifact. Accepted binaries can differ in gas by orders of magnitude, so proof completion and execution efficiency distinguish different aspects of generated programs.