VCG: A High-performance Verified Coding Agent for Python
TL;DR
We present state-of-the-art results for end-to-end natural-language-to-runnable Python generation with component-level formal verification. Our verified code generation for Python ships a runnable package plus a machine-checked Dafny certificate for each verified component.
Among systems that generate runnable Python from natural-language specifications while producing formal verification artifacts, to the best of our knowledge, VCG achieves the highest reported HumanEval pass@1 to date (94.4%) versus 77% reported by the closest prior end-to-end system. Note, however, that due to practical challenges this comparison is across different underlying models and is therefore not a controlled architectural comparison as discussed later in the blog.
Introduction
Modern LLMs write code that passes tests most of the time. But "passes tests" and "provably satisfies the specification" are not the same thing — and for code that ships into production, the distinction matters. A payment processor that passes its unit tests can still overflow on an integer edge case the tests didn't visit. A medical dose calculator that answers correctly on the benchmark's inputs can still round the wrong way on some input in practice.
Formal verification — e.g., machine-checking that an implementation satisfies its specification via an SMT solver like Z3 — has been the answer to this problem for decades. Historically, it required experts to author the specification, the implementation, and the proof annotations by hand, keeping formal methods only for critical applications and out of routine software development. However, with more and more auto-generated code with coding agents, the need for formal verification is more pertinent than ever.
We introduce VCG (Verification-Driven Code Generation): an end-to-end pipeline of specialized LLM agents that takes a natural-language coding request and produces runnable Python — with a formal verification certificate for the parts of the code that can be verified, and a well-signaled fallback for the parts that can't.
VCG is the first evaluated system that produces multi-component runnable Python packages with per-component Dafny certificates, integrity checks that reject vacuous verifications, explicit downgrade labels for the unverified subset, and rigorous evaluation across three public benchmarks.
Evaluation setup
Both VCG (with Dafny backend) and a BareLLM baseline — the same Claude Opus 4.7 model invoked in a single prompt-in, code-out call with no loops — generate 10 samples per problem at temperature 0.2, then flow through each benchmark's own official scorer. VCG produces a runnable Python package (transpiled from verified Dafny where possible via dafny build --target:py, LLM-emitted python-emit fallback where not); BareLLM produces a plain Python function. Both are graded the same way, on the benchmark's terms.
Pass@k is the standard Chen et al. unbiased estimator over the 10 samples per problem: pass@1 is the mean per-problem probability that a single sample passes; pass@10 is the probability that at least one of 10 samples passes. Higher is better for both. What "passes" means depends on the benchmark:
HumanEval / HumanEval+ use EvalPlus's check_correctness — base_pass runs the original 2021 HumanEval tests; plus_pass runs the ~80× larger adversarial test suite EvalPlus adds.
LeetCodeDataset test uses its own hidden-test suite via check(candidate).
LiveCodeBench v6 uses run_test against per-problem competition-style hidden tests.
The "Verified components ship on X%" column in the results table means the fraction of problems where the primary function's component passed the full Dafny verification path — Dafny's SMT-backed proof succeeded and the static ensures-binding integrity check confirmed the proof was against a Spec-defined predicate (not a trivially-satisfiable one). Everything else ships as an LLM-emitted python-emit fallback, labeled unverified with a runtime warning.
Summary of benchmark results
VCG is evaluated on three public coding benchmarks — HumanEval / HumanEval+ (same 164 problems, scored on two test suites — see note below), LeetCodeDataset test (228 problems), and LiveCodeBench v6 (1,055 problems) — totaling 1,447 problems and ~14,470 sample-level evaluations at 10 samples per problem.
| Benchmark | Test suite | VCG pass@1 | VCG pass@10 | Verified components ship on |
|---|---|---|---|---|
| HumanEval (164 problems) | base tests (original 2021 suite) | 94.4% | 99.4% | 95% of problems |
| HumanEval+ (same 164) | plus tests (~80× more adversarial, from EvalPlus) | 81.3% | 92.7% | 95% of problems |
| LeetCodeDataset test (228) | benchmark hidden tests | 60.8% | 85.9% | 70% of problems |
| LiveCodeBench v6 (1,055) | benchmark hidden tests | 66.9% | 88.6% | 85% of problems |
"Verified components ship on X%" means the fraction of problems where the primary function's component passed the Dafny path (and the ensures-binding integrity check described later); the remainder ship as python-emit fallbacks with explicit downgrade labels. Across all 6,169 verified components shipped, 100% pass the ensures-binding check.
HumanEval and HumanEval+ are not two benchmarks — they are the same 164-problem benchmark scored against two different test suites. The EvalPlus project extends the original HumanEval with roughly 80× more adversarial test inputs per problem, and its scorer records both a base_pass result (original tests) and a plus_pass result (adversarial extension) per sample; we aggregate the two independently from the same set of per-sample runs. Of the 1,640 possible HumanEval+ samples (164 × 10), the evaluation completed 1,632 — the remaining 8, spread across 3 problems that finished with 4 or 9 samples instead of 10 before the harness was interrupted, are excluded from the denominator rather than counted as failures. Pass@k is computed via the Chen et al. unbiased estimator over the samples we actually have. Raw per-sample artifacts for every reported run are available on request.
A note on the failure composition: the raw pass@1 numbers above count every non-passing sample as a failure, regardless of whether the failure was a wrong-answer bug, a timeout, or the benchmark harness itself crashing. On LiveCodeBench v6 (our largest benchmark, and the one where the harness surface is broadest), of the ~33% of samples that don't pass: roughly 3% are assertion failures (wrong output), 12% are runtime errors in the emitted code, 10% are timeouts, and ~8% are evaluation harness-side crashes (the LCB v6 scorer itself crashing or the pipeline failing to produce output before evaluation began). In a scenario where we exclude the harness-side bucket — samples where the code was never actually evaluated against a test — the LCB v6 pass rate would be around 72.6% rather than 66.9%. We report the raw number as the primary figure because it is the direct measurement; we note the adjusted number to be transparent about what the failure surface actually contains.
How VCG relates to prior work
Prior work in this space falls into three loose categories, ordered by how many systems occupy each:
| Scope | Includes | Named work in the space |
|---|---|---|
| LLM + prover work | LLM interacts with a formal verifier | Copra, Baldur, Clover, AutoSpec, CoqPilot, Proof-Carrying Code Completions |
| Automated verified code generation | Systems that produce machine-checked code from a spec | DafnyBench, various Dafny/Lean synthesis tools |
| End-to-end NL → runnable Python + verification certificates | Natural-language input, executable Python output, verification for the verifiable subset | Li et al. (Dafny 2025 @ POPL); VCG |
Only one prior system meaningfully occupies the third scope: Li, Zetzsche & Somayyajula, "Dafny as Verification-Aware Intermediate Language for Code Generation" (Dafny 2025 workshop, colocated with POPL 2025) — a prototype that generates Dafny from natural language and transpiles it to Python. On the one benchmark they evaluated (original HumanEval, 164 problems, Claude Sonnet 3.5), they reported a measured 77% pass rate.
VCG, evaluated on the same benchmark, reaches 94.4% pass@1 — a 17-point gap. Two important caveats on that gap: VCG runs on Claude Opus 4.7 whereas Li et al. evaluated Claude Sonnet 3.5, and neither system has been re-run under matched conditions. The observed 17-point difference therefore reflects a combination of model capability, prompting, inference configuration, and the architectural differences described below; we do not attribute it to any single factor. On the harder HumanEval+ (~80× more adversarial tests per problem), VCG reaches 81.3% pass@1 and 92.7% pass@10, and continues to scale across LeetCode-style problems that Li et al.'s prototype was not evaluated on.
Beyond the pass-rate lift, VCG differs from prior work in three architectural dimensions worth calling out:
Verification-integrity guarantees against vacuous proofs. Verifier acceptance is not the same as meaningful verification. A pre-launch audit of our own pipeline discovered that ~27% of components Dafny had blessed as proof_ok carried ensures clauses that didn't reference any predicate defined in the paired specification — the impl was being proven against a trivially-satisfiable obligation, a subtler failure mode than the {:axiom} / {:verify false} bypass tricks we had already caught in earlier hardening rounds. VCG now runs a static integrity check that rejects any Dafny proof whose ensures clauses don't bind to a spec-defined predicate, gated inside the verify-repair loop. Across all 6,169 verified components shipped, 100% pass this check. This is a syntactic guard, not a semantic one — it doesn't establish that the spec faithfully captures the requirement — but it closes one concrete, empirically-observed class of "verified but vacuous" that we suspect any NL-driven verified-code system will encounter.
Graceful degradation, not verification-or-nothing. When Dafny can't prove a component, VCG falls back to LLM-generated Python and marks it as unverified — but the code still ships. Callers know via runtime warnings that they're calling into an unverified component.
Multi-component packages, not single functions. VCG's PlannerAgent decomposes a natural-language request into a directed acyclic graph of components. Each component is verified independently. The final output is a runnable Python package — pip-installable, with an entry point, tests, and a PROVENANCE.md documenting which components are verified and which are not. For verified components, the shipped Python is transpiled from the proven Dafny via dafny build --target:py, so the certificate applies to the shipped code modulo Dafny's compiler and runtime. Unverified components are LLM-emitted Python and are labeled as such — no certificate is claimed for them.
The journey: Lessons learned through nine hardening rounds and a customer-pilot phase
We started building VCG in early 2026 with an obvious hypothesis: if you decompose a coding problem, formalize the spec, verify each component, and fall back gracefully when verification fails, you should reach or beat unverified LLM baselines on functional correctness while also providing formal guarantees.
That hypothesis did not hold. VCG loses 14–16 pp pass@1 against a strong LLM baseline. We spent nine hardening rounds figuring out why, characterizing the mechanism, and building a pipeline that ships verified code at the cost of that pass@1 tax.
The rounds, at a very high level:
Rounds 1–3 (h-01 → h-03) — first working pipeline. Established the fixed sequence of specialized agents (Planner, Requirements, Labeler, Spec, TestSynth, Impl, Prover) and the two-tier fallback (verified via Dafny, else python-emit). Discovered and closed a family of verifier-bypass tricks the LLM would learn to emit ({:axiom}, {:verify false}, {:extern}).
Round 4 (h-04) — measurement rigor. Pass@1 wasn't the right metric alone; we introduced a two-axis evaluation framework combining pass@k for functional correctness with a verification-certificate rate for machine-checked correctness. This is when we first realized the "ceiling" wasn't verification difficulty — it was spec fidelity.
Rounds 5–8 (h-05 → h-08) — hardening the spec pipeline. Added example-gates (executable test cases the compiled Python must pass before we accept a verified component), spec-review critics, and behavioral-vote spec self-consistency. Some of these landed (example-gate: kept), others were tested and disabled after ablations showed they hurt pass@1 (spec self-consistency: rejected).
Round 9 (h-09) — the ensures-binding integrity check landed (mechanism and the ~27% audit finding are described in How VCG relates to prior work above). This addressed a subtler form of vacuous verification than the h-03 bypass-attribute class; the config was frozen for benchmark evaluation after this round.
After the harden-09 config was frozen for benchmark evaluation, we ran a customer-pilot evaluation on a large real-world specification — a 59-component yield-excursion root-cause analysis system for post-silicon semiconductor test data. This surfaced a new class of failure modes that don't show up on function-scale benchmarks: chart-render components with high sampling variance, oversized components the LLM would emit despite prompt-level guidance to keep them small, and post-materialize test-repair loops that misattributed failures.
That kicked off a post-h-09 reliability arc — a set of pipeline additions that don't affect the benchmark numbers above but let VCG produce structurally-sound packages on customer-scale specs:
Post-planner size-cap validation — programmatic re-prompt if the planner emits any component with more than 8 declared functions. Prevents mega-components that reliably stub in python-emit.
Multi-candidate python-emit (MC-emit) — for python_pure components, draw N=3 candidates in parallel at diverging temperatures, pick the one that parses and defines all declared functions. Same architectural pattern as N7 for Dafny specs, applied to Python code generation.
Auto-emitted structural + fixture-liveness smoke tests — every generated repo ships with tests that verify the code imports cleanly, that the entry point runs, and that every declared function is defined and doesn't crash on degenerate input.
Test-repair loop with per-component attribution — when smoke tests fail, the pipeline extracts the failing component from the pytest traceback and re-invokes python-emit for that specific component with the failure as context.
On the yield-excursion pilot, these additions took the pipeline from 2–4 stubbed components per run to 0 stubs and 334/334 smoke tests passing on a 59-component multi-package output — structural liveness, not domain correctness.
Discussion
VCG does not beat unverified LLM baselines on pass@1 for benchmark evaluation. On LCB test, HumanEval+, and LCB v6, VCG loses 14–16 pp pass@1 to a Claude Opus 4.7 baseline in a single-prompt setting. The gap is real, consistent across benchmarks, and mechanistically caused by what we call the spec-fidelity gap: verification proves that the implementation satisfies the specification, but assertion-based benchmarks measure whether the implementation satisfies the underlying requirements. When the LLM-authored spec drifts from the requirements, a proof of impl ⊨ spec is not enough.
We should also flag likely benchmark contamination as a second contributor to the pass@1 gap. HumanEval, LeetCodeDataset, and even LiveCodeBench v6 are all likely within Claude Opus 4.7's training data — a strong LLM's high pass@1 on these benchmarks reflects memorization as much as derivation from a specification. A per-problem date-bucket analysis on LiveCodeBench v6 (which continuously harvests fresh problems and tags them by release date) shows VCG's pass@1 gap narrows by 9.4 pp on Hard-tier problems dated after mid-2024, consistent with the hypothesis that verification-driven derivation transfers better than pattern-matching to less-familiar problems — but the effect is not clean because even LCB v6's freshest problems may be within training-data reach. So the pass@1 gap likely has two contributors: (1) the spec-fidelity gap described above, and (2) memorization advantage the baseline enjoys on benchmarks it has partially seen. We do not claim to have disentangled the two rigorously.
VCG is not the right tool for every code-generation setting. For pure pass@k benchmarking, just using a strong LLM for code generation is better. VCG makes sense when your consumers value auditable specifications, machine-checked correctness certificates for the verifiable subset, or wider sample-space diversity across candidate solutions.
The tradeoff is a small pass@1 tax in exchange for verification certificates, downgrade signals, and multi-benchmark generalization. It is not a strict improvement, and we have tried to characterize both sides.
What's next
Three directions we're actively working on:
Real-world deployment. Continuing to iterate on the reliability arc against customer-scale specifications; each new domain surfaces its own failure modes that don't show up on function-scale benchmarks. Real-input trials on the yield-excursion output are underway.
Closing the spec-fidelity gap. The dominant failure mode we characterize is spec drift — the LLM-authored specification reading the requirements incorrectly. Approaches under investigation include Surface-grounded spec strengthening (lifting concrete example invocations into formal lemmas the spec must satisfy) and counter-example-driven spec repair.
Adversarial-input robustness. Standard benchmark tests use inputs authors wrote. Real code hits inputs no one wrote. A controlled fuzzing study measuring whether verification-driven code degrades more gracefully on out-of-distribution inputs (vs a baseline's silent failures) is in the works.
A technical paper covering the full experimental methodology, ablation results, and prior-art comparison is forthcoming.