HackerPapers

arXiv:2509.22908cs.SE

A benchmark for vericoding: formally verified program synthesis

Sergiu Bursuc, Theodore Ehrenborg, Shaowei Lin, Lacramioara Astefanoaei, Ionel Emilian Chiosa, Jure Kukovec, Alok Singh, Oliver Butterley, Adem Bizid, Quinn Dougherty, Miranda Zhao, Max Tan, Max Tegmark

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

Abstract

We present and test the largest benchmark for vericoding, LLM-generation of formally verified code from formal specifications - in contrast to vibe coding, which generates potentially buggy code from a natural language description. Our benchmark contains 12,504 formal specifications, with 3,029 in Dafny, 2,334 in Verus/Rust and 7,141 in Lean. Of these, 6,174 are new unseen problems. We find vericoding success rates of 27% in Lean, 44% in Verus/Rust and 82% in Dafny using off-the-shelf LLMs. Adding natural-language descriptions does not significantly improve performance. We also find that LLM progress has improved progress on pure Dafny verification from 68% to 96% over the past year. The benchmark and vericoding results are shared at https://github.com/Beneficial-AI-Foundation/vericoding-benchmark

arXiv comments
25 pages, 1 figure; data available at https://github.com/Beneficial-AI-Foundation/vericoding-benchmark
Journal reference
DOI
Subjects
cs.SESoftware Engineering cs.LGMachine Learning cs.PLProgramming Languages

On Hacker News

Linked by 1 identifiable commenter in 1 comment across 1 thread, from Mar 2026 to Mar 2026. Found in 3 HN submissions from Oct 2025 to Feb 2026. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments1 thread

  1. When AI writes the software, who verifies it? 1 comment

    • Looks like LLMs also find Dafny easier to write than Lean. This study, “A benchmark for vericoding: formally verified program synthesis”, reports: > We present and test the largest benchmark for vericoding, LLM-generation of formally verified code from formal specifications … We…

      cpetersoView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.