Recoleta
GitHub
Source note

WybeCoder: Verified Imperative Code Generation

Authors
Fabian Gloeckle, Mantas Baksys, Darius Feher, Kunhao Zheng, Amaury Hayat, Sean B. Holden, et al.
Source
arXiv
Published
Collection
Software Intelligence
Formal VerificationImperative Code GenerationLean Theorem ProvingMulti Agent SystemsCode Intelligence
Open arXivMarkdown source

Summary

WybeCoder is a hybrid agent system for generating and formally verifying imperative programs. It combines SMT-based verification with interactive Lean proof work, and it reports much higher solve rates than earlier verified-code benchmarks for this setting.

Problem

  • LLMs improved code generation and theorem proving, but formal verification of generated software still lags, especially for imperative code with mutable state and loops.
  • Existing work usually handles either functional programs in theorem provers or imperative programs in auto-active systems like Dafny; each misses part of the problem.
  • This matters because generated code still needs costly human review, and testing or fuzzing cannot give full correctness guarantees.

Approach

  • The system follows a prove-as-you-generate loop: generate imperative code, generate invariants, run verification condition generation, send routine obligations to CVC5, and send hard leftovers to Lean.
  • It uses two agent styles: a sequential refinement agent and a subgoal-decomposition multi-agent system that extracts proof obligations, solves them in parallel, and reconstructs the full proof.
  • When a proof subgoal fails, agents can request targeted code or invariant changes. Named invariants and deterministic goal names let the system transfer solved subproofs across revisions.
  • The authors translated the Verina and Clever functional-verification benchmarks into imperative Velvet/Lean tasks to evaluate this setup.
  • To reduce specification leakage and functional cheating, they allow functional specs but require imperative implementations, then filter with an LLM-based imperativeness judge.

Results

  • Best reported Verina result: 74.1% solve rate with Claude 4.5 Opus using the sequential agent at 32 turns × 16 agents.
  • Best reported Clever-Loom result: 62.1% solve rate with Claude 4.5 Opus using the sequential agent at 32 turns × 16 agents.
  • On Verina, sequential-agent scores are 64.6% (GPT-5), 55.6% (Gemini 3 Pro), 63.3% (Claude 4.5 Sonnet), and 74.1% (Claude 4.5 Opus). The listed baseline is 20.0% for DS Prover V2 7B.
  • On Clever-Loom, sequential-agent scores are 53.8% (GPT-5), 32.8% (Gemini 3 Pro), 59.6% (Claude 4.5 Sonnet), and 62.1% (Claude 4.5 Opus), versus 8.7% for the COPRA baseline.
  • The paper highlights a low-budget gain on Verina from 18% in prior reported results to 55% with their setup, and it cites 15% to 55% improvement for hybrid verification in small-budget settings.
  • Their leakage control had a large effect: one GPT-5 subgoal-decomposition setting on Verina dropped from 75.1% without the imperativeness guard to 51.9% with it, which the authors treat as a more honest measure of imperative verified code generation.

Link