Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory

Lean4Agent is introduced as a framework utilizing Lean4, a dependent-type formal language, to model and verify the behavior of agents in multi-step workflows, addressing the lack of formal methods in existing agent systems. It includes the **FormalAgentLib**, which allows for the semantic consistency verification of agent workflows, and **LeanEvolve**, which enhances workflow capabilities based on verification results. Experimental results demonstrate that workflows verified through this framework outperform unverified ones by an average of 11.94%, with LeanEvolve improving SWE performance by an additional 7.47%, highlighting its significance for practitioners seeking to enhance reliability in LLM-driven agent systems.