arxiv-2606.06523-lean4agent

Extract — Lean4Agent / FormalAgentLib: Formal Modeling and Verification for Agent Workflow and Trajectory

URL: https://arxiv.org/abs/2606.06523 (+ html https://arxiv.org/html/2606.06523)
Fetched: 2026-09-27 ~19:34 CST · defuddle parse abs + html —md
Authors: Ruida Wang, Jerry Huang, Pengcheng Wang, Xuanqing Liu, Luyang Kong, Tong Zhang
Code: https://github.com/RickySkywalker/Lean4Agent (promised open-source “near future” in paper; brief also lists this repo)
Stack: Lean v4.20.0; AgentSPEX YAML workflows; FormalAgentLib (151 types / 611 fns / 41 theorems, mostly human-written); LeanEvolve refinement

First (authors’ claim) framework using dependent-type FL (Lean 4) to uniformly model & verify LLM agent workflows and execution trajectories — not verified code, but verified agent process specs.
FormalAgentLib three layers:
1. Structural: workflow graph well-formedness (variables, StepType step vs task, edges: seq/branch/loop) — compiler-analogue.
2. Semantic: predicate system on explicit + implicit/graph-level vars (info-flow, context visibility); Hoare-style pre/post per node; verify under LLMExec axiom (“if pre holds, LLM can establish post”). Automates via type matching + Hoare + library theorems. Correct-by-construction under assumptions.
3. Trajectory: check rollouts against contracts via Lean props, external Python validators, and LLM-as-judge; localize failing step for repair.
LeanEvolve: when Layer-2 passes but task fails — formal-guided evolve (Layer-3 localization + optional env feedback) + optional pure-LLM evolve add-on for broader exploration; then rerun.
Distinct from verifying tool artifacts / SMT action policies / temporal logic alone: targets long-horizon black-box LLM steps + implicit information flow.

Setup: 40 workflows + Layer-2 specs via Claude-Opus-4.6; eval on 5 LLMs (GPT-5.2, GLM-5, Kimi-K2.5, Qwen-3.5-27B, Gemma-4-31B-it); hard SWE-Bench-Verified subset + ELAIP-Bench subset; temp 1.0, ctx 163840.
Table 1 — pass vs fail Layer-2: SWE avg +14.80% (58.27% vs 43.47%; 95% CI [10.00, 19.60]); ELAIP +9.07% (36.60% vs 27.53%; CI [5.66, 13.07]). Combined headline +11.94%. Larger gains for smaller models (Gemma SWE +27.33%).
Claude 4.5 Opus (50 hard SWE only): pass 67.33% vs fail 56.67% (+10.67%).
LeanEvolve (SWE): +7.47% avg solved; overall hard-subset 56.93% → 64.40%. Per-model add: GPT-5.2 +8.00%→70.67%; Qwen +10.67%→60.00%.
Formal-guided vs pure-LLM evolve (ELAIP initially-failed cases): formal solves +7.00% more on avg (e.g. GPT-5.2 25% vs 18.33%).
Ablations: drop graph-level predicates → ELAIP failing workflows 21/40 → only 8 still fail (many defects graph-only). Drop pure-LLM evolve → still +5.07% avg (2.40% less than full).
Layer-2 repair case: fixing context-isolated→context-aware tasks: GPT-5.2 52%→62% on 50 hard SWE.
LLM-as-judge (GPT-5.5) aligns with FormalAgentLib on ELAIP but weakly on SWE — misses implicit flows / graph predicates.
Cost footnote: ~$4k API (large models) + ~1500 GPU-h (small).

Adopt for Herdr/orchestrator: treat workflow YAML as a verifiable artifact; Lean (or lighter) contracts on info-flow & context continuity before rollout; trajectory localization → targeted prompt/step repair (LeanEvolve pattern); don’t rely on LLM-as-judge alone for SWE-like workflows.
LLMExec is the trust bottleneck: Layer-2 is conditional soundness, not absolute FV of agent behavior. Layer-3 checks the assumption on concrete traces.
Skip/overclaim risk: “verified agent” here ≠ verified product code; structural linters alone are weak (frontier models rarely fail Layer-1). Repo may still be incomplete at fetch time.
Complements code-level FV (Vero/CLEVER/WybeCoder/BMC/Specula): this is the meta layer — verify the agent’s plan graph.

Open-source timing uncertain (“near future”). Experiments on curated workflow sets (3 pass + 3 fail sampled), not all generated. Confidence high on architecture & DIY meta-harness idea; medium on absolute % lifts as fleet KPIs (subset sizes, workflow sampling). LLMExec axiom must be stated explicitly in any DIY adoption.