This paper introduces <strong>Lean4Agent</strong>, to the best of our knowledge, the first framework that uses Lean4 to model and verify agent behavior. <strong>Lean4Agent</strong> introduces <strong>FormalAgentLib</strong>, 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 <strong>FormalAgentLib</strong>, we further develop <strong>LeanEvolve</strong>, which applies the results in <strong>FormalAgentLib</strong> 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 <strong>11.94%</strong>, and <strong>LeanEvolve</strong> further improves SWE performance by <strong>7.47%</strong> on average. Furthermore, <strong>Lean4Agent</strong> establishes a foundation for a new field of using expressive dependent-type FL to formally model and verify agent behavior.</p>\n","updatedAt":"2026-06-09T04:25:51.693Z","author":{"_id":"6618d1c3c1167c8d8702b19d","avatarUrl":"/avatars/24611ca6c4158f4978ac8476a87d8d9c.svg","fullname":"Ruida WANG","name":"RickyDeSkywalker","type":"user","isPro":false,"isHf":false,"isHfAdmin":false,"isMod":false,"followerCount":1,"isUserFollowing":false}},"numEdits":0,"identifiedLanguage":{"language":"en","probability":0.82977694272995},"editors":["RickyDeSkywalker"],"editorAvatarUrls":["/avatars/24611ca6c4158f4978ac8476a87d8d9c.svg"],"reactions":[],"isReport":false}}],"primaryEmailConfirmed":false,"paper":{"id":"2606.06523","authors":[{"_id":"6a27956c6dde1c5ef75bd0e8","name":"Ruida Wang","hidden":false},{"_id":"6a27956c6dde1c5ef75bd0e9","name":"Jerry Huang","hidden":false},{"_id":"6a27956c6dde1c5ef75bd0ea","name":"Pengcheng Wang","hidden":false},{"_id":"6a27956c6dde1c5ef75bd0eb","name":"Xuanqing Liu","hidden":false},{"_id":"6a27956c6dde1c5ef75bd0ec","name":"Luyang Kong","hidden":false},{"_id":"6a27956c6dde1c5ef75bd0ed","name":"Tong Zhang","hidden":false}],"publishedAt":"2026-06-02T00:00:00.000Z","submittedOnDailyAt":"2026-06-09T00:00:00.000Z","title":"Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory","submittedOnDailyBy":{"_id":"6618d1c3c1167c8d8702b19d","avatarUrl":"/avatars/24611ca6c4158f4978ac8476a87d8d9c.svg","isPro":false,"fullname":"Ruida WANG","user":"RickyDeSkywalker","type":"user","name":"RickyDeSkywalker"},"summary":"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.","upvotes":1,"discussionId":"6a27956d6dde1c5ef75bd0ee","githubRepo":"https://github.com/RickySkywalker/Lean4Agent","githubRepoAddedBy":"user","ai_summary":"Large language models can be equipped with formal verification frameworks using dependent-type languages to improve multi-step workflow reliability and performance.","ai_keywords":["Large Language Models","agent systems","formal methods","formal languages","dependent-type languages","Lean4","FormalAgentLib","LeanEvolve","SWE-Bench-Verified","ELAIP-Bench"],"ai_summary_model":"Qwen/Qwen2.5-Coder-32B-Instruct","githubStars":1,"organization":{"_id":"68ef00955bff0d62c986e4f9","name":"UIUC-ScaleML","fullname":"UIUC ScaleML Lab","avatar":"https://cdn-avatars.huggingface.co/v1/production/uploads/64cb1ad1667f4f80852f6050/ZUSgn9xQjfqDOHiI_-7Tw.png"}},"canReadDatabase":false,"canManagePapers":false,"canSubmit":false,"hasHfLevelAccess":false,"upvoted":false,"upvoters":[{"_id":"6618d1c3c1167c8d8702b19d","avatarUrl":"/avatars/24611ca6c4158f4978ac8476a87d8d9c.svg","isPro":false,"fullname":"Ruida WANG","user":"RickyDeSkywalker","type":"user"}],"acceptLanguages":["en"],"dailyPaperRank":0,"organization":{"_id":"68ef00955bff0d62c986e4f9","name":"UIUC-ScaleML","fullname":"UIUC ScaleML Lab","avatar":"https://cdn-avatars.huggingface.co/v1/production/uploads/64cb1ad1667f4f80852f6050/ZUSgn9xQjfqDOHiI_-7Tw.png"},"markdownContentUrl":"https://huggingface.co/buckets/huggingchat/papers-content/resolve/2606/2606.06523.md"}">

Get this paper in your agent:

Don't have the latest CLI?

Cite arxiv.org/abs/2606.06523 in a model README.md to link it from this page.

Cite arxiv.org/abs/2606.06523 in a dataset README.md to link it from this page.

Cite arxiv.org/abs/2606.06523 in a Space README.md to link it from this page.

Add this paper to a collection to link it from this page.