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**，通过应用库中的验证结果修订工作流以增强其能力。在SWE-Bench-Verified困难子集及ELAIP-Bench子集上，针对5个主流大语言模型的大量实验表明，通过验证的工作流平均性能比未通过者高出**11.94%**，而**LeanEvolve**进一步将SWE性能平均提升**7.47%**。此外，**Lean4Agent**为使用具表达力的依赖类型形式语言形式化建模与验证智能体行为这一新领域奠定基础。