Lean4Agent introduces formal verification for LLM agent workflows using Lean4
Lean4Agent is the first framework that uses the dependent‑type language Lean4 to formally model and verify multi‑step LLM agent workflows and execution trajectories. Experiments on SWE‑Bench‑Verified and ELAIP‑Bench show verification‑passing workflows improve performance by ~12%, and the LeanEvolve component adds another ~7% gain.