Verification for the 99%: Benchmarking Contract-Based Verifiable Code Generation in Pure Python

Benchmarks for verifiable code generation are built almost exclusively on verification-oriented languages (Dafny, Verus, Lean) that mainstream developers do not use. We present PyVeriBench, a benchmark for contract-based code generation in pure Python: 59 tasks with typed signatures, mutation-validated PEP 316 contracts, and 391 differentially-confirmed non-equivalent mutants. The benchmark is built around an audit of its own verifier. Candidates are checked by unit tests, property-based testing (Hypothesis), and bounded symbolic execution (CrossHair); because bounded executors mis-model real language semantics, every symbolic counterexample is concretely replayed before it counts. Replay quarantines the 1.7–2.7% of completions carrying spurious verifier reports, all traceable to one idiom-triggered modeling defect, so scoring rests on validated falsification evidence and never trusts raw verifier output. The headline metric, CEF@1 (counterexample-freedom under a time budget), is deliberately weaker than “verified”. Across three open Qwen2.5-Coder configurations (1.5B/3B in FP16, 7B in 4-bit AWQ) we evaluate code generation, specification generation, and counterexample-guided repair, and find that symbolic checking catches bug classes both test suites and property-based sampling miss; that good specifications (sound and mutation-killing) rise from 20% to 51% across configurations, where small models mostly fail to express legal formal conditions while what they try to express is usually reasonable; and that the dominant failure mode of self-repair is degenerate repetition, which an explicit anti-repetition instruction does not reduce (1.5B ablation). All experiments run on a single 12 GB consumer GPU; the benchmark, harness, and raw logs will be released.