VerifyThisBench: Joint Evaluation of Code, Specifications, and Proof

Large language models (LLMs) have demonstrated remarkable progress in code generation, but many existing benchmarks are approaching saturation and offer little guarantee on the trustworthiness of the generated programs. To improve visibility into model reasoning on formal correctness, we introduce \verify, a new benchmark that evaluates end‑to‑end program verification from natural language descriptions: models must (i) extract formal specifications, (ii) implement in a verification‑aware language, and (iii) construct machine‑checkable proofs. Our evaluation reveals a gap between formal verification and true correctness. While models can sometimes produce programs that pass verification, only a small fraction are actually aligned with the intended task: across 1,078 tasks, six SOTA models collectively produce just 36 human-verified correct solutions, with the best model achieving only 20. This discrepancy arises because verification only guarantees correctness with respect to the generated specification, not the original intent. To address this, we introduce a filtering methodology combining automatically generated test cases with an independent LLM-based semantic judge, requiring human inspection only when the two signals disagree. Further, we propose VerifyThisBench, a relaxed variant where partial specifications, implementations, or proofs are provided disentangle sources of difficulty. Together, We release VerifyThisBench with test suite, VerifyThisBenchXS, and a unified evaluation environment spanning seven verification tools to support future research on trustworthy program synthesis.