wybecoder-verified-imperative-code-generation

Extract — WybeCoder: Verified Imperative Code Generation

• URL: https://github.com/facebookresearch/wybecoder (+ project page https://facebookresearch.github.io/wybecoder; paper PDF on site)
• Fetched: 2026-09-27 ~19:34 CST · GitHub MCP README + defuddle parse project page —md (PDF not HTML)
• Authors: Fabian Gloeckle*, Mantas Bakšys* (equal), Darius Feher, Kunhao Zheng, Amaury Hayat, Sean B. Holden, Gabriel Synnaeve, Peter O’Hearn (FAIR Meta / CERMICS / Cambridge / UCL / …)
• Code: https://github.com/facebookresearch/wybecoder · License CC-BY-NC 4.0
• Stack: Velvet (Dafny-like imperative DSL) embedded in Lean 4 via Loom; VCG → cvc5 SMT; leftover goals interactive Lean; optional MCP via Loogle + Leanexplore

Core claims

• Prove-as-you-generate: code, loop invariants, and proofs co-evolve in one agent loop — not “write then verify later.”
• Hybrid verification: SMT (cvc5) discharges easy VCs; Lean interactive proofs handle the rest; compiler/REPL feedback drives refinement.
• Two strategies: (1) Sequential Agent — single-agent turn loop, parallel independent attempts = pass@k; (2) Subgoal Decomposition — extract VCs, parallel sub-provers, reconstruct full proof; conflict-driven method modification across iterations.
• Translates Verina (189) and CLEVER (161 → Clever-Loom) into imperative Loom specs for hybrid evaluation; first benches tailored to SMT+Lean hybrid environments.
• Imperativeness Judge (LLM): rejects functional/spec leakage so solutions must be genuinely imperative (addresses CLEVER-style leakage concerns at the Loom layer).
• Inference scaling: no plateau across orders of magnitude of compute; Heapsort verified with 357 sub-agents (dozens of invariants/subgoals, hundreds of LOC).

Numbers

• Verina: best 74.1% solve (140/189 = 128 proved + 12 disproved) — Claude Opus 4.5, sequential 32 turns × 16 agents. Subgoal decomp Opus 8×128 → 66.7%. Baselines much lower (DS Prover V2 7B 20%; Gemini 3 Pro seq 55.6%; GPT-5 seq 64.6%).
• Clever-Loom: best 62.1% (100/161) — Opus 4.5 seq 32×16. COPRA (Claude 3.7, 600s) baseline only 8.7%. Decomp Opus 8×128 → 57.8%.
• Sorting frontier: Selection/Bubble/Insertion/Binary-Insertion ✓; Heapsort (Heapify/Maxheap/Sort) ✓; Quicksort Partition+Sort ✓ but Step ✗; Mergesort Mergeruns+Sort ✓ but Mergepass ✗; Recursive Quicksort ✗.
• Scaling note: extra compute on one decomp copy helps to ~1200 model calls then pass@2 preferred; sequential crossover much earlier (~22 calls).

DIY-relevant patterns

• Harness shape: Loom/Velvet method + invariants → lake/REPL → cvc5 auto → Lean fallback → trajectory dumps + viewer (scripts/build_viewer_data.py / serve_viewer.py).
• Adopt for Herdr-style fleets: hybrid SMT+ITP gate on imperative code; subgoal decomposition when single-agent plateaus; imperativeness/anti-leak judge; Loogle MCP for theorem search. Configs under configs/ (decomp), configs/other_models/ (linear), configs/ablation/.
• Skip/caveat: CC-BY-NC (non-commercial); Clever-Loom ≠ CLEVER end-to-end staged pipeline (WybeCoder gets 62% on Loom-translated implementation VCs; CLEVER paper’s few-shot/COPRA end-to-end is ~1/161 — different task). Requires Lean+Loom+cvc5 install (lake update, Loom CaseStudies Mathlib REPL, loogle cache).
• Named after Edsger Wybe Dijkstra.

Gaps / confidence

• Project page + README are primary (paper PDF not parsed here). Disprove path exists on sequential Verina but not on subgoal decomp. Confidence high on architecture/numbers from project page tables; medium on transfer to non-Loom DIY stacks without re-benching.