Formal verification in agent-driven development (deep)
Deep brief — Formal verification × agent-driven development
Section titled “Deep brief — Formal verification × agent-driven development”Locked scope
Section titled “Locked scope”In: Agent propose → deterministic checker → repair loops; Lean 4 + mathlib agent tooling; Bend2 (bendlang/bend) vs Bend1; SMT/BMC/Dafny/Verus/TLA+/Cedar-style gates; benches and failure modes; DIY fleet patterns relevant to Noa’s Herdr/orchestrator context.
Out: Brand/Design work; vault hygiene; implementing production code in this run; treating “LLM said verified” as FV.
Seed digest (quick pass, do not overwrite blindly): 2026-09-27 Formal verification in agent-driven development
Time budget: ~2h from start → deadline in frontmatter. Quiet continues until Close or block.
Source table
Section titled “Source table”| url | why-it-matters | priority | status |
|---|---|---|---|
| https://arxiv.org/abs/2608.13522 | Vero paper: repo-level Lean 4 code+proof bench; headline 27/43 full solves — sets realistic expectations | high | done |
| https://vero.verina.io/ | Vero leaderboard + harness docs; companion to paper for DIY eval patterns | high | queued |
| https://github.com/sunblaze-ucb/vero | Vero benchmark + sandbox grading code (Lean multi-module instances) | high | queued |
| https://github.com/bendlang/bend | Bend2 primary toolchain (LAWS.bend / PROOF.bend, BendRT); Apache-2.0 | high | done |
| https://bend2.dev/notes/what-is-bend2/ | Independent technical notes: maturity, no tactics, Lean formalization mismatches | high | done |
| https://bend2.dev/notes/bend2-vs-lean/ | Direct Bend2 vs Lean comparison for fleet design choices | high | done |
| https://bend2.dev/learn/proofs/ | Canonical Bend proof workflow (law/def, {==}, rewrite motives) | high | done |
| https://arxiv.org/abs/2605.21434 | Agentic Model Checking / BMC-Agent: agents propose, CBMC/Kani verify | high | done |
| https://github.com/agentic-prover/aprover | AProver/BMC-Agent runnable harness (C/Rust/Java BMC backends) | high | queued |
| https://arxiv.org/abs/2608.30803 | Schwarz: solver-aware obligation-local SMT repair (95.2% agentic-verif; 91.5% SV-COMP subset) | high | done |
| https://arxiv.org/html/2606.32007 | AxDafny: verifier-guided Dafny agent; 725/782 DafnyBench | high | done |
| https://arxiv.org/abs/2409.13082 | AutoVerus: multi-agent Verus proof synthesis for Rust | high | done |
| https://arxiv.org/abs/2512.18436 | VeruSAGE: agent-based Verus for systems; coding agents often competitive | high | queued |
| https://github.com/microsoft/verus-proof-synthesis | AutoVerus/VeruSAGE code + benches | med | queued |
| https://github.com/facebookresearch/wybecoder | WybeCoder: prove-as-you-generate imperative code via Lean Velvet/Loom + cvc5 | high | done |
| https://arxiv.org/html/2607.25333v1 | Specula: autonomous TLA+/TLC specs + models for system code; 249 bugs / 48 projects | high | done |
| https://github.com/specula-org/Specula | Specula implementation for DIY TLA+ agent loops | med | queued |
| https://aws.amazon.com/blogs/security/why-policy-in-amazon-bedrock-agentcore-chose-cedar-for-securing-agentic-workflows/ | AgentCore Cedar: NL→policy + Cedar Analysis as formal authz gate | high | done |
| https://aws.amazon.com/blogs/opensource/introducing-cedar-analysis-open-source-tools-for-verifying-authorization-policies/ | Cedar Analysis OSS (Lean symbolic compiler + CLI) | med | queued |
| https://arxiv.org/abs/2505.13938 | CLEVER: staged Lean spec→equiv→impl→prove; non-computable specs anti-leak | high | done |
| https://github.com/trishullab/clever | CLEVER benchmark + evaluation harness | med | queued |
| https://arxiv.org/abs/2606.06523 | Lean4Agent / FormalAgentLib: verify agent workflows/trajectories in Lean, not only code | high | done |
| https://github.com/RickySkywalker/Lean4Agent | Lean4Agent code for FormalAgentLib / LeanEvolve | med | queued |
| https://cs.stanford.edu/people/brando9/professional_documents/papers/NeurIPS_2026_VeriBench.pdf | VeriBench: Python→Lean autoformalization; agent-skill ~0.1–0.29 | high | done |
| https://arxiv.org/html/2602.18307v1 | VeriSoftBench: repo-scale Lean software proof obligations (~41% best) | med | queued |
| https://arxiv.org/abs/2602.11136 | FormalJudge: Dafny+Z3 neuro-symbolic oversight vs LLM-as-judge | med | queued |
| https://arxiv.org/html/2507.15225 | Delta Prover: Lean decomposition + iterative reflection (math; harness patterns transferable) | med | queued |
| https://github.com/DimitriosThomaidis/AutoProv | AutoProv: Dafny in Docker+GHA specifier→coder→verify→repair CI pattern | med | queued |
| https://lean-lang.org/ | Lean 4 official site — kernel/lake/mathlib entry for DIY harness wiring | med | queued |
| https://github.com/HigherOrderCO/Bend | Bend1/HVM2 ancestor — disambiguation only (do not conflate with Bend2) | med | queued |
| https://github.com/verus-lang/verus | Verus primary verifier docs/repo (SMT Rust contracts baseline) | med | queued |
| https://x.com/bcherny/status/2102543349102338309 | Cherny: Lean/TLA+ on Agent SDK — model→CEx→fix (buzz vs FV framing) | med | done |
| https://x.com/bcherny/status/2102803868837126172 | Cherny clarification: “verify” = model bugfinding, not product-level FV | high | done |
| https://x.com/rv_inc/status/2102843017560510772 | Runtime Verification: buzz vs real FV; Specula/Lean; model≠runtime | high | done |
| https://x.com/VictorTaelin/status/2102764825231470862 | Taelin: proof economics (1 LOC → tens of proof); AI shifts cost calculus | med | queued |
First Read batch (top 8)
Section titled “First Read batch (top 8)”- https://arxiv.org/abs/2608.13522 — Vero
- https://github.com/bendlang/bend — Bend2 README
- https://bend2.dev/notes/what-is-bend2/ — Bend2 maturity
- https://bend2.dev/notes/bend2-vs-lean/ — Bend2 vs Lean
- https://arxiv.org/abs/2605.21434 — BMC-Agent / Agentic Model Checking
- https://arxiv.org/abs/2608.30803 — Schwarz
- https://arxiv.org/abs/2409.13082 — AutoVerus
- https://aws.amazon.com/blogs/security/why-policy-in-amazon-bedrock-agentcore-chose-cedar-for-securing-agentic-workflows/ — Cedar AgentCore
Map gaps (for later batches)
Section titled “Map gaps (for later batches)”- AdaCore SPARK / GNAT Foundry Intersection: only X discussion in seed; need primary AdaCore docs
- VeriBench: Stanford PDF read (NeurIPS_2026_VeriBench.pdf); no stable arXiv abs yet in Map
- AutoRocq / KVerus: cited inside Schwarz related work; no dedicated primary read yet
- BendTT / BendRT Lean formalization papers mentioned in seed — URLs not locked
- TLA+ / TLC official docs for DIY Specula-style gates (secondary)
- Cherny second clarification thread (2102898067133595992) — confirm permalink in Read
Open questions
Section titled “Open questions”- Prefer one deep companion digest vs several split Digests (Lean / Bend2 / DIY playbook)? Default: several focused digests + this brief as index.
Running notes
Section titled “Running notes”-
Map complete 2026-09-27 ~19:45 CST: 35 sources queued (WebSearch + GitHub MCP + X + light arXiv fetch). Status→reading; first batch = top 8.
-
Scope locked from Noa: “Deep research in this field” after the quick FV digest + Lean/Bend2 asks.
-
Read batch 1 in flight (2026-09-27 ~19:32): Vero, Bend2×3, BMC-Agent, Schwarz, AutoVerus, Cedar AgentCore.
-
Read batch B done 2026-09-27 ~19:34 CST (executor, no Codex): BMC-Agent (arXiv 2605.21434 html), Schwarz (2608.30803 html), AutoVerus (2409.13082 html), Cedar AgentCore AWS blog — all via
defuddle parse --md. Extracts undersources/arxiv-2605.21434-bmc-agent.md,arxiv-2608.30803-schwarz.md,arxiv-2409.13082-autoverus.md,aws-agentcore-cedar-policy.md. Headline DIY takeaways: (1) agents-propose/solvers-verify with CBMC/Kani + CEx realism tiers (62 confirmed bugs; VibeOS 34/145); (2) Schwarz obligation-local SMT repair 95.2%/91.5% — lemmas beat theory policies in ablation; (3) AutoVerus 137/150 Verus-Bench via 3-phase gen→refine→debug + Lynette cheat-filter; (4) Cedar as analyzable default-deny tool gate (NL→policy only with Analysis). No Digests written this batch. -
Read batch A done 2026-09-27 ~19:35 CST (Vero + bendlang/bend + what-is-bend2 + bend2-vs-lean). Extracts under
_deep/formal-verification-agents/sources/. No Digests/ yet.- Vero (arXiv:2608.13522): first repo-level Lean4 code+proof bench; 43 instances / 743 APIs / 2,705 specs; best GPT-5.5 xhigh 27/43 cp (25 po); 10 untouchable; 87%+ spec pass ≠ full solve; audit found 38 defects pre-release; ~$106/full-solve; anti-cheat layers (axioms, implemented_by).
- Bend2 README: LAWS.bend (human) + PROOF.bend (AI) +
bend PROOF.bendgate;--safe→ BendTT Lean kernel (v4.34.0); no tactics; Bend1/HVM incompatible; compiler 99% AI-written / checker unproven except--safe. - what-is-bend2: maturity 2.0.5; explicit proofs only; checker↔Lean formalization mismatches; foreign/IO outside proofs; fixed-assignment parallelism (no work-steal); M4 Max Life 7.8s→0.06s GPU.
- bend2-vs-lean: choose Bend for affine+CPU/GPU executable laws; Lean for mathlib/tactics; checker 0.295s vs Lean 36s on 12.8k synthetic defs — not a mathlib port; don’t pick on check speed alone.
-
Read batch 2 split: 2A (WybeCoder, Specula, CLEVER, Lean4Agent) done — see note below; 2B (VeriBench, AxDafny, Cherny/RV X, bend proofs) done.
-
Read batch 2B done 2026-09-27 ~19:36 CST (executor, no Codex): VeriBench PDF, AxDafny html, Cherny×2 + RV Inc X, bend2.dev/learn/proofs. Extracts:
veribench-neurips-2026.md,arxiv-2606.32007-axdafny.md,x-bcherny-lean-agent-sdk.md,x-rv-inc-buzz-vs-real-fv.md,bend2-learn-proofs.md. Highlights: (1) VeriBench SCSC agent-skill Codex/Claude/Leanstral 0.289/0.224/0.103 — IC1=1.0 but TE1≤0.105 (theorem-equivalence gap); (2) AxDafny 725/782 (92.7%) DafnyBench, LCB-Pro-Dafny 56.4% vs 11.6% pass@1, verify≠runtime (TLE dominant); (3) Cherny: Lean/TLA+ Agent SDK → 16 PRs, then clarifies “verify” = model→CEx→repro→fix; (4) RV Inc: buzz vs real FV — model≠runtime needs faithful translation + trusted semantics + checkers; Specula/K/Lean already useful; (5) Bend proofs tutorial: law/def,{==},%ih : motivewith_, Empty elim. No Digests. Parallel 2A untouched. -
Read batch 2A done 2026-09-27 ~19:36 CST (executor, no Codex): WybeCoder (GitHub README + project page), Specula (arXiv 2607.25333 html+abs), CLEVER (2505.13938 abs+html), Lean4Agent/FormalAgentLib (2606.06523 abs+html) — prefer
defuddle parse --md(GitHub via MCP). Extracts:wybecoder-verified-imperative-code-generation.md,arxiv-2607.25333-specula.md,arxiv-2505.13938-clever.md,arxiv-2606.06523-lean4agent.md. Highlights: (1) WybeCoder prove-as-you-generate Velvet/Loom+cvc5 — Verina 74.1% / Clever-Loom 62.1% (Opus 4.5 32×16); Heapsort w/ 357 sub-agents; CC-BY-NC; Clever-Loom ≠ CLEVER E2E; (2) Specula TLA+/TLC agent loops — 249 bugs / 48 projects, 68 confirmed / 24 fixed, 0 FP (reproduced), median ~3.7h /$57, bidirectional trace-val+MC anti-reward-hack; (3) CLEVER staged Lean anti-leak — E2E ≤1/161 (~0.62%), non-computable Prop specs; (4) Lean4Agent FormalAgentLib verifies workflows/trajectories under LLMExec — pass vs fail Layer-2 +14.8% SWE / +9.1% ELAIP; LeanEvolve +7.47% SWE. No Digests/. -
Synthesize in flight (~19:35): writing Lean, Bend2, and DIY playbook companion digests from extracts.
-
Synthesis done 2026-09-27 ~19:40 CST (executor, no Codex; Digests only; quiet). Read all 18 extracts under
sources/. Wrote three companion digests (seed untouched):Digests/2026-09-27 Lean 4 agents for verified software.md— harness wiring (lake/kernel/axiom allowlist); Vero 27/43, CLEVER ≤1/161, VeriBench skill 0.10–0.29, VeriSoft~41%; WybeCoder 74.1%/62.1% Clever-Loom (≠ CLEVER E2E); Lean4Agent FormalAgentLib (+14.8% SWE Layer-2); Cherny model→CEx→fix vs RV three-trust chain; DIY CI gates.Digests/2026-09-27 Bend2 for verified parallel agents.md— Bend2 vs Bend1/HVM; LAWS/PROOF/bend PROOF.bend --safe; vs Lean (tactics/mathlib vs explicit+BendRT); maturity (AI compiler, checker mismatches, no tactics); when-to-use for fleets.Digests/2026-09-27 Agent FV toolbox and DIY playbook.md— propose→verify→repair map across BMC-Agent/Schwarz/AutoVerus/AxDafny/Specula/Cedar; comparison table; Herdr DIY recipe + overclaim traps + confidence.
-
Status→synthesizing (phase 3). Next: Close — delete continue routine and notify Noa. Parent owns Close notification.
-
Close completed (~19:37): three companion digests written; continue routine deleted; Noa notified.