3 papers
cs.SE2026
FVSpec: Real-World Property-Based Tests as Lean Challenges
Quinn Dougherty, Max von Hippel, Simon Henniger +2
We present a benchmark for evaluating AI models and agents on real-world formal software verification tasks. We first scrape 11,039 property-based tests (PBTs) from real-world Pyth…
cs.SE2025
A benchmark for vericoding: formally verified program synthesis
Sergiu Bursuc, Theodore Ehrenborg, Shaowei Lin +10
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 potentia…
cs.SE2025
Proving the Coding Interview: A Benchmark for Formally Verified Code Generation
Quinn Dougherty, Ronak Mehta
We introduce the Formally Verified Automated Programming Progress Standards, or FVAPPS, a benchmark of 4715 samples for writing programs and proving their correctness, the largest…