Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory

arXiv:2606.06523 · cs.AI, cs.LG, cs.LO, cs.SE · Submitted 2026-06-02 · Read on arXiv

Listen

Radio episode about this paper

Transcript

Introduction to the show: ident: AI Radio. Generated commentary on the latest Artificial Intelligence papers.

Tom: We're looking at the paper: "Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory".

Jane: Here's the gist of the paper. Equipping Large Language Models (LLMs) to execute reliable multi-step workflows has become a central challenge in artificial intelligence, necessitating formal methods for specifying, verifying, and debugging agent execution trajectories The gist is that Lean4Agent is the first framework using dependent-type formal language to uniformly model, verify, and refine LLM agent systems.

Tom: How it works Lean4Agent launches FormalAgentLib, an extensible three-layer Lean4 library for formally modeling and verifying agent behaviors across three levels of correctness: structural, semantic, and runtime trajectory Layer 1 verifies the structural well-formedness of the agent workflow through a workflow graph.

Jane: This layer defines data types for variables and execution nodes, enabling verification of "structural well-formedness" analogous to "compiler-level checks for programs".

Tom: It models an agent workflow as a heterogeneous graph G:= ⟨V, E⟩ where each node is represented as vi:= ⟨ri, wi, ti, τi⟩.

Title and authors: Lu: The paper introduces FormalAgentLib, which is an extensible three-layer Lean4 library for modeling and verifying agent behaviors across three levels of correctness: structural, semantic, and runtime trajectory.

Meng: Three layers of correctness sounds complex. Can you break down what each layer actually checks? What’s the first thing it looks at?

Lalam: Layer one verifies the structural well-formedness of the workflow through a workflow graph, defining data types for variables and execution nodes to check for structural errors, like making sure downstream nodes can actually read variables produced in parallel branches <ref:2606.06523#pg1>.

Tom: That makes sense. So Layer two is about what <ref:2606.06523#pg1>? Is it checking if the logic makes sense?

Lu: Layer two develops a predicate-based system to model the static semantic soundness of the workflow under explicit assumptions about local LLM correctness <ref:2606.06523#pg1>. It checks whether each step’s preconditions are entailed by previously established predicates, assuming that if an LLM step is executed correctly, it will produce a context satisfying its postconditions.

Jane: So it’s checking the logic *before* it runs, based on what we assume the AI steps can do? That’s interesting because that gets to the core issue of how we trust these models.

Meng: Okay, so Layer three sounds like where things get tricky—the actual execution <ref:2606.06523#pg2>. What does that layer do in practice? Does it just run tests?

Lalam: Layer three checks whether the LLMExec assumption holds on particular execution trajectories by using modules called "LLM-as-judge" and external Python validators to analyze the state against step-level postconditions, which lets them localize the failure-inducing steps <ref:2606.06523#pg2>.

The paper's summary: Lu: Beyond FormalAgentLib, they propose LeanEvolve, which is a runtime workflow-refinement method driven by trajectory verification and optional environment feedback. It uses the verification results from FormalAgentLib and an LLM together to identify flaws in current workflows and revise the specifications.

Meng: So if it finds a flaw at runtime, what does that mean for deployment? Does it just re-prompt the model, or is there something more systematic?

Lalam: LeanEvolve’s first mode is formal-guided evolve, which uses Layer three’s trajectory analysis to localize the likely failure-inducing step and violated predicates to give an LLM information to revise that specific part of the workflow <ref:2606.06523#pg2>.

Tom: So it doesn't just guess what went wrong; it points to the exact step and tells the AI how to fix that specific part. That sounds much better than a general system re-prompt.

Jane: And there’s also a pure LLM evolve add-on mode, which does a stepwise rewrite without any formal guidance, just to explore other possibilities. So they give you a choice in how you want to refine the workflow?

Lu: The paper shows that these verification-passing workflows outperform failing ones by an average of eleven point nine four percent on SWE and achieve an additional average improvement of seven point four seven percent on the SWE task with LeanEvolve.

Meng: An eleven point nine four percent gain is significant, especially in a field where we’re still figuring out how to make these agents robust at scale. So they have some solid experimental data there, I guess.

The paper's improvements: Tom: So we're wrapping up on Lean4Agent and LeanEvolve. Basically, this work gives us a framework that uses dependent type theory to model and verify agent behaviors, addressing the challenge of specifying and debugging complex agent execution trajectories.

Jane: It sets up a solid foundation for verifiable LLM-agent systems by decomposing behavior into structured steps and translating natural language requirements into checkable predicates.

Lu: It establishes a unified basis for modeling long-horizon black-box systems, which is something we really need as these agents get more complex.

Meng: I'm still thinking about the cost of running this verification system on actual traffic, but conceptually, this is the way forward for making these agents safer in high-stakes domains.

Lalam: The framework provides a promising foundation for verifiable, self-improving LLM-agent systems through dependent type formal languages and it offers principles for modeling long-horizon black-box systems >

Conclusion: Tom: So we’ve gone through how they build this whole three-layer system, from checking the basic structure to verifying what happens when it actually runs on a trajectory. It’s about using dependent type theory to give us formal proof of correctness for these agent workflows.

Jane: Exactly. The naive question is, why do we need this level of formal verification for agents? Because without it, when you have long-horizon tasks where the AI has to make many decisions in a sequence, those errors can get really hard to track down later.

Lu: What I find interesting is how they decompose the problem into these distinct layers of correctness. Layer one handles the structural stuff—making sure the workflow graph actually makes sense, like ensuring nodes can read what other nodes write, which stops you from having a "read-consistency error."

Meng: But on my side, I’m thinking about deployment. If we have a workflow that passes all these formal checks but still fails in production because of something the formal model didn't capture, does it actually help us deploy faster? What about the cost of running this verification layer at scale?

Lalam: The framework is designed to handle black-box LLM executions by breaking them down into structured steps and translating natural language requirements into checkable predicates. I’m pretty sure that decomposition is the key to making it work with these massive models.

Tom: And then you have LeanEvolve, which takes all that analysis and uses it for refinement. It lets the system localize the failure-inducing step by comparing the actual execution trajectory against those formal postconditions.

Jane: That’s where things get practical for a user. Instead of just getting a vague error message from an LLM, you get targeted feedback on exactly which part of your workflow needs revision, and then you can actually fix that specific part.

Lu: The experiments show that these verified workflows are significantly better than the ones that aren't verified. We’re seeing improvements like seventeen point eight percent on the SWE task just by using LeanEvolve to guide the repair process.

Meng: That seventeen point eight percent gain is solid, but I still see a gap between that lab result and what happens when we run this on real-world, noisy traffic where the LLM's behavior isn't perfectly modeled. We need to know how robust these formal checks are against genuine runtime surprises.

Lalam: The system is extensible too, so you can add your own specific predicates using that 'ext' type if you want to model those tricky semantic gaps that the core system might miss. I’m confident in its ability to identify context management errors before they ever roll out.

Jane: So, this isn't just a theoretical exercise anymore; it’s giving developers a concrete tool to build things that are more predictable and reliable, even when working with these complex language models. It moves us toward designing systems that are correct by construction.

Tom: Yep. To wrap up, "Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory" gives us a unified way to model, verify, and refine agent systems using dependent type theory across structural, semantic, and runtime levels.

Lu: It sets a path forward for modeling long-horizon black-box systems with the rigor we need as these agents get bigger.

Meng: Next up on our show, we’re looking at how embedding models are improving probabilistic race prediction. We'll see if that kind of representation learning can give us any useful structure when dealing with complex sequence prediction tasks.

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

University of Illinois Urbana-Champaign

cs.AI, cs.LG, cs.LO, cs.SE

Submitted: 2026-06-02

Updated: 2026-10-20

Comments: Nips 2026 accepted paper

Code: https://github.com/RickySkywalker/Lean4Agent

License: http://creativecommons.org/licenses/by/4.0/

Importance score: 89/100

The gist: Equipping Large Language Models (LLMs) to execute reliable multi-step workflows has become a central challenge in artificial intelligence, necessitating formal methods for specifying, verifying, and

Key concepts

Layer 1: Structural Verification
This layer checks the basic structure of the agent workflow using a graph. It defines data types for variables and execution nodes, ensuring that the workflow graph is well-formed, similar to compiler checks for programs. It models the flow of execution through defined nodes and edges.
Layer 2: Semantic Verification
This layer uses a predicate system to check if the workflow makes sense under assumptions about local LLM correctness. It verifies that each step's preconditions are met by previously established predicates, ensuring static semantic soundness before deployment.
Layer 3: Runtime Trajectory Checking
This layer monitors actual execution paths (trajectories) using 'LLM-as-judge modules' and external validators. It analyzes the state of the execution against step-level postconditions to localize exactly which steps cause failures during runtime.
LeanEvolve
This is a dual-mode refinement approach that uses trajectory analysis to guide workflow improvement. The formal mode suggests specific revisions based on diagnostics, while a pure LLM mode allows for broader exploration of task outcomes.

Terminology

Summary

Equipping Large Language Models (LLMs) to execute reliable multi-step workflows has become a central challenge in artificial intelligence, necessitating formal methods for specifying, verifying, and debugging agent execution trajectories The gist is that Lean4Agent is the first framework using dependent-type formal language to uniformly model, verify, and refine LLM agent systems.

How it works

Lean4Agent launches FormalAgentLib, an extensible three-layer Lean4 library for formally modeling and verifying agent behaviors across three levels of correctness: structural, semantic, and runtime trajectory Layer 1 verifies the structural well-formedness of the agent workflow through a workflow graph. This layer defines data types for variables and execution nodes, enabling verification of structural well-formedness analogous to compiler-level checks for programs. It models an agent workflow as a heterogeneous graph G:= ⟨V, E⟩ where each node is represented as vi:= ⟨ri, wi, ti, τi⟩.

How it works

Layer 2 develops a predicate-based system to model the static semantic soundness of the agent workflow under explicit assumptions about local LLM’s correctness. This involves a Predicate System that models properties of explicit and implicit variables, and a Semantic Workflow Graph that organizes these predicates across the workflow. The system verifies whether each step’s preconditions are entailed by previously established predicates under the assumption that if an LLM step is executed in a predicate context satisfying its preconditions, then the execution can produce a context satisfying its postconditions.

How it works

Layer 3 checks whether the LLMExec assumption holds on particular trajectories. This layer uses LLM-as-judge modules as complementary runtime checkers for variables with NL definitions, and external Python validators for predicates outside Lean’s decidable core. By analyzing trajectory states against step-level postconditions, Layer 3 localizes the failure-inducing steps, enabling runtime self-checking and formal-guided workflow evolution.

How it works

LeanEvolve is a dual-mode approach for refining agent workflows using execution trajectories, task outcomes, and verification diagnostics. The first mode is formal-guided evolve, which uses Layer 3’s trajectory analysis to localize the likely failure-inducing step and the violated predicates, providing an LLM with that information to revise the corresponding part of the workflow. A pure-LLM evolve add-on mode performs a stepwise rewrite without formal guidance, complementing formal-guided evolution by allowing broader exploration.

How it works

Extensive experiments on SWE and paper understanding tasks across five leading LLMs indicate that verification-passing workflows outperform failing ones by an average of 11.94%. With LeanEvolve, verified workflows achieve an additional average improvement of 7.47% on the SWE task. This demonstrates the usefulness of workflow verification and refinement methods.

How it works

FormalAgentLib's semantic verification detects non-trivial context management errors before the workflow’s roll-out, such as a violation of evaluateChoicesIndependent predicate in ELAIP-Bench results. The system also identifies structural errors, like a read-consistency error, where downstream nodes cannot read variables produced inside parallel branches due to a lack of a gather step.

How it works

The framework leverages dependent type theory to formally model agent behaviors, addressing the challenge that existing approaches are constrained by the expressiveness of their underlying formal language This establishes a foundation for using expressive dependent-type FL to uniformly model, verify, and refine agent systems.

How it works

The framework provides a solid and unified basis for verifiable LLM-agent systems and opens the door to future directions in training and developing self-improving LLM agents. It also offers principles for modeling long-horizon black-box systems.

How it works

The framework is extensible, allowing user-defined predicates through the ext type, and enables localization of execution-time failures revealed by trajectories. This structure supports correct-by-construction workflow design.

How it works

The framework's implementation uses Lean v4.20.0, containing 151 types and 611 functions to formally model the workflow, with the core of FormalAgentLib being almost entirely written by humans and verified to ensure correctness. The system includes theorems that help prove properties of agent workflows.

How it works

The framework is designed for use in high-stakes domains where complex LLM-agent workflows are increasingly deployed, necessitating formal speculation about both workflow specification and execution trajectory levels However, the application of FL to uniformly model and verify LLM agent systems remains largely understudied.

How it works

The framework provides a promising foundation for verifiable, self-improving LLM-agent systems through dependent type formal languages. It is intended to support further development of the field.

How it works

The experiment costs for large models are around 4,000 dollars, while small models cost around 1,500 GPU hours for running on specialized hardware. The paper contributes to society by providing a more reliable foundation for the LLM agent systems.

How it works

The framework decomposes agent behavior into structured steps and abstracts natural-language requirements into checkable predicates, thereby leaving some semantic ambiguity outside the formal system. This decomposition is key to its success in modeling black-box LLM executions.

How it works

The framework's structure includes a Layer 2 Predicate System that models pre- and post-conditions of agent executions, which is verified under the LLMExec assumption. This allows for automated proof of static semantic soundness while being extensible to new domains.

How it works

LeanEvolve's formal-guided evolution shows that predicate-based diagnostics can provide more fine-grained modification than pure-LLM revisions, as formal guidance is the primary driver of LeanEvolve’s performance. This suggests that predicate-based diagnostics can pinpoint workflow flaws and guide targeted repairs.

How it works

The framework's application in SWE and paper understanding tasks shows that verification-passing workflows achieve significant improvements, such as an average gain of 14.80% on the SWE task. The results show that "passing-verification workflows outperform failing ones by 14.80% on average with a 95% bootstrap CI of [10.00%, 19.60%].

How it works

The framework's design includes specific types for modeling control flow, such as seqEdge, branchEdge, and loopEdge in the WorkflowEdge definition. This allows for the formal modeling of sequential execution, branching, and looping behaviors within the workflow structure.

How it works

The framework's Semantic Workflow Graph organizes semantic nodes as Hoare-style pre- and post-condition pairs, which are organized into a graph S = ⟨G, spara, S, L, C⟩. This structure allows submodules to be integrated by treating their postconditions in spara as input contracts and return nodes’ preconditions as output contracts.

How it works

The framework's trajectory verification layer uses LLM-as-judge modules and analyzes trajectory states against step-level postconditions to localize failures. This enables runtime self-checking and formal-guided workflow evolution.

How it works

The framework's structural verification layer detects errors like a read inconsistency error when a node reads a variable that is neither an initial parameter nor produced by a reachable predecessor. This provides checks analogous to simple compiler-level verifications for programs.

How it works

The framework's goal specification defines required predicate coverage for each sub-goal, such as requiring GraphLevelPredicateKeys.pathCoverage and GraphLevelPredicateKeys.contextContinuity. This ensures that workflows are designed to meet specific formal requirements.

How it works

The framework's error localization capability is demonstrated by identifying a failure where a step expects fields in evidence pack that were never produced by the preceding step, violating the required schema predicate. This shows how external predicates can detect semantic violations in workflow outputs.

How it works

The framework's refinement process involves replacing context-isolated task nodes with context-aware step nodes when Layer 2 verification identifies a lack of context continuity across execution steps. This demonstrates the practical utility of formal modeling and verification in guiding workflow repair.

Improvements for AI systems

  1. Formal verification of agent workflows ensures semantic consistency under explicit assumptions, allowing for correct-by-construction workflow design. This capability prevents execution failures by formally checking that each step’s preconditions are satisfied before execution, which is crucial for complex, long-horizon tasks.

  2. Development of LeanEvolve enables runtime workflow refinement driven by trajectory verification and feedback, allowing the system to revise specifications to enhance performance. This iterative improvement can lead to tangible gains, such as the reported 7.47% average improvement on SWE task performance by revising workflows based on localized failure diagnostics.

  3. Localization of execution time failures is achieved through Layer 3 analysis, which localizes the violated step in the workflow by applying Lean, external programs, and LLM-as-judge to check the execution trajectory. This allows agents to pinpoint exactly the execution step responsible for the failure, enabling targeted repairs instead of broad system re-prompting.

  4. The framework supports modeling complex control flows like branching and looping using a dependent-type predicate system, which uniformly model[s] branching, looping, and submodule composition behaviors. This formal rigor ensures that structural errors, such as read/write consistency violations in parallel scopes, are detected before runtime.

Abstract

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.

Sources

Related papers