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 execution-time 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 and a subset of ELAIP-Bench 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.

翻译：赋予大语言模型执行可靠多步工作流的能力已成为人工智能领域的核心挑战。尽管近年来大语言模型的智能体能力取得进展，但大多数智能体系统仍缺乏用于规范、验证和调试其工作流与执行轨迹的形式化方法。这一挑战与数学中长期存在的问题相呼应——自然语言的歧义性推动了形式化语言的发展。受此范式启发，我们提出**Lean4Agent**（据我们所知，首个使用依赖类型形式化语言Lean4建模与验证智能体行为的框架）。**Lean4Agent**创建了**FormalAgentLib**——一个可扩展的Lean4库，用于在显式假设下形式化建模与验证智能体工作流的语义一致性，并实现对轨迹中执行时错误的精准定位。基于**FormalAgentLib**，我们进一步开发**LeanEvolve**，其应用**FormalAgentLib**的验证结果对工作流进行修订以增强能力。在SWE-Bench-Verified的困难子集及ELAIP-Bench子集上，针对5个前沿大语言模型的广泛实验表明：通过验证的工作流性能平均优于未通过验证的工作流**11.94%**，而**LeanEvolve**进一步将软件工程任务性能平均提升**7.47%**。此外，**Lean4Agent**为利用表达型依赖类型形式化语言建模与验证智能体行为这一新领域奠定了基础。