Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory

Based on the text provided, here is a detailed technical summary of the paper "Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory":

Overview

The paper introduces Lean4Agent, the first framework to utilize Lean4, a dependent-type formal language (FL), to uniformly model, verify, and refine Large Language Model (LLM) agent workflows and execution trajectories. The authors address the critical challenge of ensuring reliability in multi-step agent systems, where natural language ambiguity often leads to hallucinations, logical inconsistencies, and execution failures. By borrowing paradigms from formal theorem proving, Lean4Agent provides mathematically provable guarantees for agent behavior.

Core Contributions

The framework consists of two primary components:

1. FormalAgentLib: An extensible Lean4 library for formally modeling and verifying agent workflows.
2. LeanEvolve: A runtime refinement method that uses verification results to automatically improve workflows.

Methodology: The Three-Layer Verification System

FormalAgentLib operates on three distinct layers of correctness:

Layer 1: Structural Verification

• Goal: Verify the syntactic and structural well-formedness of the workflow, analogous to compiler checks.
• Mechanism: Defines a type system for variables, execution nodes, and graph transitions. It checks for:
  • Node reachability.
  • Edge validity (sequential, branching, looping).
  • Read/Write Consistency: Ensures nodes only read variables that are either initial parameters or produced by reachable predecessor nodes.
• Outcome: Detects structural errors like "unresolved reads" where a step attempts to access data not generated in its scope.

Layer 2: Static Semantic Verification

• Goal: Verify semantic self-consistency under explicit assumptions (specifically, the LLMExec assumption: if an LLM step starts in a state satisfying preconditions, it produces a state satisfying postconditions).
• Mechanism:
  • Predicate System: Translates ambiguous natural language instructions into concrete, decidable predicates (e.g., isValidJson, matchesJsonSchema, nameExists).
  • Hoare-Style Logic: Models each agent step as a pre-condition/post-condition pair.
  • Semantic Workflow Graph: Propagates these contracts through the workflow graph to ensure that the output of one step satisfies the input requirements of the next.
  • Implicit Variables: Tracks information flow and context management to detect errors humans might miss (e.g., context isolation in parallel branches).
• Outcome: Identifies workflows that are semantically self-contained before execution.

Layer 3: Execution Trajectory Verification

• Goal: Validate the LLMExec assumption on actual execution runs and localize failures.
• Mechanism:
  • Uses Lean to evaluate decidable predicates.
  • Uses external tools (e.g., Python validators) for runtime checks (e.g., URL connectivity).
  • Uses LLM-as-a-Judge for non-decidable properties, leveraging environment feedback (e.g., test case errors).
• Outcome: Pinpoints the exact step where a trajectory deviates from the expected post-conditions, enabling targeted debugging.

LeanEvolve: Formal-Guided Refinement

When a workflow passes static verification but fails during execution, LeanEvolve is employed to refine it:

• Formal-Guided Mode: Uses Layer 3 diagnostics to identify the specific violated predicate and the failing step. An LLM is then prompted to revise the workflow specification based on this precise error localization.
• Pure-LLM Mode: A fallback/add-on that performs broader exploration and trial-and-error revisions without formal guidance, useful for tasks where formal feedback is sparse.
• Result: The system iteratively evolves the workflow until it solves the task.

Experimental Results

The authors evaluated Lean4Agent on two challenging benchmarks across five leading LLMs (including GPT-5.2, GLM-5, Kimi-K2.5, etc.):

1. SWE-Bench-Verified (Hard Subset): Real-world software engineering tasks involving code generation and debugging.
2. ELAIP-Bench: AI paper understanding tasks requiring complex reasoning and evidence retrieval.

Key Findings:

• Verification Impact: Workflows that passed Layer 2 verification outperformed those that failed by an average of 11.94% (14.80% on SWE, 9.07% on ELAIP). This demonstrates that formal verification effectively filters out flawed workflows.
• Refinement Impact: Using LeanEvolve, verified workflows achieved an additional average improvement of 7.47% on the SWE task.
• Formal vs. Pure LLM: Formal-guided evolution outperformed pure-LLM evolution by 7.00% on average in fixing initially failed cases, proving that precise error localization is superior to blind trial-and-error.
• Model Sensitivity: Smaller models showed greater sensitivity to workflow quality, gaining more from verification than larger models.

Conclusion

Lean4Agent establishes a new paradigm for verifiable AI. By applying dependent-type formal languages to agent systems, it moves beyond heuristic evaluation to provide mathematically grounded guarantees. The framework not only improves task performance but also offers a foundation for developing self-improving, reliable autonomous agents in high-stakes domains. The authors plan to open-source the code to foster further research in this field.