WybeCoder: Verified Imperative Code Generation

Abstract

Recent progress in large language models (LLMs) has advanced automatic code generation and formal theorem proving, yet software verification has not seen the same improvement. To address this gap, we propose WybeCoder, an agentic code verification framework that enables prove-as-you-generate development where code, invariants, and proofs co-evolve. It builds on a recent framework that combines automatic verification condition generation and SMT solvers with interactive proofs in Lean. To enable systematic evaluation, we translate two benchmarks for functional verification in Lean, Verina and Clever, to equivalent imperative code specifications. On complex algorithms such as Heapsort, we observe consistent performance improvements by scaling our approach, synthesizing dozens of valid invariants and dispatching dozens of subgoals, resulting in hundreds of lines of verified code, overcoming plateaus reported in previous works. Our best system solves 74% of Verina tasks and 62% of Clever tasks at moderate compute budgets, significantly surpassing previous evaluations and paving a path to automated construction of large-scale datasets of verified imperative code.

Results at a Glance

Overview

WybeCoder combines SMT-based automatic verification with interactive Lean theorem proving in a hybrid loop. The agent generates imperative code in Velvet—a Dafny-like language embedded in Lean 4 via the Loom framework—annotates it with loop invariants, and iteratively refines both code and proofs using compiler feedback.

Figure 1. WybeCoder subgoal decomposition multi-agent system. Starting from a problem specification, the agent generates an implementation and attempts to discharge verification conditions using CVC5. Remaining goals are tackled interactively in Lean, driving iterative implementation refinement or completing the proof.

Two agent strategies are supported:

• Sequential Agent — Single-agent turn-based loop with iterative refinement. Multiple independent attempts run in parallel (pass@k).
• Subgoal Decomposition — Extracts verification subgoals, dispatches parallel provers, and reconstructs the full proof. Supports conflict-driven method modification across iterations.

Code Example

The following implementation of the sum of fourth powers of odd numbers was generated and verified end-to-end by GPT-5 on verina_basic_43. It includes a non-trivial closed-form loop invariant, a separate algebraic identity lemma, and a multi-case proof block dispatched by loom_solve.

Contributions

1. Hybrid Software VerificationWe combine SMT solvers with interactive Lean proofs for LLM-based verification, and introduce the first benchmarks tailored to hybrid environments.
2. Inference Scaling WorkflowsWe study workflows for large-scale inference, identifying subgoal decomposition and goal-directed modification as key components.
3. Complex Algorithm VerificationOur system verifies challenging algorithms like Heapsort, managing dozens of subgoals and hundreds of lines of code.
4. Imperativeness JudgeAn LLM-based judge enforces genuine imperative implementations, addressing specification and functional leakage.

Inference Scaling

Performance shows consistent scaling without plateaus across several orders of magnitude of compute budget. We compare sequential agents and subgoal decomposition across frontier models.

(a) Claude 4.5 Opus. Sequential agents vs. subgoal decomposition on Verina.

(b) Gemini 3 Pro. Subgoal decomposition outperforms sequential agents for Gemini.

Model comparison. Inference scaling for multi-agent system with different models on Verina, using up to 128 subagents.

Sequential vs. parallel compute. Given a maximum budget of C language model calls, the optimal breakdown into k·T ≤ C with k ≤ 32 attempts and T ≤ 32 turns per attempt.

Multi-agent scalability. Allocating additional compute to a single subgoal decomposition copy continues to improve performance up to ~1200 model calls, after which pass@2 becomes preferable. For sequential agents the crossover occurs much earlier, at ~22 calls.

Detailed Results

Verina (189 problems)

Budget is represented as turns limit × number of agents launched for each problem. For Sequential Agent, k agents in parallel corresponds to pass@k. Solve rate combines both prove rate and disprove rate. For subgoal decomposition, there is no disproving.

Clever-Loom (161 problems)

Sorting Algorithm Verification

Sorting algorithms sit at the frontier of what is feasible with moderate compute budgets. The successful verification of Heapsort using 357 sub-agents demonstrates the scalability of our approach. Reynolds (1981) gives a by-hand proof in a section starred to connote difficulty, and later formal treatments would sometimes take up an entire paper.

BibTeX