Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory
Lean4Agent is a framework using dependent-type formal language to model, verify, and refine LLM agent workflows. It uses three layers—structural, semantic, and runtime trajectory verification—to ensure correctness from design through execution. This allows for 'correct-by-construction' workflow design and automated refinement of agent systems.