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

LLM-agent systems lack unified formal methods for specifying, verifying, and debugging workflows and execution trajectories. Lean4Agent introduces FormalAgentLib and LeanEvolve to verify and refine these systems, with verification-passing workflows outperforming failing ones by an average of 11.94% and LeanEvolve adding 7.47% on SWE tasks.

  • Problem

    LLM-agent systems lack unified formal methods for specifying and verifying both workflows and execution trajectories, despite their increasing deployment in high-stakes domains.

  • Method

    Lean4Agent uses dependent-type formal language through FormalAgentLib to verify workflows and trajectories, while LeanEvolve uses verification results and optional environment feedback to refine workflows.

  • Results

    Verification-passing workflows outperform failing ones by an average of 11.94% across SWE and paper-understanding tasks, while LeanEvolve adds a further average improvement of 7.47% on SWE.

  • Takeaways & Limitations

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

  • Takeaways & Limitations

    Full experiments could not be run on Claude-Opus because of its high cost; evaluation was limited to the Layer-2 SWE-Bench experiment.

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 addresses the lack of a unified formal framework for specifying and verifying LLM-agent workflows and execution trajectories. It introduces FormalAgentLib for verification and failure localization, and LeanEvolve for workflow refinement.

  • Existing verification approaches for LLM systems remain fragmented across output evaluation, tool-call contracts, action policies, and artifact checking.
  • Lean4Agent uses dependent-type formal language to uniformly model, verify, and refine agent systems.
  • FormalAgentLib verifies workflow structure, semantic consistency under explicit assumptions, and execution-time failures revealed by trajectories.
  • LeanEvolve uses verification results and an LLM to identify workflow flaws and revise specifications for improved performance.
  • 14.80% average improvement occurs on the hard SWE-Bench-Verified subset and 9.07% on the ELAIP-Bench subset for verified versus failing workflows.With LeanEvolve, verified workflows gain an additional average 7.47% on SWE tasks.
  • Lean4Agent provides a basis for verifiable, self-improving LLM-agent systems and modeling long-horizon black-box systems.

2 Methodology

The methodology represents workflows as typed graphs and verifies them at structural, semantic, and trajectory levels. FormalAgentLib provides predicate-based reasoning and failure localization, while LeanEvolve refines workflows using execution evidence and diagnostics.

  • 2.1 Preliminaries: An agent workflow is represented as a heterogeneous graph of execution nodes and transitions, with nodes specifying read variables, written variables, instructions, and execution types.
  • 2.1 Preliminaries: An execution trajectory is a valued path over the workflow graph containing pre- and post-execution states, executed nodes, and reasoning or tool-call traces.
  • 2.2 FormalAgentLib: FormalAgentLib is organized into structural verification, semantic verification, and trajectory-level analysis layers.
  • 2.2.1 Layer 1: Structural Verification: Layer 1 checks structural properties including node reachability, edge validity, and read/write consistency.
  • 2.2.2 Layer 2: Static Semantic Verification: Layer 2 translates workflow requirements into predicates and propagates Hoare-style preconditions and postconditions across sequential, branching, and looping behaviors.
  • 2.2.2 Layer 2: Static Semantic Verification: Under the LLMExec assumption, Layer 2 verifies local semantic soundness by ensuring each node’s preconditions are satisfied before execution.A failed verification identifies violated requirements but does not imply that the workflow can never produce a correct answer.
  • 2.3 LeanEvolve: LeanEvolve revises workflows that pass Layer-2 verification but produce incorrect or uncertain execution results, using trajectories, task outcomes, and verification diagnostics.

3 Experiment

Lean4Agent is evaluated on SWE-Bench-Verified and ELAIP-Bench using workflow verification, trajectory verification, and workflow refinement across five LLMs. Verification-passing workflows consistently outperform failing workflows, while LeanEvolve further improves performance through formal-guided revisions.

  • Experiment setup: The experiments evaluate FormalAgentLib verification and LeanEvolve refinement on SWE-Bench-Verified and ELAIP-Bench across five leading LLMs.SWE uses a 50-problem hard subset, while the paper-understanding evaluation randomly selects 100 ELAIP-Bench problems.
  • FormalAgentLib verification: The verification experiment compares three randomly selected passing workflows with three failing workflows after linter filtering and Layer-2 semantic verification.Average task-pass rates across the two benchmarks measure the value of semantic verification.
  • LeanEvolve refinement: Formal-guided evolution solves 7.00% more initially failed ELAIP-Bench cases on average than pure-LLM evolution.The comparison uses initially failed trajectories and evaluates whether verification-guided localization improves subsequent workflow revisions.
  • FormalAgentLib verification: Verification-passing workflows outperform failing workflows by 14.80% on SWE-Bench-Verified and 9.07% on ELAIP-Bench.The reported 95% bootstrap confidence intervals are [10.00%, 19.60%] and [5.66%, 13.07%], respectively.
  • FormalAgentLib verification: Passing workflows typically specify variables precisely and use structured retry loops and reasonable context management, whereas failing workflows violate preconditions or disrupt information flow.Paper-understanding failures also include context-aware per-choice evaluation that can affect later choices.
  • LeanEvolve refinement: LeanEvolve raises the hard SWE-Bench subset accuracy from 56.93% to 64.40%, adding 7.47% solved instances on average after refinement.Formal-guided refinement is especially helpful for edge cases and cross-file modifications, while pure-LLM evolution supports broader exploration.
  • Ablation: Removing pure-LLM evolution leaves a 5.07% average SWE-Bench improvement, 2.40% below the full system, indicating formal-guided evolution drives the remaining gains.The pure-LLM add-on contributes exploratory revisions not always captured by formal feedback.
  • Case studies: Case studies show FormalAgentLib detecting context-management errors before rollout and LeanEvolve localizing a failed verification step before guiding a successful repair.The examples cover unavailable execution context, dependent answer-choice evaluation, and a SWE fix that initially passed despite failing tests.

4 Related Work

Existing agent-verification work provides structural validation or targeted checks, but lacks a unified framework for formally modeling and verifying workflows and execution trajectories.

  • Agent workflow languages provide structural validation through typed or graph-based execution organization, but offer limited semantic-correctness guarantees.
  • Tool and artifact verification improves reliability but typically targets specific agent behaviors rather than complete workflows and trajectories.
  • No existing framework is identified as formally modeling and verifying agent workflows and trajectories in a unified manner.
  • Formal-reasoning research has extended from neural theorem proving to broader settings, including natural-language mathematics and related formal-method applications.

5 Conclusion

Lean4Agent unifies dependent-type formal modeling and verification of agent workflows and trajectories through FormalAgentLib, then uses LeanEvolve to refine workflows from verification and environment feedback. Across SWE and paper-understanding tasks, verification-passing workflows outperform failing ones, while LeanEvolve yields an additional SWE improvement.

  • Lean4Agent applies dependent-type formal language to uniformly model and verify LLM-agent workflows and execution trajectories.
  • FormalAgentLib verifies workflow semantic consistency under explicit assumptions and localizes execution-time failures revealed by trajectories.
  • LeanEvolve refines workflows using FormalAgentLib verification and optional environment feedback to improve task performance.
  • 11.94% average improvement separates verification-passing from verification-failing workflows across SWE and paper-understanding tasks and 5 leading models.
  • 7.47% further average improvement is achieved by LeanEvolve on the SWE task.

A.1 Additional results on Claude

On Claude 4.5 Opus, verification-passing workflows achieve higher average accuracy than verification-failing workflows on the 50-hard-problem SWE-Bench-Verified subset.

  • 67.33% average accuracy for verification-passing workflows exceeds 56.67% for verification-failing workflows on Claude 4.5 Opus.
  • 10.67% absolute improvement is observed for verification-passing workflows over verification-failing workflows.
  • Claude 4.5 Opus is evaluated only on the 50-hard-problem subset because of the high evaluation cost of Claude models.

A.2 Main results with 95% CI

Across five evaluated models and both benchmarks, paired bootstrap confidence intervals show that verification-passing workflows significantly outperform failing workflows in nearly all model-task pairs, with one exception.

  • 95% paired bootstrap confidence intervals are computed from 10,000 resamples across both benchmarks and five evaluated models.
  • Verification-passing workflows significantly outperform verification-failing workflows in nearly all model-task pairs.
  • Qwen-3.5-27B on ELAIP-Bench is the only exception because its 95% confidence interval includes zero.
  • The workflow-quality gain is less pronounced in that setting, possibly because the model already has comparatively strong baseline performance.

A.3 LLM-as-judge workflow quality analysis

The paper compares FormalAgentLib’s semantic verification with an LLM-as-judge baseline and illustrates how verification can guide workflow repair. The library represents workflows, variables, predicates, and control flow in Lean4 to detect structural and semantic inconsistencies.

  • FormalAgentLib is compared with an LLM-as-judge baseline for SWE-Bench and ELAIP-Bench workflows.
  • A failed workflow can be repaired by replacing context-isolated task nodes with context-aware step nodes, allowing it to pass Layer-2 verification.
  • The workflow model includes nodes, typed variables, instructions, control-flow edges, entry and exit nodes, and initial parameters.
  • Layer-1 checks expose a read-consistency error when parallel branches produce outputs that are not gathered into the outer scope.

B.2.5 Error case external predicates can locate

External-variable predicates identify semantic mismatches between a workflow’s expected JSON schema and the structure actually produced by an earlier step. In the example, Lean verification localizes the failure to the compose_answer step.

  • The compose_answer step expects passages and summary fields in evidence_pack, but the preceding producer emits a different JSON structure.
  • The unsatisfied matchesJsonSchema predicate causes the workflow to fail Lean-based semantic verification.
  • The verification output reports the missing schema predicate for compose_answer and lists predicates available for related variables.

C.1 Workflow Errors identified by FormalAgentLib

FormalAgentLib identifies workflow errors in a multi-step SWE-Bench plan by checking its structure, execution instructions, and verification requirements. The plan progresses from repository exploration through reproduction, fixing, verification, and patch submission.

  • C.1.1 Failed verification in SWE task: The failed verification plan defines a five-stage workflow: explore the repository, reproduce the issue, implement a fix, verify it, and submit a patch.
  • C.1.1 Failed verification in SWE task: The exploration stage asks the agent to understand the repository and identify relevant source files from the problem statement.
  • C.1.1 Failed verification in SWE task: The reproduction stage requires creating and running a script, then analyzing its output to determine the root cause.
  • C.1.1 Failed verification in SWE task: The implementation stage requires a minimal targeted source-code fix while excluding tests and configuration files from modification.
  • D.1 Original YAML workflow: The verification stage reruns the reproduction script, tests edge cases and available regressions, and iterates if the fix fails.
  • C.1.1 Failed verification in SWE task: The submission stage creates a patch containing only intended source changes, verifies its contents, and does not commit the changes.

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

The Lean file encodes a SWE workflow as structural and semantic graphs, then runs checks for reachability, read resolution, edge validity, predicate requirements, and goal coverage. The displayed results show successful structural checks and context-aware semantic properties for the example plan.

  • The transformed Lean file imports structural, semantic, and graph-level predicate modules to verify the workflow.
  • Semantic nodes attach preconditions and postconditions such as valid tools, issue reproduction, fix implementation, and verification evidence.
  • The workflow graph defines sequential nodes from repository exploration through patch creation, with typed initial parameters and a single exit.
  • The structural diagnostics inspect write consistency, reachability, read resolvability, and the validity of graph edges, entry, exits, and orphan nodes.
  • The example proves read resolution, edge validity, entry validity, exit validity, exit reachability, and absence of orphan nodes with native_decide.
  • The semantic graph tracks predicate state after each node and reports cumulative predicates established during execution.
  • Context continuity passes because the step chain provides conversation history, while unified loop-back passes through implicit retry markings.
  • Goal coverage is computed by analyzing the semantic graph against the workflow’s goal specification.

E Limitations

Lean4Agent has three stated limitations: incomplete inspection of black-box behavior, possible errors in LLM-generated predicate annotations, and difficulty evaluating some components quantitatively.

  • Black-box LLM behavior cannot be fully inspected, so natural-language requirements are abstracted into checkable predicates and some semantic ambiguity remains outside the formal system.
  • LLM-generated predicate annotations may be mis-specified or contain annotation errors, despite the resulting Lean checks being formal.
  • Modern LLMs generate few structural mistakes or explicit variable mismatches, making some components difficult to evaluate quantitatively beyond targeted case studies.

F Experiment Costs

The experiments require substantial computational spending, with large models evaluated through official APIs and small models run on dedicated GPUs; the paper also notes potential harmful reverse use.

  • Large-model experiments cost around $4,000 through official API calls, including evaluations of GPT-5.2, GLM-5, Kimi-K2.5, and Claude.
  • Small-model experiments use 4xGH200 VLLM GPUs and cost around 1,500 GPU hours for Qwen-3.5-27B and Gemma-4-31B.
  • The paper identifies potential harmful effects from using the system in reverse with LLM systems.
Loading 2606.06523v2…