PaperlayerView exact revision on arXiv

Source-linked AI summary

Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory

Ruida Wang, Jerry Huang, Pengcheng Wang, Xuanqing Liu, Luyang Kong, Tong Zhang

arXiv:2606.06523v2cs.AIcs.LGcs.LOcs.SE

TL;DR

Formal specification of LLM-agent workflows and execution trajectories remains important as complex agents are deployed in high-stakes domains. Lean4Agent uses dependent-type Lean4 to model and verify agent behavior; experiments report verification-passing workflows outperforming failing ones by 11.94% on average and LeanEvolve improving SWE performance by 7.47% on average.

  • Problem

    As complex LLM-agent workflows enter high-stakes domains, formal specification of both workflows and execution trajectories remains an important research need.

    Source: §1 · pp. 1–2

  • Method

    Lean4Agent uses dependent-type Lean4 to model and verify agent workflows and trajectories, with FormalAgentLib supporting semantic verification and failure localization and LeanEvolve refining workflows using verification feedback.

    Source: §1 · pp. 2–3, §5 · p. 9

  • Results

    11.94% average advantage for verification-passing workflows over failing ones across SWE and paper-understanding tasks, and LeanEvolve yields a further 7.47% average improvement on SWE.

    Source: §5 · p. 10

  • Takeaways & Limitations

    Lean4Agent provides a foundation for verifiable, self-improving LLM-agent systems through dependent-type formal languages.

    Source: §5 · p. 10

    High Claude-Opus costs limited its evaluation to the Layer-2 SWE-Bench experiment, reported in Appendix A.1.

    Source: §3.3.1 · p. 7

Abstract

from arXiv · show

Equipping Large Language Models (LLMs) to execute reliable multi-step workflows has become a central challenge in artificial intelligence. Despite recent advances in LLMs' agentic capabilities, most agent systems still lack formal methods for specifying, verifying, and debugging their workflow and execution trajectories. This challenge mirrors a long-standing problem in mathematics, where the ambiguity of natural languages (NLs) motivates the development of formal languages (FLs). Inspired by this paradigm, we propose **Lean4Agent**, to the best of our knowledge, the first framework that uses Lean4, a dependent-type FL to model and verify agent behavior. **Lean4Agent** launches **FormalAgentLib**, an extensible Lean4 library for formally modeling and verifying agent workflows' semantic consistency under explicit assumptions, and enabling localization of execution-time failures revealed by trajectories. Building on **FormalAgentLib**, we further develop **LeanEvolve**, which applies results in **FormalAgentLib** to revise workflows to enhance its capability. Extensive experiments on a hard problem subset of SWE-Bench-Verified and a subset of ELAIP-Bench across 5 leading LLMs indicate that the verification-passing workflows outperform the failing ones by an average of **11.94%**, and **LeanEvolve** further improves SWE performance by **7.47%** on average. Furthermore, **Lean4Agent** establishes a foundation for a new field of using expressive dependent-type FL to formally model and verify agent behavior.

1 Introduction

Lean4Agent uses Lean4 to model and verify agent workflows and execution trajectories, then uses verification feedback to refine workflows. Across two benchmark subsets and five LLMs, verified workflows outperform those that fail verification, and LeanEvolve further improves SWE performance.

Introduction

  • Existing approaches are fragmented and constrained in expressiveness, leaving workflow specifications and execution trajectories without a unified verification framework.The need is heightened as LLM-agent workflows are increasingly deployed in high-stakes domains.Source: §1 · pp. 1–2
  • FormalAgentLib checks workflow structure, dependent-type pre/postcondition semantics under LLMExec assumptions, and runtime trajectories to localize failing steps.Its semantic layer supports branching, looping, and submodule composition; the trajectory layer uses an LLM to inspect step-level pre- and postconditions.Source: §1 · p. 2, Figure 1 · p. 2
  • LeanEvolve uses FormalAgentLib verification results and optional environment feedback to identify workflow flaws and revise specifications.The revisions aim to improve workflow performance.Source: §1 · p. 3
  • Verified workflows improve performance by 14.80% on the SWE task and 9.07% on the ELAIP-Bench subset; LeanEvolve adds 7.47% on the SWE task.Experiments use a hard-problem subset of SWE-Bench-Verified and a subset of ELAIP-Bench across five leading LLMs.Source: §1 · p. 3

2 Methodology

Lean4Agent formalizes agent workflows and execution trajectories in Lean4, then uses verification guidance to support workflow improvement. FormalAgentLib verifies workflow structure and semantics and analyzes execution trajectories; LeanEvolve uses those diagnostics to revise workflows.

2.1 Preliminaries

  • An agent workflow is a heterogeneous graph of execution nodes and transitions, while an execution trajectory is the valued path of states, nodes, and reasoning or tool-call traces produced when the agent runs.The implementation uses AgentSPEX’s YAML workflow format, though the graph formulation can adapt to general workflow specifications.Source: §2.1 · p. 3

2.2 FormalAgentLib

  • FormalAgentLib is an extensible Lean4 library for modeling and verifying agent workflows and trajectories, organized into structural, semantic, and trajectory-analysis layers.The paper describes it as the first effort, to the authors’ knowledge, to use an expressive dependent-type formal language to verify agent behavior.Source: §2.2 · pp. 3–4

2.2.1 Layer 1: Structural Verification

  • The structural layer verifies workflow well-formedness, including node reachability, edge validity, and read/write consistency, such as reads lacking an initial parameter or reachable producer.It defines types for variables, execution nodes, and graph transitions, providing LLM-independent structural checks analogous to compiler-level verification.Source: §2.2.1 · p. 4

2.2.2 Layer 2: Static Semantic Verification for Agent Workflow

  • FormalAgentLib checks static semantic soundness by verifying step preconditions against predicates propagated through the workflow under an explicit LLM-execution assumption.Its Hoare-style contracts include loop and conditional nodes; verification identifies unmet requirements and violating steps, while a failure indicates the specification is not self-contained under the stated assumptions, not that success is impossible. Graph-level information-flow and context predicates can expose context-management inconsistencies.Source: §2.2.2 · p. 5

2.2.3 Layer 3: Execution Trajectory Verification

  • FormalAgentLib checks whether the LLM-execution assumption holds on particular trajectories and uses step postconditions to localize failure-inducing steps for runtime self-checking and workflow evolution.Lean propositions, external Python validators, and LLM-as-judge modules check different predicates; judges can use environment feedback such as SWE test-case errors.Source: §2.2.3 · pp. 5–6

2.3 LeanEvolve

  • LeanEvolve revises workflows that pass Layer-2 verification but produce incorrect or uncertain results on an execution, aiming to avoid the localized failure on future runs.Formal-guided evolution uses trajectory analysis and optional environment feedback to identify likely failure steps and violated predicates; a pure-LLM stepwise rewrite is an optional add-on for tasks allowing multiple attempts, and the refined workflow is rerun on the same problem.Source: §2.3 · p. 6

3 Experiment

The experiments evaluate FormalAgentLib’s workflow verification and LeanEvolve’s refinement across software-engineering and AI-paper-understanding tasks. Results indicate benefits from verification and formal-guided evolution, with ablations and case studies examining their mechanisms and failure detection.

3.1.1 Task and Benchmark

  • The evaluation used 50 hard SWE-Bench-Verified problems and 100 randomly selected ELAIP-Bench questions, representing LLM-intensive and workflow-intensive tasks.SWE-Bench-Verified supplies unit-test feedback, while ELAIP-Bench [Dai et al., 2025] contains multiple-choice questions from AI papers.Source: §3.1.1 · p. 6

3.1.2 Experiment Methods

  • The study compared randomly selected verification-passing and failing workflows, tested trajectory refinement, and ran Lean v4.20.0 experiments across five leading LLMs.Researchers generated 40 workflows with Claude-Opus-4.6, evaluated three passing and three failing workflows, and compared formal-guided with pure-LLM evolution on 20 initially failing ELAIP trajectories; Claude-Opus was evaluated only on Layer-2 SWE. AgentSPEX ran at temperature 1.0 with context length 163,840.Source: §3.1.2 · pp. 6–7, §3.2 · p. 7, §3.3.1 · p. 7

3.3.1 FormalAgentLib Verification Results

  • 14.80% average gain on SWE-Bench-Verified and 9.07% on ELAIP-Bench marked the performance advantage of Layer-2 verification-passing workflows over failing ones.The reported 95% bootstrap confidence intervals were [10.00%, 19.60%] for SWE and [5.66%, 13.07%] for ELAIP; the improvements were statistically significant.Source: Table 1 · p. 7, §3.3.1 · p. 7

3.3.2 LeanEvolve Enhancement Results

  • 7.47% more solved instances on average raised SWE-Bench hard-subset accuracy from 56.93% to 64.40%; formal-guided evolution solved 7.00% more initially failed cases than pure-LLM evolution.Formal-guided refinement helped with edge cases and cross-file changes, while pure-LLM evolution supported broader exploration.Source: Table 2 · p. 7, Table 3 · p. 7, §3.3.2 · p. 8

3.4.1 Ablation of Graph-level predicates

  • On ELAIP-Bench, removing graph-level predicates reduced failing workflows from 21 of 40 to 8, exposing defects caught only by workflow-level constraints.Frequent violations involved makeUnifiedJudgement and unifiedLoopBack, which capture consistency requirements that local predicates cannot model.Source: §3.4.1 · p. 8

3.4.2 Ablation of Pure-LLM evolve

  • 5.07% average improvement remained after removing LeanEvolve’s pure-LLM add-on, 2.40% less than the full system’s gain.The ablation suggests formal-guided evolution is the primary performance driver, while the add-on contributes broader exploratory revisions.Source: Table 4 · p. 8, §3.4.2 · p. 8

3.5.1 Workflow Errors identified by FormalAgentLib

  • FormalAgentLib detected context-management errors in SWE and ELAIP workflows, including unavailable implementation evidence and answer-choice evaluations influenced by earlier choices.The latter violated evaluateChoicesIndependent, which requires independent or uniform evaluation of choices.Source: §3.5.1 · pp. 8–9

3.5.2 Workflow evolve study

  • In a django_15098 case, Layer-3 verification localized an incorrect fix to verify_fix, and LeanEvolve revised the instruction so the next fix passed.The revised step required tracing the full error chain and validating the fix against relevant tests rather than stopping at the first apparent cause.Source: §3.5.2 · p. 9

4 Related Work

Prior work provides structural workflow checks or tool-specific verification, but does not unify formal modeling of agent workflows and trajectories. Related formal-reasoning efforts largely target domains with precise specifications, unlike agent behavior.

4.1 Verification for agentic system

4.2 LLMs for Formal Theorem Proving

5 Conclusion · A Additional Experiment Results

Lean4Agent uses dependent-type formal language to model and verify LLM-agent workflows and execution trajectories, and LeanEvolve uses verification to refine workflows. Experiments report that verification-passing workflows outperform failing ones and that LeanEvolve further improves SWE performance; the appendix introduces additional results omitted from the main paper.

5 Conclusion

  • Lean4Agent is presented, to the authors’ best knowledge, as the first comprehensive dependent-type framework for uniformly modeling and verifying LLM-agent workflows and execution trajectories.FormalAgentLib models workflow semantic consistency under explicit assumptions and helps localize execution-time failures revealed by trajectories.Source: §5 · p. 9
  • 11.94% average improvement separates verification-passing from failing workflows, while LeanEvolve yields a further 7.47% average improvement on SWE.The experiments cover SWE and paper-understanding tasks across five leading models.Source: §5 · p. 10
  • LeanEvolve refines agent workflows using FormalAgentLib verification and optional environment feedback to improve task performance.Its reported further average improvement is 7.47% on SWE.Source: §5 · pp. 9–10
  • Lean4Agent is proposed as a foundation for verifiable, self-improving LLM-agent systems using dependent-type formal languages.Source: §5 · p. 10

A Additional Experiment Results

A.1 Additional results on Claude

On Claude 4.5 Opus, workflows that pass verification outperform those that fail on the 50-hard-problem subset of SWE-Bench-Verified.

A.1 Additional results on Claude

  • On SWE-Bench-Verified’s 50-hard-problem subset, verification-passing Claude 4.5 Opus workflows averaged 67.33% accuracy versus 56.67% for failing workflows, a 10.67% absolute improvement.This result provides additional evidence that workflows selected by verification transfer across models.Source: §A.1 · p. 14
  • Claude 4.5 Opus was evaluated only on the 50-hard-problem subset because of the high evaluation cost of Claude models.Source: §A.1 · p. 14

A.2 Main results with 95% CI

Verification-passing workflows significantly outperform verification-failing ones in nearly all model-task pairs, with one ELAIP-Bench exception.

A.2 Main results with 95% CI

  • Across both benchmarks, verification-passing workflows significantly outperform failing ones in nearly all model-task pairs; only Qwen-3.5-27B on ELAIP-Bench has a 95% CI including zero.The 95% paired bootstrap confidence intervals use 10,000 resamples; the authors suggest the gain may be less pronounced because this model already has comparatively strong baseline performance on that task.Source: §A.2 · p. 14

A.3 LLM-as-judge workflow quality analysis · A.4 Layer-2 guided workflow refinement · B Details of FormalAgentLib implementation

The sections show Layer-2 verification’s practical value for evaluating and repairing workflows, then describe FormalAgentLib’s types and semantic structures for modeling them. The implementation also makes explicit the assumptions used for semantic reasoning.

A.3 LLM-as-judge workflow quality analysis

  • Layer-2 verification largely agrees with LLM-as-judge on paper-understanding workflows, but judge assessments align weakly with Lean verification and empirical performance on ambiguous, execution-dependent SWE tasks.The comparison used GPT-5.5 prompted with workflow descriptions and semantic requirements similar to those used for Lean verification.Source: §A.3 · p. 14

A.4 Layer-2 guided workflow refinement

  • 10% absolute accuracy gain, from 52% to 62%, followed replacing context-isolated task nodes with context-aware step nodes after verification identified a context-continuity gap.The refined workflow passed Layer-2 verification and was reevaluated with GPT-5.2 on the 50-problem hard subset of SWE-Bench-Verified.Source: §A.4 · p. 15

B Details of FormalAgentLib implementation

B.1.1 BaseType Full Definition; B.1.2 StepType Full Definition

  • BaseType covers primitive, collection, record, optional, and unknown values; StepType distinguishes pure YAML control operations from LLM actions with structured or unstructured outputs.The BaseType definition adds DecidableEq to facilitate proofs.Source: §B.1.1 · p. 15, §B.1.2 · p. 16

B.1.3 WorkflowNode Full Definition

  • WorkflowNode records an identifier, optional name, step type, typed context reads and writes, and an optional LLM instruction whose variable references are extracted into reads.Source: §B.1.3 · p. 16

B.1.4 WorkflowEdge Full Definition; B.1.5 WorkflowGraph Full Definition

  • Workflow edges encode sequencing, branches, loops, and parallel forks and joins, while WorkflowGraph collects nodes, edges, entry and exit identifiers, and parameters.Source: §B.1.4 · pp. 16–17, §B.1.5 · p. 17

B.2.1 PredicateType Full Definition

  • PredicateType includes environment, value-validity, tool and module, task-completion, custom, and extensible checks, plus conjunction and disjunction.Source: §B.2.1 · pp. 18–19

B.2.2 SemanticWorkflowNode Full Definition; B.2.3 SemanticWorkflowGraph Full Definition; B.2.4 Definition of LLM execution axiom

  • SemanticWorkflowNode annotates a base node with decidable variable preconditions and postconditions, while SemanticWorkflowGraph adds parameter, loop, and conditional specifications; llmExecAxiom assumes instructions are executed as specified when preconditions hold.Source: §B.2.2 · p. 19, §B.2.3 · p. 19, §B.2.4 · p. 19

B.1.6 Error case that layer 1 can identify. · B.2.5 Error case external predicates can locate · C Examples for Case Study

The examples show how layer-1 verification detects a scoping error caused by missing output gathering, while external-variable predicates identify a schema mismatch that makes Lean semantic verification fail.

B.1.6 Error case that layer 1 can identify.

  • The layer-1 example runs four LLM branches in parallel to produce multiple intermediate results.Source: §B.1.6 · p. 17
  • Without a gather step, branch-local outputs do not reach the outer scope, so downstream nodes cannot read them and a read-consistency error results.Source: §B.1.6 · p. 17

B.2.5 Error case external predicates can locate

  • An external-variable predicate finds that compose_answer requires evidence_pack fields the preceding step never produced, leaving its schema predicate unsatisfied and Lean verification failing.The consumer expects fields such as passages and summary, but the producer emits a different JSON structure.Source: §B.2.5 · p. 20
  • Before finding evidence, the example parses the paper for its title and sections, then extracts 3–7 search keywords from the question.Source: §B.2.5 · p. 21
  • The producer step find_evidence locates verbatim passages and returns text and source fields in its JSON output.Source: §B.2.5 · p. 21
  • The compose_answer instruction instead accesses each passage's quote and page fields and expects an evidence_pack summary.Source: §B.2.5 · p. 21

C.1 Workflow Errors identified by FormalAgentLib … D.1 Original YAML workflow

The supplied appendix excerpts present SWE and ELAIP workflows and related execution behavior, including staged analysis and verification, evidence selection, workflow evolution, patch submission, and task-completion signaling. They include failed plans but do not explain the verification failures.

C.1.1 Failed verification in SWE task

  • The SWE plan first explores the repository and reproduces the reported issue with a script, whose output informs root-cause analysis.It directs the agent to identify relevant source files before creating and running a reproduction script.Source: §C.1.1 · p. 23
  • After reproduction, the SWE plan calls for a minimal, targeted source-code fix, followed by rerunning the reproduction and testing edge cases or available regression tests.If verification fails, the agent is instructed to analyze the problem, adjust the fix, and retest.Source: §C.1.1 · p. 24
  • The SWE workflow ends by creating and checking a patch containing the intended source changes, then submitting it after verification.The plan separates patch creation, inspection, and submission into ordered steps.Source: §C.1.1 · pp. 24–25

C.1.2 Failed verification in ELAIP-Bench

  • For ELAIP-Bench, the plan begins by producing a paper overview and listing the paper’s main section headings.These outputs precede its question-focused evidence search.Source: §C.1.2 · p. 25
  • The ELAIP plan extracts question keywords and negation cues, then classifies whether the question expects one answer or multiple answers.The classification step returns either “Single-answer” or “Multiple-answer.”Source: §C.1.2 · pp. 25–26
  • The ELAIP plan searches for paragraphs matching the question keywords, filters for direct relevance, and keeps at most five verbatim evidence snippets.The supplied passages end at the heading for evidence-quality verification, without specifying its checks.Source: §C.1.2 · p. 26
  • The ELAIP workflow checks whether evidence can distinguish the answer options, then judges each option independently as supported, contradicted, or not established.Source: §C.1.2 · pp. 26–27
  • For multi-answer questions, the workflow counts supported options and, if fewer than two are supported, revisits borderline judgments under a more lenient standard for up to three rechecks.Source: §C.1.2 · p. 27

C.2 Workflow evolve study example

D Examples of Lean Verification System

D.1 Original YAML workflow

  • The original SWE YAML workflow moves through repository exploration, issue reproduction, source-code repair, fix verification, and patch submission.Source: §D.1 · pp. 31–32
  • The verify_fix step reruns the reproduction, runs any available regression test, checks edge cases, and directs refinement if a check fails.Source: §D.1 · p. 32
  • Patch submission requires verifying that the patch contains only intended source changes and excluding tests, reproduction files, helper tools, setup files, and binaries.Source: §D.1 · pp. 32–33
  • A response with no tool call signals that the task is complete, after which the system prevents further tool calls.Source: §D.1 · p. 33

D.2 Layer-1 and 2 Lean file and its running results

The section presents a Lean4 model of a sequential issue-fixing workflow and reports structural verification checks and selected workflow-quality results. Its code also traces semantic state and invokes goal-coverage analysis.

D.2 Layer-1 and 2 Lean file and its running results

  • The modeled workflow sequences repository exploration, issue reproduction, fixing, verification, and patch creation, with semantic nodes specifying evidence-related preconditions and postconditions.The graph connects the five nodes with sequential edges from exploration through patch creation.Source: §D.2 · pp. 33–34
  • Lean proved read resolvability, valid edges, valid entry and exits, exit reachability, and absence of orphan nodes; context continuity and unified loop-back also pass.The section attributes context continuity to the step chain and unified loop-back to implicit-retry annotations on step nodes.Source: §D.2 · pp. 35, 37
  • The Lean code prints a cumulative semantic-state trace and invokes goal-coverage analysis for the workflow’s stated issue-fixing goal.The supplied passages show the trace and formatted report calls but do not provide the report’s full output.Source: §D.2 · pp. 36–37

E Limitations

Lean4Agent has limitations in inspecting black-box behavior, relying on LLM-generated predicate annotations, and quantitatively evaluating some components.

E Limitations

  • Black-box LLM behavior cannot be fully inspected; structuring steps and translating natural-language requirements into predicates leaves some semantic ambiguity outside the formal system.The framework aims to verify the full agent execution cycle, but this abstraction does not eliminate that ambiguity.Source: E Limitations · p. 37
  • LLM-generated predicate annotations may contain mis-specified predicates or annotation errors, even though the resulting Lean checks are formal.The experiments use LLM-generated annotations because workflows are complex and tasks are numerous.Source: E Limitations · p. 37
  • Because modern LLMs often produce few structural mistakes or explicit variable mismatches, some components are difficult to evaluate quantitatively beyond targeted case studies.Source: E Limitations · p. 37

F Experiment Costs · G Broader Impacts

The paper reports the costs and compute setup for experiments on large and small models, and describes both a reliability benefit for LLM agent systems and potential harmful use.

F Experiment Costs

G Broader Impacts

  • The paper presents a more reliable foundation for LLM agent systems as its societal contribution.Source: G Broader Impacts · p. 37
  • The paper notes that its contribution could also be used in reverse to cause harmful effects using LLM systems.Source: G Broader Impacts · p. 37

Related papers

Loading 2606.06523v2…