# Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory

arXiv: https://arxiv.org/abs/2606.06523 · HTML: https://mlsanity.com/paper/2606.06523/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in Software engineering coding agents, one of 16 directions in LLM agents and tool use.
- Builds on 33 of its 53 references that are in the map.
- First posted on arXiv 2 Jun 2026.

## Placed in

- LLM agents and tool use / [Software engineering coding agents](https://mlsanity.com/agents/software-engineering-coding-agents/)

## Builds on (most cited first, 30 of 33)

- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [Judging LLM-as-a-Judge with MT-Bench and Chatbot Arena](https://mlsanity.com/paper/2306.05685/) (2023)
- [Efficient Memory Management for Large Language Model Serving with PagedAttention](https://mlsanity.com/paper/2309.06180/) (2023)
- [SWE-bench: Can Language Models Resolve Real-World GitHub Issues?](https://mlsanity.com/paper/2310.06770/) (2023)
- [GLM-5: from Vibe Coding to Agentic Engineering](https://mlsanity.com/paper/2602.15763/) (2026)
- [Kimi K2.5: Visual Agentic Intelligence](https://mlsanity.com/paper/2602.02276/) (2026)
- [Multi-Agent Collaboration Mechanisms: A Survey of LLMs](https://mlsanity.com/paper/2501.06322/) (2025)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [Live-SWE-agent: Can Software Engineering Agents Self-Evolve on the Fly?](https://mlsanity.com/paper/2511.13646/) (2025)
- [A Self-Improving Coding Agent](https://mlsanity.com/paper/2504.15228/) (2025)
- [TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts](https://mlsanity.com/paper/2407.03203/) (2024)
- [LLM-based Agents Suffer from Hallucinations: A Survey of Taxonomy, Methods, and Directions](https://mlsanity.com/paper/2509.18970/) (2025)
- [VeriGuard: Enhancing LLM Agent Safety via Verified Code Generation](https://mlsanity.com/paper/2510.05156/) (2025)
- [Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience](https://mlsanity.com/paper/2512.17260/) (2025)
- [Towards Verifiably Safe Tool Use for LLM Agents](https://mlsanity.com/paper/2601.08012/) (2026)
- [VERINA: Benchmarking Verifiable Code Generation](https://mlsanity.com/paper/2505.23135/) (2025)
- [MiroThinker-1.7 & H1: Towards Heavy-Duty Research Agents via Verification](https://mlsanity.com/paper/2603.15726/) (2026)
- [MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving](https://mlsanity.com/paper/2503.03205/) (2025)
- [ToolGate: Contract-Grounded and Verified Tool Execution for LLMs](https://mlsanity.com/paper/2601.04688/) (2026)
- [PDL: A Declarative Prompt Programming Language](https://mlsanity.com/paper/2410.19135/) (2024)
- [AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms](https://mlsanity.com/paper/2602.09464/) (2026)
- [Let's Reason Formally: Natural-Formal Hybrid Reasoning Enhances LLM's Math Capability](https://mlsanity.com/paper/2505.23703/) (2025)
- [Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification](https://mlsanity.com/paper/2603.19329/) (2026)
- [Bridging LLM Planning Agents and Formal Methods: A Case Study in Plan Verification](https://mlsanity.com/paper/2510.03469/) (2025)
- [GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving](https://mlsanity.com/paper/2510.11769/) (2025)
- [FANS -- Formal Answer Selection for Natural Language Math Reasoning Using Lean4](https://mlsanity.com/paper/2503.03238/) (2025)
- [Lean4Physics: Comprehensive Reasoning Framework for College-level Physics in Lean4](https://mlsanity.com/paper/2510.26094/) (2025)

## Built on by (most cited first, 1 of 1)

- [BenchShield: Formal Model-Backed Instrumentation for Reward Integrity in LLM-Agent Evaluation Infrastructure](https://mlsanity.com/paper/2609.11028/) (2026)

## Abstract (arXiv)

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.