Proof Compilation Is Not Correctness: End-to-end Evaluation of Agents That Generate Verifiable Code
TL;DR Formal verification can prove that code satisfies a specification. But who verifies that the specification captures what the user actually meant? We built a unified benchmark and evaluation harness to measure that gap.
Today, large language models are capable of generating source code that looks plausible, compiles, and often passes a useful set of unit, integration and smoke tests. However, code generation is a complex problem, which requires a certain level of determinism, which probabilistic generation using autoregressive language models is unable to guarantee. Existing methods try to circumvent this issue by generating code with a machine-checkable proof that it behaves correctly for every valid input. Doesn't this process of producing provably correct code solve the code reliability problem?
The answer is no.
Background: Verifiable Code Generation (VCG)
The state-of-the-art methodology for generating provably correct code is to choose a Formal Theorem Prover (FTP) like Lean, Dafny, Verus or Rocq, and design an LLM-based agent that uses the FTP as a tool. The agent then attempts generating the requested implementation and a machine-compilable proof of contract under Hoare logic.
Briefly, denote inputs x to, and outputs y of a function C implemented in a programming language as y = C(x). Then, given x satisfies some pre-conditions, i.e. it lies in a set P(x), the formal verifier attempts to generate a proof that x and y jointly satisfy some post-conditions, i.e. ∀x ∈ P(x), (x, C(x)) ∈ Q(x, y).
An FTP, by design, can establish that an implementation-proof pair satisfies a given formal specification, i.e. the tuple (P, Q). However, neither the FTP, nor the agent can establish that the formal specification faithfully captures a user's intent as inferred from their natural-language specification. If an agent formalizes the wrong requirement, the verifier may specify and prove a wrong thing perfectly.
This intent-specification gap motivates a key open question which is still largely unaddressed: how can we reliably evaluate agents that translate natural-language requirements into machine-verifiable code?
As a first step to addressing this question, we built a unified benchmark and evaluation harness for verifiable code generation (VCG). The suite brings together thousands of specification- and proof-generation examples, supports Lean 4 and Dafny, runs heterogeneous agents behind a common interface, and evaluates their output using signals that range from compilation to behavioral testing and semantic comparison.
Our initial experiments point to a simple conclusion: reliable code generation is a systems and evaluation problem, not just an agent-design problem. Structured agent workflows substantially improve formal validity and behavioral accuracy, but even a very high compilation rate can easily hide a large semantic gap.
The missing link between intent and proof
A natural-language-to-verifiable-code pipeline has at least four stages as shown in Figure 1 below:
- Interpret the user's requirement.
- Translate that requirement into a formal specification.
- Generate an implementation and proof or contract.
- Ask a verifier to check the formal artifact.
The final stage, i.e. the FTP, provides hard (deterministic) feedback about the validity of the proof. Lean, Dafny, and other formal systems reject artifacts that do not satisfy their rules. However, that guarantee is conditional in that the verifier checks the implementation against the specification it receives.
Example: Agent oversimplifies the intent
Consider the requirement "return the maximum element of an array." An agent might produce the valid post-condition result ∈ input. This weak property is easy to satisfy and may be easy to prove, but it says only that the result is an element of the input. A complete specification also needs to state that "every input element is less than or equal to the result." Both specifications are formal. However, only the latter captures the intended behavior.
This creates what we call the intent-specification gap. Closing the gap is nontrivial for the following three reasons:
- Machine verification is necessary but insufficient. A type-checked or formally verified artifact can still express the wrong behavior; thus, simply validating a generated proof is insufficient.
- Correct specifications are not unique. One could potentially check proofs against a dataset of human verified intent-proof pairs. But, the same abstract requirement may have many logically equivalent formulations, so exact string matching is a poor correctness test.
- Existing practical metrics are incomplete. (1) Finite tests cannot prove unrestricted equivalence; (2) reference-based methods require a trusted reference; and, (3) structural similarity can miss semantically equivalent formulations.
The evaluation of the intent-specification gap can be visualized using an evidence ladder as shown in Figure 2. Producing an artifact is the weakest signal, while parsing and type-checking add necessary evidence. Non-vacuity checks eliminate obvious loopholes. Behavioral tests probe intended examples and counterexamples to the specification. Semantic comparison to a trusted reference provides stronger evidence when it is available. At the top is agreement with the user's intended meaning, which is the property we ultimately care about and the hardest one to measure.
Building a unified VCG benchmark
Existing datasets contain valuable pieces of the problem, but they differ in language, stage, schema, metadata, and evaluation protocol. We assembled them behind a common benchmark interface so that agent workflows and metrics can be studied consistently.
The current suite contains:
| Task | Formal system | Examples | Primary signals |
|---|---|---|---|
| Specification generation | Dafny | 2,050 | Typechecking, verification, equivalence |
| Specification generation | Lean 4 | 6,073 | Typechecking, structural diagnostics, behavioral tests, semantic comparison |
| Proof generation | Lean 4 | 504 | Proof validity, safety, concision, structure |
The 8,123 specification-generation examples and 504 proof-generation examples were consolidated from existing benchmarks including VERINA, CLEVER, AlgoVeri, VeriCoding, and VeriSoftBench. We de-duplicated records while retaining source and license provenance.
The evaluation harness is designed to evaluate and experiment with real agents on various specification-generation (SpecGen) and proof-generation (ProofGen) metrics available in literature. A subprocess wrapper gives different agents a common, and intentionally minimal input-output contract. Successful generations are cached to avoid unnecessary model calls. Expensive metrics are batched, parallelized where appropriate, checkpointed, and resumable. Missing optional infrastructure is reported as an unavailable metric with a structured reason instead of aborting an entire run. Results are published to a static dashboard for row-level inspection and side-by-side comparison.
One answer requires multiple metrics
For SpecGen in Lean 4, we evaluate several complementary layers of metrics using our evaluation harness. Each metric type addresses a different aspect of the generated formal specification:
| Evaluation layer | Example metrics | What it tells us | What it cannot tell us |
|---|---|---|---|
| Formal validity | Lean 4 type-check | Whether the generated artifact elaborates | Whether it expresses the intended behavior |
| Behavioral correctness | Positive recall, negative rejection, balanced accuracy, VERINA pass@1 | Whether examples are accepted and counterexamples rejected | Whether the specification is correct for all inputs |
| Ground-truth comparison | BEq+, GTED | Whether a candidate is provably equivalent or structurally close to a reference | Whether the reference itself perfectly captures intent; proof search may be inconclusive |
| Fast diagnostics | Normalized exact match, signature F1, logical-atom F1, conservative non-vacuity checks | Whether representation and logical vocabulary resemble the reference and avoid obvious loopholes | Semantic correctness |
No individual metric can be treated as "the" accuracy of specification generation. Instead, each metric reveals a different potential failure mode. Typechecking catches malformed Lean 4 code, or invalid proof attempts. Behavioral tests expose candidates that compile but accept the wrong outputs. Reference-based methods identify stronger forms of agreement when their assumptions hold. They also depend on the quality of normalization done to bring the reference and the generated specification in the same form before comparison. Fast structural metrics make large-scale diagnosis practical, but should not be confused with proofs.
This layered approach mirrors a broader lesson in agentic systems: reliable autonomy comes from combining heterogeneous validation signals, then preserving enough trace data to understand when those signals disagree.
Comparing three approaches on VERINA
We evaluated three SpecGen workflows on the same 189 Lean tasks from VERINA. Each task includes a natural-language description, a formal specification, and positive and negative behavioral examples. The three agentic workflows are as follows:
- Prompted Claude tested direct, unassisted formalization from the description using one zero-shot attempt at implementation and proof.
- LeanAide added an agentic workflow with multiple candidates, formal-language filtering, and one compiler-guided repair attempt upon Lean 4 typecheck failure.
- CLEVER adapted used a typed signature and stronger, template-constrained input scaffolding.
Note that the comparison is not a pure model leaderboard, since the systems differ in prompts, context, candidate counts, and repair policy. However, the purpose of this experiment was to study complete workflows, not isolate a single model variable.
| Workflow | Generated | Type-checked | Behavioral pass (189 tasks) | Behavioral pass (evaluable tasks) |
|---|---|---|---|---|
| Prompted Claude | 189/189 | 128/189 (67.7%) | 47/189 (24.9%) | 47/165 (28.5%) |
| LeanAide | 177/189 | 177/189 (93.7%) | 67/189 (35.4%) | 67/155 (43.2%) |
| CLEVER adapted | 189/189 | 150/189 (79.4%) | 81/189 (42.9%) | 81/165 (49.1%) |
The following are findings from our experiment:
1. Structured workflows improve accuracy
Both structured approaches achieved higher behavioral pass rates than direct prompting. The strongest result came from CLEVER's constrained scaffolding: 81 of 189 tasks passed the behavioral criterion, compared with 47 for prompted Claude.
This is consistent with a common pattern in literature on VCG agents: explicit workflows, intermediate representations, and validation stages can outperform asking a capable model to solve the entire problem in a single shot. The model still matters, but the surrounding system determines what information it sees, what output shape it must produce, and what feedback it can use.
2. Scaffolding matters more as tasks become harder
On the "basic" subset of the VERINA dataset, prompted Claude achieved a 38.0% behavioral pass rate. On the advanced subset, it fell to 7.4%, a drop of 30.6 percentage points. The structured systems were more stable: LeanAide moved from 35.2% to 35.8%, while CLEVER adapted moved from 47.2% to 37.0%.
The more demanding the formalization task became, the less reliable one-shot prompting was. Typed context, templates, candidate generation, and verification-aware workflows provided useful inductive bias when the description alone was not enough.
3. Compilation leaves a large semantic gap
LeanAide produced 177 artifacts that type-checked, but only 67 passed the available behavioral checks. In other words, 110 type-checked candidates still failed the behavioral criterion.
One example involved a specification for integer average. The intended constraint correctly encoded rounding behavior. LeanAide generated a different inequality that type-checked, but rejected a valid case where a = 3, b = 4, and result = 3.
The compiler did its job: it confirmed that the statement was valid Lean 4. The failure was semantic, not syntactic.
Repair needs semantic feedback
Compiler-guided repair improved LeanAide's compilation rate. Of 29 candidates sent through one repair attempt, 17 recovered and compiled.
But compiler feedback describes formal-language errors. It can point to a missing token, an invalid type, or a declaration that does not elaborate. It generally cannot say, "This condition no longer captures the user's meaning." Without semantic feedback, a repair loop can make an artifact well-formed while leaving its behavior wrong.
This suggests a potentially more capable architecture for verifiable code generation:
- Generate multiple candidate specifications.
- Reject malformed and obviously vacuous candidates.
- Execute positive and negative behavioral checks when examples are available.
- Compare surviving candidates against trusted references or semantic invariants.
- Feed counterexamples and structured semantic failures back into generation.
- Only then generate and verify the implementation and proof.
The verifier remains essential, but it becomes one component in a broader plan-evaluate-repair loop.
What this benchmark does, and does not, establish
The suite is not yet a universal agent leaderboard. Some metrics apply only to source datasets with the right metadata; for instance the VERINA behavioral tests require positive and negative samples for each formal specification. BEq+ and GTED depend on trusted references and can be inconclusive. Agents currently differ in how many candidates and retries they receive, so workflow results should not be interpreted as controlled model ablations.
Next steps: The next steps are to develop and calibrate better measures of semantic equivalence, test metrics against controlled pairs of faithful and subtly weakened specifications, and run full-scale ablations that isolate the contributions of prompting, context, candidate diversity, verifier feedback, behavioral feedback, and repair. In the longer term, the same evaluation signals can guide generation, i.e. developing more powerful VCG agents. A benchmark that diagnoses semantic failure can become the foundation of an agent that corrects it.
From code generation to intent-aligned systems
Verifiable code generation combines two very different strengths. Neural models are flexible: they can translate natural language, retrieve patterns, and propose implementations. Symbolic systems are precise: they apply explicit rules and provide deterministic, inspectable judgments.
Neither is enough alone. A probabilistic model cannot turn likely tokens into a correctness guarantee by assertion. A symbolic verifier cannot recover the user's intent from an incomplete formal statement.
The opportunity is neuro-symbolic and agentic: use models to propose and revise formal artifacts; use compilers, tests, proof assistants, reference checks, and counterexamples to constrain that search; and instrument the entire workflow so that failures become evidence for the next iteration.
The central lesson from this work is straightforward: It is not sufficient to only check whether generated code is verified. Rather, we should ask what, exactly, has been verified, and how we know it is the right thing. The second part of the question is a fairly open problem, and at a philosophical level, is reminiscent of a well-known dilemma in statistical learning:
The behavior of a data-driven system cannot generally be established from first principles; its generalization properties must instead be inferred statistically from observations independent of those used to construct it. Consequently, reliable evaluation of increasingly data-driven systems itself requires sufficiently rich and representative evaluation data.
Since SpecGen is largely a data-driven problem, it will inevitably need evaluation data to assess its quality.