Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory

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

arXiv · PDF · Open in the Atlas

Code that ran

We lifted 16 functions out of this paper's own repositories and ran 14 of them in a sandbox. "Ran" means the function executed on a synthesized input and returned a value. It is not a reproduction of the paper's results.

Repositories linked to this paper

• RickySkywalker/Lean4Agent

Some links come from the archived Papers with Code dataset (CC BY-SA 4.0): attribution and licence.

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 executiontime 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 [Jimenez et al., 2024] and a subset of ELAIP-Bench [Dai et al., 2025] 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.

For agents

The same record, over MCP at https://syntology.ai/mcp:

get_harvested_code_for_paper("2606.06523")
get_code_for_paper("2606.06523")
have("2606.06523")

Connect an agent — have() is free.