AI agents write code fast. They do not prove it correct. Vero, a new benchmark from ArXiv (2608.13522v1), asks whether agents can produce both implementation and machine-checked proof in multi-module repositories. The answer is no, not yet. The strongest agent configurations solve only 27 of 43 instances and close zero specifications on the hardest repos.
This is not a failure of model scale. It is a plumbing problem. Verified code generation requires coordinating code synthesis, proof construction, and specification alignment across modules. When the proof assistant rejects a candidate, the agent must backtrack with constraints, not just retry blindly. The proof is the product, and the orchestration flow determines whether you ship both or neither.
What Vero Measures
Vero evaluates joint implementation and proof synthesis at repository scale. Each of the 43 instances is a multi-module codebase in Lean 4 with:
- Predetermined API interfaces
- Manually curated formal specifications
- Reference implementations for validation
- Support for proof-only and code-and-proof modes
The benchmark spans Python, Dafny, Verus, and Coq source material, covering cryptographic protocols, distributed systems, and data structures. Agents must generate both code and proofs that satisfy the specification, or formally prove the specification is unsatisfiable.
This is not function-level verification. It is repository-level coherence. A correct proof for module A may assume properties of module B that the agent has not yet proven. The agent must track dependencies, manage proof state across modules, and detect circular reasoning.
The Code-Proof Coordination Loop
Verified code generation introduces a feedback loop between three components:
- Code generator: Produces candidate implementations from natural language or partial specifications
- Proof assistant: Type-checks code and verifies proofs (Lean 4 in Vero’s case)
- Proof synthesizer: Generates tactics and lemmas to close proof obligations
The orchestration question is whether these run sequentially, interleaved, or in a proof-guided mode where the proof assistant constrains the code search space.
Sequential Flow
The agent generates code first, then attempts to prove it correct. This is the simplest pipeline but wastes compute when the implementation is unprovable. The agent may generate idiomatic code that violates the specification in subtle ways (off-by-one errors, missing edge cases, incorrect invariants).
Interleaved Flow
The agent alternates between code generation and proof construction, using proof failures to refine the implementation. This requires the agent to parse proof assistant error messages and map them back to code changes. Lean’s error messages are precise but not always actionable for an LLM without additional context.
Proof-Guided Flow
The proof assistant runs first, generating proof obligations that constrain the implementation space. The agent then generates code that satisfies these obligations by construction. This inverts the traditional flow and requires the specification to be detailed enough to guide synthesis.
Vero does not mandate a specific flow. Agents are free to choose their coordination strategy. The benchmark measures only whether the final artifact (code plus proof) type-checks and satisfies the specification.
Failure Modes and Backtracking
When the proof assistant rejects a candidate, the agent faces three options:
- Retry with constraints: Add the failed proof obligation as a negative example and regenerate
- Backtrack to specification: Revise the implementation to align with a simpler proof strategy
- Abandon and flag: Formally prove the specification is unsatisfiable or the reference code is incorrect
Vero includes an audit mechanism for option three. Agents can submit a proof of unsatisfiability or a counterexample to the reference implementation. This surfaces latent errors in the benchmark itself and prevents agents from being penalized for correct refusals.
The strongest agents in the evaluation still fail to leverage this mechanism effectively. They retry the same proof strategy multiple times rather than exploring alternative implementations or challenging the specification.
State Management Across Modules
Multi-module verification requires tracking proof state across files. A lemma proven in module A may be reused in module B, but only if the agent maintains a dependency graph and avoids circular reasoning.
Vero repositories include predetermined API interfaces, which act as module boundaries. The agent must:
- Prove each module satisfies its interface contract
- Use only the interface (not the implementation) when reasoning about dependencies
- Detect when a proof assumes properties not yet proven in upstream modules
This is a state management problem. The agent needs a data structure that tracks:
- Proven lemmas and their assumptions
- Unproven proof obligations and their dependencies
- Module boundaries and interface contracts
Without this, the agent will generate proofs that assume their own conclusions or fail to reuse proven lemmas, leading to redundant proof work.
Observability for Proof Failures
Debugging proof failures requires more than a binary success signal. Useful observability includes:
- Proof trees: The structure of the proof attempt, showing which tactics succeeded and where the proof got stuck
- Tactic traces: The sequence of proof steps, with intermediate goals and hypotheses
- Type-checking errors: Specific mismatches between expected and actual types
- Timeout locations: Which proof obligations exceeded the time budget
Vero does not prescribe an observability format, but agents that log only success/fail will struggle to improve. The proof assistant (Lean 4) provides rich error messages, but agents must parse and act on them.
A practical observability stack for verified code generation might include:
-- Example proof trace structure
structure ProofTrace where
goal : Expr
tactics : List (Tactic × Result)
finalState : Option ProofState
timeElapsed : Nat
errorMessage : Option String
-- Agent logs this for each proof attempt
def logProofAttempt (trace : ProofTrace) : IO Unit := do
IO.println s!"Goal: {trace.goal}"
for (tactic, result) in trace.tactics do
IO.println s!" {tactic} -> {result}"
match trace.finalState with
| some state => IO.println s!"Final state: {state}"
| none => IO.println s!"Failed: {trace.errorMessage.getD "unknown"}"This gives the agent a structured view of what worked, what failed, and where to focus next attempts.
Caching and Proof Reuse
Verified code generation is expensive. A single proof may require dozens of tactic applications and multiple LLM calls. Caching proven lemmas across agent runs avoids re-proving identical subgoals.
The caching strategy depends on proof granularity:
| Granularity | Cache Key | Invalidation Trigger | Trade-off |
|---|---|---|---|
| Lemma | Lemma statement hash | Specification change | High hit rate, coarse invalidation |
| Tactic sequence | Goal + tactic list | Any upstream proof change | Low hit rate, fine-grained reuse |
| Proof term | Full proof object | Never (immutable) | Perfect reuse, large storage |
| Module | Module interface hash | Interface change | Coarse reuse, simple invalidation |
Vero does not include caching infrastructure, but production systems will need it. A proof cache might look like:
class ProofCache:
def __init__(self, storage_backend):
self.backend = storage_backend
self.hit_count = 0
self.miss_count = 0
def get_proof(self, lemma_hash, dependencies):
# Check if lemma proof exists and dependencies are satisfied
cached = self.backend.get(lemma_hash)
if cached and self._deps_valid(cached, dependencies):
self.hit_count += 1
return cached.proof
self.miss_count += 1
return None
def store_proof(self, lemma_hash, proof, dependencies):
self.backend.put(lemma_hash, {
'proof': proof,
'deps': dependencies,
'timestamp': time.time()
})The invalidation logic is critical. A cached proof is only valid if all its dependencies (upstream lemmas, module interfaces) remain unchanged. Dependency tracking is the same state management problem described earlier.
Architecture: Proof-First vs Code-First
Two architectural patterns emerge for verified code generation:
Code-First: Generate implementation, then attempt proof. Fails fast on unprovable code but wastes compute on proof attempts.
Proof-First: Generate proof obligations from specification, then synthesize code to satisfy them. Requires detailed specifications but guarantees provability by construction.
Vero supports both. The benchmark includes a proof-only mode where reference implementations are provided, and a code-and-proof mode where the agent generates both.
The proof-first architecture looks like:
- Parse formal specification into proof obligations
- Generate proof skeleton with holes for implementation details
- Synthesize code to fill holes, guided by proof context
- Type-check and verify the complete artifact
The code-first architecture looks like:
- Generate implementation from natural language description
- Attempt to prove it satisfies the specification
- On failure, extract counterexample or error message
- Refine implementation and retry
Neither dominates. Code-first is faster when the implementation is obvious. Proof-first is safer when the specification is complex and the implementation space is large.
Security Boundaries
Verified code generation introduces new attack surfaces:
- Malicious specifications: An attacker provides a specification that is satisfiable but encodes unintended behavior
- Proof assistant exploits: Bugs in the proof checker allow invalid proofs to pass
- Dependency confusion: The agent imports a malicious module that satisfies the interface but violates assumptions
Vero does not address these directly, but production systems must. The specification is the security boundary. If the specification is wrong, the proof is meaningless.
A practical security model treats the specification as untrusted input and requires:
- Human review of specifications before proof attempts
- Sandboxed execution of the proof assistant
- Dependency pinning and integrity checks for imported modules
- Audit logs of all proof attempts and failures
The proof assistant itself must be trusted. Lean 4 has a small trusted kernel, but bugs in the elaborator or tactic framework could allow invalid proofs. Formal verification of the proof assistant is an active research area but not yet practical for production.
Deployment Shape
A verified code generation system has three deployment options:
- Batch: Agent generates code and proofs offline, human reviews before merge
- Interactive: Agent assists human during development, suggesting proofs in real time
- Autonomous: Agent generates and merges verified code without human review
Vero evaluates autonomous mode. The agent has full access to the Lean toolchain and must produce a complete, verified repository.
Batch mode is safer but slower. The agent runs overnight, and a human reviews the generated code and proofs the next day. This works for low-frequency tasks like protocol implementations or security-critical libraries.
Interactive mode is faster but requires tight integration with the developer’s editor. The agent must respond to partial code in milliseconds and provide actionable proof suggestions. This is a different engineering problem than batch generation.
Autonomous mode is the goal but not yet reliable. The Vero results show that even frontier agents fail on hard repositories. Deploying autonomous verified code generation to production requires fallback strategies when the agent cannot close a proof.
Technical Verdict
Use verified code generation when:
- Correctness is more valuable than speed (cryptographic protocols, safety-critical systems, financial logic)
- The specification is precise and stable
- You have expertise to review proofs and debug proof failures
- The codebase is modular with clear interface boundaries
Avoid it when:
- The specification is vague or changes frequently
- Proof failures are not actionable (no observability, no debugging tools)
- The team lacks formal methods experience
- Iteration speed matters more than correctness guarantees
Vero shows that repository-scale verified code generation is not yet solved. Agents can handle individual functions but struggle with multi-module coherence, proof reuse, and backtracking strategies. The plumbing (state management, observability, caching) is as important as the model. If you are building verified code generation, invest in the orchestration layer first. The proof is the product, and the infrastructure determines whether you ship it.