Formal verification in agent-driven development

Formal verification in agent-driven development

One-liner

Treat agents as proposal engines and deterministic checkers (SMT, BMC, kernels, model checkers, policy analyzers) as soundness gates: generate specs → generate code+proofs → verify in CI → repair on failure. Buzz (“LLM verified it”) ≠ real FV; the checker must be outside the model.

Related: 2026-09-26 Cloud agent orchestrators in the wild · 2026-09-26 Herdr for v0 cloud orchestrator · 2026-09-27 Cloudflare Code Mode · Cloud agent orchestrator

---

Confidence / disambiguation

Claim	Confidence	Note
Agents + hard checkers is the durable pattern	High	Academic (AProver/BMC-Agent, Schwarz, AxDafny, WybeCoder, AutoVerus) + industry (AgentCore Cedar, AutoProv-style CI) converge on agents propose, solvers verify
Repo-scale end-to-end verified generation is solved	Low	Vero: best agent fully solves only 27/43 Lean 4 multi-module instances; VeriBench agent-skill scores ~0.1–0.29
Cherny “formally verified the Agent SDK with Lean”	Medium as bug-finding; Low as full FV	Author later clarified: model hairiest state machines → find CEx → reproduce → fix. rv_inc: model ≠ runtime code
Bend2 as production FV+parallel stack	Medium (language real); Low (maturity)	Public Apache-2.0 toolchain at bendlang/bend; young; no tactics; Lean formalization of core has documented mismatches with implementation
“Types as proofs” / LLM-as-judge as FV	Buzz unless kernel/SMT discharges	Dependent-typed proofs and SMT-backed contracts are FV; vibe checks and LLM judges are not

Name collisions

Name	What it is	Use here?
Lean 4	Dependent-type theorem prover + programming language; mathlib	Yes — primary interactive prover for agents
Bend 1 / HigherOrderCO/Bend	Massively parallel language on HVM2; no dependent laws in published syntax	Related ancestor only
Bend 2 / bendlang/bend	New language: affine dependent types + LAWS.bend proofs + BendRT CPU/GPU	Yes — treat as Bend2
Unrelated “Bend” (Iron Man, street slang, etc.)	Ignore	No

---

1. What formal verification means here

In agent-driven development, formal verification (FV) means: a property is stated in a precise language, and a deterministic tool either proves it, finds a counterexample, or fails/times out — independent of the LLM’s confidence.

Rough taxonomy

Family	What you get	Tools	Agent role
Deductive / contract	Impl satisfies requires/ensures (or Verus specs) via SMT	Dafny, Verus, F*, Frama-C/WP, SPARK	Propose impl + invariants + lemmas; repair on VC failure
Interactive theorem proving	Kernel-checked proof terms	Lean 4, Rocq/Coq, Isabelle/HOL, Agda	Propose tactics/terms; iterate on elaborator errors; search mathlib
Model checking	Exhaustive (or bounded) exploration of a model	TLA+/TLC, Alloy, Spin	Autoformalize specs/models; classify CEx; refine abstractions
Bounded model checking (BMC)	Bit-precise checks up to unwind bound (k)	CBMC, Kani	Infer contracts; build harnesses; validate CEx
Policy / authorization analysis	Analytic properties of policy sets	Cedar Analysis (AgentCore Policy)	NL → policy; analysis rejects vacuous/conflicting policies
Types-as-proofs (lightweight)	Encoding safety in the type system	Rust ownership, SPARK, Bend affine ownership	Still need laws for app invariants

Spec gap

Most agent-generated code has no formal spec. The hard problem is often autoformalization (NL/tests → contracts), not closing proofs for a given correct spec. Wrong specs → false “verified” or silent misses.

---

2. How agent workflows use FV

Canonical loop (appears across AProver, AxDafny, AutoProv, Schwarz, AutoVerus, WybeCoder):

NL / issue / AGENTS.md
        │
        ▼
┌───────────────────┐
│ Specifier agent   │  → contracts, TLA invariants, LAWS.bend, Cedar policies
└─────────┬─────────┘
          ▼
┌───────────────────┐
│ Coder / prover    │  → code + proof annotations / Lean terms / Bend proofs
└─────────┬─────────┘
          ▼
┌───────────────────┐
│ Hard checker (CI) │  dafny verify | verus | lake build | cbmc | tlc | bend PROOF.bend | cedar analyze
└─────────┬─────────┘
     pass │ fail
          ▼
┌───────────────────┐
│ Repair agent      │  feed diagnostics / CEx / obligation snapshots → patch → re-verify
└───────────────────┘

Workflow variants

1. Generate specs only — then humans or separate agents implement (Specula TLA+; Cedar NL→policy).
2. Generate code + proofs together (“prove-as-you-generate”) — WybeCoder (Velvet/Loom in Lean 4), AxDafny, Vero code+proof mode.
3. Proof-only — impl fixed; restore invariants (DafnyBench, AutoVerus, Vero proof mode).
4. Verify-in-CI / fail-closed — AutoProv (Dafny in Docker sandbox + GHA); AdaCore GNAT Foundry Intersection (SPARK + tests + coverage gate agent edits).
5. Repair-on-failure — verifier diagnostics → local obligation repair (Schwarz makes SMT failures local; AxDafny feeds dafny verify messages).
6. Hybrid PBT + formal — property-based tests for broad surface; FV on crypto boundaries, parsers, concurrency cores, authz. Cheap coverage + expensive proofs where it matters.
7. Model-then-bugfind — agent builds Lean/TLA model of a subsystem, finds CEx, reproduces on real code, patches (Cherny/Agent SDK workflow — valuable, not full FV).

---

3. Concrete tools, projects, papers, products

Agent harnesses already doing this

Project	Stack	Pattern	Links
AProver / BMC-Agent	LLM + CBMC (C) / Kani (Rust)	Agentic model checking: top-down specs, compositional BMC, CEx validation, CEGAR-style refinement	github.com/agentic-prover/aprover · arXiv:2605.21434
Schwarz	Agent + SMT (C, Rust/Verus)	Solver-aware obligation-local repair; 95.2% on agentic-verif bench; 91.5% SV-COMP ReachSafety subset	arXiv:2608.30803
AxDafny	Dafny + AxProverBase agents	Verifier-guided repair; 725/782 DafnyBench (92.7%)	axiomatic-ai.com/blog/axdafny · arXiv HTML
WybeCoder	Lean 4 / Velvet / Loom + cvc5	Prove-as-you-generate imperative code; subgoal decomposition	facebookresearch/wybecoder
AutoVerus / VeruSAGE	Verus (Rust)	Multi-agent proof repair; generic coding agent + Verus often competitive	microsoft/verus-proof-synthesis · arXiv:2409.13082 · VeruSAGE arXiv:2512.18436
AutoProv	Dafny in zero-trust Docker + GHA	Specifier → Coder → Verifier → Repair → transpile to Python	DimitriosThomaidis/AutoProv
Specula	TLA+ / TLC + agents	Autonomous specs + models for system code; trace validation	arXiv:2607.25333 (also cited by Runtime Verification)
Lean4Agent / FormalAgentLib	Lean 4	Verify agent workflows/trajectories (structural / semantic / runtime), not only program proofs	RickySkywalker/Lean4Agent
AutoRocq	Rocq/Coq	Iterative proof agent for program verification	ACM FSE companion framing; generate-and-validate with coding agents
FormalJudge	Dafny + Z3	Neuro-symbolic oversight vs LLM-as-judge	arXiv:2602.11136
Cedar / AgentCore Policy	Cedar + Cedar Analysis	NL→policy; schema validation; symbolic analysis; runtime allow/deny at Gateway	AWS Security Blog · neselab/cedar-synthesis-engine
AdaCore Intersection	Ada/SPARK	Agents edit; formal proof + tests + coverage + traceability gate	Discussion: x.com/SteelbridgeSol/status/2103405247565603078

Benchmarks (reality check)

Bench	What it measures	Headline
Vero	Repo-level Lean 4 code+proof	Best agent 27/43 full solves (vero.verina.io · arXiv:2608.13522)
CLEVER	Spec → prove equiv → impl → prove	Staged Lean pipeline (trishullab/clever · arXiv:2505.13938)
VeriBench	Python→Lean autoformalization	Agent-skill ≈ 0.29 / 0.22 / 0.10 (Codex / Claude Code / Leanstral)
VeriSoftBench	Real Lean 4 repo proofs	Best ~41% with curated context
DafnyBench	Restore proof hints	AxDafny 92.7%

---

4. Lean 4 deeply (theorem prover / mathlib / agent workflows)

What Lean is

Lean 4 is both a dependently typed programming language and an interactive theorem prover. Source and tactic scripts elaborate into proof terms checked by a small trusted kernel. mathlib is the large community library of definitions, lemmas, and tactics — the reuse layer that makes Lean practical for math and for software formalization (once APIs are stated in Lean).

Piece	Role for agents
lake build / elaborator	Hard gate: no sorry, no smuggled axioms (benchmarks enforce allowlists)
mathlib + LeanSearch	Lemma retrieval; agents fail often by mis-picking theorems
Tactics (simp, rw, induction, …)	Automation that produces kernel-checked terms
Native compilation / Tasks	Can run verified code; concurrency is explicit, not Bend-style auto-GPU

Agent + Lean patterns

1. Interactive repair loop — propose Lean → compile → feed errors → retry (Delta Prover, AxProverBase-style minimal agents, COPRA lineage).
2. Decomposition — informal plan → formal lemmas → prove leaves → assemble (DSP / LEGO-Prover / OpenProver Planner–Worker–Verifier).
3. Library-augmented search — REAL-Prover / OpenProver lean_search over mathlib.
4. Verified code generation — CLEVER / Verina / WybeCoder / Vero: impl + machine-checked specs, not only math olympiad proofs.
5. Verified agent workflows — Lean4Agent FormalAgentLib: type-check workflow graphs and trajectory obligations under assumptions (LLMExec).
6. Hardware — CircuitProver: Verilog/specs → Lean models + reusable proof libraries.
7. Bug-finding models — Cherny: model SDK state machines in Lean/TLA+, hunt CEx, fix real code (x.com/bcherny/status/2102543349102338309, clarification …/2102898067133595992).

Lean vs “math-only” vs “software FV”

• AlphaProof-class systems excel at contest math; transferring to multi-module software repos is exactly what Vero stress-tests — and scores show the gap.
• Lean is currently the best available public ITP for DIY agent fleets that need mathlib-scale reuse + kernel trust. Cost: context windows, lake sync, tactic fragility, and the need for faithful models of the runtime language (Python/TS/Rust semantics are not free).

DIY Lean gate

In CI: lake build on agent-touched modules; reject sorry / extra axioms; optional second job that re-checks a spliced clean tree (Vero-style anti-cheat). Keep human gate on spec review — proofs only show “code meets this spec.”

---

5. Bend2 deeply (disambiguation + agent-driven use)

Disambiguation

Artifact	Org / repo	Runtime	Proof story	Parallelism
Bend 1	HigherOrderCO/Bend	HVM2 interaction nets	No dependent law language in published Bend1 syntax	Automatic parallel reduction; run-cu CUDA
Bend 2 (“Bend2”)	bendlang/bend · bend-lang.com · @bendlang · Victor Taelin @VictorTaelin	BendRT (C; Metal/CUDA via f!)	Dependent types + law / proof def; LAWS.bend + PROOF.bend	Explicit balanced fork/join a b = f(x) g(y); no work stealing
Notes site	bend2.dev	Explains Bend2 vs Lean, ownership, limits	Independent technical notes (2026-09)	—

Bend2 = Bend version 2, not a separate product name. Bend1 sources and HVM do not carry over.

What Bend2 is trying to be

Pitch (upstream README): an ambiguity-free language for communicating intent to AIs — laws more precise than NL, proofs that the AI’s edits obey them, fast CPU/GPU execution. Framing: LAWS.bend ≈ “AGENTS.md backed by proof.”

Workflow for agents:

1. Formalize app rules in LAWS.bend.
2. After every edit, run bend PROOF.bend (or check the file under proof).
3. Fail closed: agent must repair until laws hold.
4. Parallelize divide-and-conquer with fork syntax / ! for GPU.

Core formalization of the safe fragment lives in Lean (bendtt.lean); papers: BendTT, BendRT. Upstream notes mismatches between Lean formalization and the TypeScript checker — treat as “promising young stack,” not a fully metatheory-certified compiler.

Bend2 vs Lean (for fleet design)

Dimension	Lean 4	Bend 2
Proof construction	Terms or tactics; huge automation	Explicit proof terms; no tactics (as of 2.0.5 notes)
Libraries	mathlib ecosystem	Base + demos; small
Parallel / GPU	Tasks / foreign	First-class fork/join + !
Agent maturity	Many harnesses + benches (Vero, CLEVER, …)	Young; community reports agent proof effort can be harder than Lean for same claim (x.com/yalexey/status/2102403180445495313)
Trust story	Mature kernel + public compiler	Public Apache-2.0; checker/compiler still evolving; Victor notes AI still “incredibly stupid” on hard Bend2 work (x.com/VictorTaelin/status/2102750877706584369)

Marketing vs guarantee

Laws only cover what you wrote. Foreign C/JS, DB drivers, and network effects are outside the proof. Weak laws are easy to “prove” and useless. Same failure mode as every other FV stack — Bend’s agent-facing UX just makes it more tempting to overclaim.

When to try Bend2 in a DIY fleet: greenfield numerical / parallel backends where you want agents to own both speedups and a small set of invariants, and you accept young tooling. When to prefer Lean/Dafny/Verus/TLA: anything needing libraries, tactics, existing verified artifacts, or industry analyzers.

---

6. Practical DIY patterns for an agent fleet

Fits Cloud agent orchestrator / Herdr-style runners: verification is a skill + CI gate, not a vibe.

When to verify

Verify (or model-check)	Leave informal / PBT / review
Authz, money, crypto, parsers on untrusted input	UI copy, glue, one-off scripts
Concurrency / state machines / protocols	Soft real-time heuristics
Public API contracts of agent-generated libraries	Internal helpers with few callers
Policy at tool gateway (Cedar-style)	Prompt text itself
Invariants listed in LAWS / AGENTS “must never”	Aesthetics, latency tuning

Cost / latency knobs

• Bounded checks first (BMC unwind (k), TLC state bound, short lake targets).
• Compositional verification (per-function contracts) before whole-program.
• Cache specs/proofs across runs (AProver spec store pattern).
• Tiered: unit tests → PBT → FV on hot modules → human for spec diffs.
• Expect token cost on repair loops; Schwarz-style local obligations beat dumping whole SMT logs.

Human gates (recommended)

1. Spec / law review before trusting a green CI (Cherny/RV point: model fidelity).
2. Threat-model label on findings (AProver: active vs latent public-API).
3. No auto-merge on first proof of a new invariant class.
4. Dual-source specs or triangulation when LLM writes contracts.

Minimal fleet recipe

Herdr / orchestrator job
  → coding agent edits worktree
  → verify skill: (dafny|verus|lake build|cbmc|tlc|bend|cedar) in sandbox
  → on fail: repair agent ≤ N rounds
  → on pass: PR + optional human on spec diff

Optional: Code Mode sandbox (2026-09-27 Cloudflare Code Mode) to run verifiers as typed tools without stuffing MCP schemas into context.

---

7. Limits and failure modes

1. Wrong or weak specs — proof of the wrong property; silent miss if specs too permissive (AProver threat note).
2. Model ≠ code — Lean/TLA model of TS/Python can find real bugs and miss language/runtime gaps (rv_inc).
3. Bounds — BMC/unwind and TLC finite instances don’t imply unbounded correctness.
4. Solver timeouts / unknowns — without solver-aware repair (Schwarz), agents thrash.
5. Proof debt — “1 line of code, tens of lines of proof” (VictorTaelin); AI changes economics but doesn’t erase it.
6. Repo-scale still hard — Vero 27/43; VeriSoftBench ~35–41%.
7. Spec fabrication — LLM invents wrong reference behavior (WybeCoder/BMC-Agent domain-heavy false positives; need realism filters).
8. Buzz inflation — calling any Lean/TLA experiment “full formal verification of the product.”
9. Compiler/metatheory bugs — Bend2 documents checker vs Lean formalization mismatches; proofs don’t catch a wrong compiler.
10. Authorization ≠ functional correctness — Cedar envelopes tools; doesn’t prove the tool’s business logic.

---

8. Sources

Docs / products

• AWS: Why AgentCore Policy chose Cedar
• AxDafny blog (Axiomatic AI)
• Vero benchmark site
• bend-lang.com · What is Bend2? · Bend2 vs Lean

Papers

• Agentic Model Checking — arXiv:2605.21434
• Schwarz — arXiv:2608.30803
• Vero — arXiv:2608.13522
• AxDafny — arXiv HTML 2606.32007
• AutoVerus — arXiv:2409.13082
• VeruSAGE — arXiv:2512.18436
• Specula — arXiv:2607.25333
• CLEVER — arXiv:2505.13938
• FormalJudge — arXiv:2602.11136
• Lean4Agent — arXiv:2606.06523 (PDF variants)
• Delta Prover — arXiv HTML 2507.15225

GitHub

• agentic-prover/aprover
• facebookresearch/wybecoder
• microsoft/verus-proof-synthesis (AutoVerus)
• sunblaze-ucb/vero (per Vero site)
• trishullab/clever
• DimitriosThomaidis/AutoProv
• RickySkywalker/Lean4Agent
• bendlang/bend (Bend2)
• HigherOrderCO/Bend (Bend1 / HVM2)
• HigherOrderCO/HVM2
• neselab/cedar-synthesis-engine

X / Twitter (permalinks)

• Boris Cherny — Lean/TLA+ on Claude Agent SDK: x.com/bcherny/status/2102543349102338309
• Cherny clarification (model → CEx → reproduce → fix): x.com/bcherny/status/2102898067133595992 · …/2102803868837126172
• Runtime Verification — buzz vs real FV; Specula/K/Lean: x.com/rv_inc/status/2102843017560510772
• Naming pedantry (FM ≠ full FV): x.com/ptntlbyrnths/status/2102933041626968189
• Victor Taelin — proof economics: x.com/VictorTaelin/status/2102764825231470862
• Taelin — Bend evolution / agent compute: x.com/VictorTaelin/status/2102507735497470163 · …/2103127951264845889
• Bend2 launch framing: x.com/LomashKumar52/status/2100763954398306757 · x.com/SystemArch_AI/status/2101039581856411899
• Agent proof cost Bend vs Lean: x.com/yalexey/status/2102403180445495313
• AdaCore SPARK agent gate: x.com/SteelbridgeSol/status/2103405247565603078

---

Bottom line for Researchy / Noa

Wire fail-closed checkers into the fleet (Dafny/Verus/Lean lake/CBMC|Kani/TLA+/Cedar/Bend LAWS) behind Herdr/orchestrator jobs; spend humans on specs and threat models; use Lean for deep proofs + mathlib, Bend2 experimentally for parallel+laws greenfields, and never confuse model-based bug finding with product-level formal verification.