Lean 4 agents for verified software

Confidence

Claim	Confidence	Note
Lean kernel + `lake` is the right DIY ITP gate	High	Seed + Vero/CLEVER/VeriBench harnesses all assume kernel authority outside the model
Repo-scale verified generation is production-ready	Low	Vero best full-solve 27/43; 10 instances untouchable (arXiv:2608.13522)
Cherny Lean/TLA+ Agent SDK work = product FV	Low as FV; Medium as bugfinding	Author clarified model→CEx→reproduce→fix (x.com/bcherny); RV: model≠runtime (rv_inc)
WybeCoder Clever-Loom % ≈ CLEVER E2E	False equivalence	Clever-Loom 62.1% on translated Loom VCs; CLEVER E2E ≤1/161 — different tasks

1. Harness wiring (kernel, mathlib, lake, CI)

Lean 4 elaborates source + tactics into proof terms checked by a small trusted kernel; mathlib supplies lemmas/tactics; lake build is the hard gate for DIY fleets ([seed](Digests/2026-09-27 Formal verification in agent-driven development); lean-lang.org).

Piece	Agent role	Fail-closed check
Elaborator / `lake build`	Propose Lean → compile → repair on errors	Build must succeed on agent-touched modules
Kernel	Authoritative soundness	No smuggled axioms beyond allowlist
mathlib + search (Loogle / LeanSearch)	Lemma retrieval	Mis-picked theorems are a top failure mode
Tactics (`simp`, `rw`, `induction`, …)	Produce kernel-checked terms	Prefer tactic scripts that elaborate cleanly over opaque macros
Anti-cheat (Vero-style)	Prevent hollow “proofs”	Slot-scoped re-render; reject `native_decide` abuse, hollow typeclasses, `@[implemented_by]` oracle split; print axiom allowlist (Classical.choice / propext / Quot.sound + trusted) (Vero extract)

Eval pins seen in extracts: Vero Lean v4.29.1; Lean4Agent v4.20.0; BendTT Lean pin v4.34.0 (separate stack). Pin one toolchain per fleet job.

2. Benchmarks — realistic expectations

Vero — repo-level code+proof (arXiv:2608.13522 · github.com/sunblaze-ucb/vero · vero.verina.io)

First repo-level Lean 4 joint code+proof bench: 43 multi-module instances, 743 APIs, 2,705 specs (from Python/Dafny/Verus/Coq sources).
Best agent (GPT-5.5 xhigh): 27/43 full solves (code+proof), 25/43 proof-only; 10 untouchable in both modes.
Spec pass 87.3% (best cp) ≠ repo completion — shared invariants, lemma libraries, build consistency dominate failures.
Cost: ~ $2,865** / 43 instances (~**$ 106 / full solve); ~23% of spend on the 10 unsolvable.
Formal audit during curation found 38 spec defects (+ joint-unsat groups) before release — agents can also prove ref-impl incorrectness / unsat.

CLEVER — staged anti-leak E2E (arXiv:2505.13938 · trishullab/clever)

161 HumanEval-derived problems. Success = (1) NL→Lean spec ψ + proof ψ ≅ held-out ψ*; (2) impl π + proof π satisfies ψ* (ground truth, not model’s ψ).
Specs are non-computable Prop (quantifiers/inductives) to block copy-spec-into-impl + simp vacuity.
End-to-end full solve ≤1/161 (~0.62%) across evaluated few-shot/COPRA setups — frontier hardness.
Spec compile can be 71–90% while spec proved and E2E stay near zero.

VeriBench — Python→Lean autoformalization (Stanford PDF)

Agents emit Lean impl + tests + theorems + proofs from executable Python; Harbor sandbox harness.
Headline agent-skill (S_e = (IC_1 \cdot IC_2 \cdot TE_1)^{1/3}): Codex 0.289, Claude Code 0.224, Leanstral 0.103.
IC1=1.0 (typecheck) for Codex/Claude Code, but TE1≤0.105 — theorem↔gold semantic gap is at least as hard as proof search.
TE1 uses Claude Sonnet 4.6 LLM judge (proxy, not kernel bi-implication); treat as estimate.

VeriSoftBench (seed / brief)

Repo-scale Lean software proof obligations; best ~41% with curated context (seed table). Use as secondary calibration alongside Vero.

Contrast table

Bench	Task	Headline
Vero	Fill Lean multi-module code+proofs	27/43 full solves
CLEVER	Spec→equiv→impl→prove E2E	≤1/161
VeriBench	Python→Lean autoformalization	Skill ~0.10–0.29
VeriSoftBench	Lean software POs	Best ~41%
WybeCoder Verina / Clever-Loom	SMT+Lean hybrid imperative VCs	74.1% / 62.1% (≠ CLEVER E2E)

3. WybeCoder — prove-as-you-generate (facebookresearch/wybecoder)

Stack: Velvet (Dafny-like imperative DSL) in Lean 4 via Loom; VCG → cvc5; leftover goals interactive Lean; optional Loogle MCP.
Pattern: code + invariants + proofs co-evolve (not write-then-verify). Sequential agent (pass@k) or subgoal decomposition (parallel sub-provers + conflict-driven repair).
Verina: best 74.1% (Opus 4.5, 32×16); Clever-Loom: 62.1%. Heapsort verified with 357 sub-agents.
Imperativeness Judge rejects functional/spec leakage so solutions stay genuinely imperative.
License CC-BY-NC 4.0 — non-commercial constraint for DIY product use.
DIY adopt: hybrid SMT+ITP gate; subgoal decomp when single-agent plateaus; anti-leak judge. Do not cite Clever-Loom as CLEVER E2E.

4. Lean4Agent / FormalAgentLib — verify workflows, not only code (arXiv:2606.06523 · RickySkywalker/Lean4Agent)

Models agent workflows/trajectories in Lean (AgentSPEX YAML → FormalAgentLib).
Three layers: (1) Structural graph well-formedness; (2) Semantic Hoare-style contracts under LLMExec axiom (“if pre holds, LLM can establish post”); (3) Trajectory check rollouts + localize failing step.
Pass vs fail Layer-2: SWE +14.8%, ELAIP +9.1%; LeanEvolve +7.47% SWE on initially-failed cases.
LLM-as-judge aligns on ELAIP but weakly on SWE (misses implicit flows / graph predicates).

5. Cherny vs real FV

Source	What happened	What it is
Cherny claim	Opus “formally verify” Claude Agent SDK with Lean; 16 PRs; also TLA+	Viral framing as FV
Cherny clarification	“Verify” loose → model hairiest SM → find CEx → reproduce → fix	Model bugfinding
RV Inc	Both excitement and skepticism have a point; Specula/K/Lean already useful	Need faithful translation + trusted semantics + trusted checkers before product FV

6. DIY CI gate patterns (Lean-specific)

Herdr / orchestrator job
  → coding agent edits Lean modules
  → lake build (+ mathlib sync cache)
  → axiom / sorry / implemented_by allowlist scan
  → optional: Vero-style clean-tree re-check
  → on fail: repair ≤ N rounds (feed elaborator errors; optional Loogle)
  → on pass: PR + human on NEW specs / invariant classes

Copy from benches:

Full-repo gate as success (Vero) — not per-lemma %.
Non-computable specs + held-out ψ* (CLEVER) for any “verified codegen” claim.
Conjunctive scores (VeriBench SCSC) — IC1 alone is useless.
Hybrid SMT discharge + Lean fallback (WybeCoder) when imperative VCs dominate.
Workflow YAML contracts (Lean4Agent) as a meta-layer before rollout.
Spec / law human review before trusting green CI (Cherny/RV).

Skip / defer: scoring on typecheck alone; equating Clever-Loom to CLEVER; claiming product FV from Lean models of TS/Python without faithful semantics; unbounded trust in LLMExec.

Sources

Vero — arXiv:2608.13522 · extract sources/vero-can-ai-agents-build-formally-verified-software-repositories.md
CLEVER — arXiv:2505.13938 · sources/arxiv-2505.13938-clever.md
VeriBench — NeurIPS 2026 PDF · sources/veribench-neurips-2026.md
WybeCoder — github.com/facebookresearch/wybecoder · sources/wybecoder-verified-imperative-code-generation.md
Lean4Agent — arXiv:2606.06523 · sources/arxiv-2606.06523-lean4agent.md
Cherny / RV — sources/x-bcherny-lean-agent-sdk.md, sources/x-rv-inc-buzz-vs-real-fv.md
Seed — 2026-09-27 Formal verification in agent-driven development