Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory

The paper introduces Lean4Agent, a framework utilizing Lean4 for formal modeling and verification of agent behavior, particularly for LLM-driven multi-step workflows. It addresses the absence of formal methods in current agent systems by allowing semantic consistency checks and enabling the localization of execution-time failures.