Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory

# Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory
Source: [https://arxiv.org/html/2606.06523](https://arxiv.org/html/2606.06523)
\\minted@def@optcl

envname\-P envname\#1 amlblock\]YAMLbreaklines, fontsize= amlblockred\]YAMLbreaklines, fontsize=, bgcolor=diffredamlblockgreen\]YAMLbreaklines, fontsize=, bgcolor=diffgreen

Ruida Wang1,Jerry Huang1,Pengcheng Wang1,Xuanqing Liu2,Luyang Kong2Tong Zhang1 1University of Illinois Urbana\-Champaign,2Independent researcher \{ruidaw,jerry8,pw29\}@illinois\.edu xuanqingliu@outlook\.com, luyangkong@gmail\.com tozhang@illinois\.edu

###### Abstract

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 proposeLean4Agent, to the best of our knowledge, the first framework that uses Lean4, a dependent\-type FL to model and verify agent behavior\.Lean4AgentlaunchesFormalAgentLib, 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 onFormalAgentLib, we further developLeanEvolve, which applies results inFormalAgentLibto revise workflows to enhance its capability\. Extensive experiments on a hard problem subset of SWE\-Bench\-Verified\(Jimenez et al\.,[2024](https://arxiv.org/html/2606.06523#bib.bib11)\)and a subset of ELAIP\-Bench\(Dai et al\.,[2025](https://arxiv.org/html/2606.06523#bib.bib6)\)across 5 leading LLMs indicate that the verification\-passing workflows outperform the failing ones by an average of11\.94%, andLeanEvolvefurther improves SWE performance by7\.47%on average\. Furthermore,Lean4Agentestablishes a foundation for a new field of using expressive dependent\-type FL to formally model and verify agent behavior\.

## 1Introduction

Developing Artificial Intelligence \(AI\) systems with mathematically provable properties has long been a central aspiration of the computer science community\(Seshia et al\.,[2022](https://arxiv.org/html/2606.06523#bib.bib30)\)\. With the rapid development of LLMs’ agentic capabilities, complex LLM\-agent workflows are increasingly being deployed in high\-stakes domains\(Tran et al\.,[2025](https://arxiv.org/html/2606.06523#bib.bib34)\)\. This trend heightens the need for formal speculations about LLM agent systems in both workflow specification and execution trajectory levels\.

Existing approaches to verifying LLM\-based systems remain fragmented in scope and formats\. Early approaches, such as LLM\-as\-judge\(Zheng et al\.,[2023](https://arxiv.org/html/2606.06523#bib.bib49)\), evaluate models’ NL outputs but remain vulnerable to hallucination and overconfidence, especially in long\-horizon executions\(Lin et al\.,[2025a](https://arxiv.org/html/2606.06523#bib.bib16)\)\. Recent work has introduced formal methods, including simple Hoare\-style logic contracts for verifying tool calls\(Liu et al\.,[2026](https://arxiv.org/html/2606.06523#bib.bib19)\), SMT\-backed verification of action\-level policies\(Miculicich et al\.,[2025](https://arxiv.org/html/2606.06523#bib.bib21)\), and temporal\-logic checking of its artifacts\(Ramani et al\.,[2025](https://arxiv.org/html/2606.06523#bib.bib27)\)\. However, each line of work only addresses part of the problem and is constrained by the expressiveness of its underlying formal language\. The temporal logic language is unable to model data\-dependent properties, and SMT\-based contract checks struggle to express higher\-order reasoning\. Thus, to the best of our knowledge, existing work does not yet provide a unified framework for formally modeling and verifying agent workflows and trajectories\. Both are important for long\-horizon autonomous agents\(Wang et al\.,[2026](https://arxiv.org/html/2606.06523#bib.bib36)\)\.

![Refer to caption](https://arxiv.org/html/2606.06523v1/x1.png)Figure 1:Lean4Agent Framework:TheLean4Agentframework consists of two main components\. \(a\)FormalAgentLibis a three\-layer Lean4 library for formally modeling and verifying agent behaviors\. Layer 1 verifies the structural correctness of the workflow through a workflow graph\. Layer 2 develops a predicate \(pred\.\) system to model pre\- and post\-conditions of agent executions and verify the semantic self\-consistency usingLLMExecassumptions\. Layer 3 localizes the violated step in the workflow by applying Lean, external programs, and LLM\-as\-judge to check the execution trajectory\. \(b\)LeanEvolveuses verification results to refine workflows, and it builds formal\-guided workflow evolution with the pure\-LLM evolve add\-on to further enhance its capabilities\.A parallel challenge has long existed in modern pure mathematics, where most problems involve proving theorems without numerical answers\. Because NL is inherently ambiguous, validating complex mathematical arguments becomes increasingly difficult as proofs grow in length and sophistication\. To address this issue, mathematicians and computer scientists have adopted dependent type theory\(Martin\-Löf and Sambin,[1984](https://arxiv.org/html/2606.06523#bib.bib20)\)to formally verify proofs\. This paradigm has led to expressive formal languages \(FLs\) such as Lean\(De Moura et al\.,[2015](https://arxiv.org/html/2606.06523#bib.bib7); Moura and Ullrich,[2021](https://arxiv.org/html/2606.06523#bib.bib22)\)and Coq\(Coq,[1996](https://arxiv.org/html/2606.06523#bib.bib5)\), as well as LLM tools for them\. Despite their success in mathematics, the application of FL to uniformly model and verify the LLM agent systems remains largely understudied\.

To address these challenges, we proposeLean4Agent, to the best of our knowledge, the first framework that uses dependent\-type FL to uniformly model, verify, and refine agent systems\. The overview ofLean4Agentcan be found in Figure[1](https://arxiv.org/html/2606.06523#S1.F1)\.Lean4AgentlaunchesFormalAgentLib, an extensible three\-layer Lean4 library for formally modeling and verifying agent workflows and trajectories across three levels of correctness: structural, semantic, and runtime trajectory\. Layer 1 verifies the structural well\-formedness of the agent workflow, analogous to compiler\-level checks for programs\. Layer 2 develops a dependent\-type predicate system to specify pre\- and post\-conditions for individual execution steps\. It also enables us to uniformly model branching, looping, and submodule composition behaviors\. WithLLMExec, an assumption of LLMs’ local correctness, we are able to automate the proof of static semantic soundness while being extensible to new domains\. It is done by type matching, Hoare\-logic reasoning, and auxiliary theorems proved byFormalAgentLib\. This layer allows workflow specifications to be formally verified under assumptions before deployment, supporting correct\-by\-construction workflow design\(Seshia et al\.,[2022](https://arxiv.org/html/2606.06523#bib.bib30)\)\. Layer 3 uses a verified workflow with the help of an LLM to inspect execution trajectories, determine whether step\-level pre\- and post\-conditions are satisfied, and localize the execution step responsible for the failure\.

Building onFormalAgentLib, we further proposeLeanEvolve, a runtime workflow\-refinement method driven by trajectory verification and optional environment feedback\.LeanEvolveutilize an LLM together withFormalAgentLibverification results to identify flaws in current workflows and revise the specifications, thereby improving workflow’s performance\.

We summarize our contributions ofLean4Agentas follows: \(1\) We launchFormalAgentLib, to the best of our knowledge, the first extensible Lean4 library for formally modeling and verifying agent workflows’ semantic consistency under explicit assumptions, and enabling localization of failures revealed by trajectories\. \(2\) Based onFormalAgentLib, we proposeLeanEvolve, a formal\-guided workflow evolution method that uses verification feedback and optional environment signals to refine agent workflows\. \(3\) We conduct extensive experiments to evaluateLean4Agentthrough software\-engineering \(SWE\) task using a hard\-problem\-subset of SWE\-Bench\-Verified\(Jimenez et al\.,[2024](https://arxiv.org/html/2606.06523#bib.bib11)\)and AI\-paper understanding tasks using subset of ELAIP\-Bench\(Dai et al\.,[2025](https://arxiv.org/html/2606.06523#bib.bib6)\)across five leading LLMs\. Compared with workflows that fail verification,FormalAgentLib\-verified workflows achieve average improvements of14\.80%on the SWE task and9\.07%on the ELAIP\-Bench subset\. WithLeanEvolve, verified workflows achieve an additional average improvement of7\.47% on the SWE task\. This statistically significant improvement demonstrates the usefulness of theLean4Agent’s workflow verification and the effectiveness of its refinement method\.

Broadly speaking,Lean4Agentprovides a solid and unified basis for verifiable LLM\-agent systems and opens the door to future directions in training and developing self\-improving LLM agents\. It also offers principles for modeling long\-horizon black\-box systems\. To support further development of the field, we will open\-source the code in[https://github\.com/RickySkywalker/Lean4Agent](https://github.com/RickySkywalker/Lean4Agent)in the near future\.

## 2Methodology

This section introduces the design of theLean4Agentframework\. The goal is to provide a formal foundation for modeling and verifying agent workflows and trajectories under explicit assumptions and to use the formal guidance to improve workflow design\. Section[2\.1](https://arxiv.org/html/2606.06523#S2.SS1)introduces key preliminaries, Section[2\.2](https://arxiv.org/html/2606.06523#S2.SS2)describes the design ofFormalAgentLib, and Section[2\.3](https://arxiv.org/html/2606.06523#S2.SS3)presents theLeanEvolvemethod\.

### 2\.1Preliminaries

We define three central concepts used throughout this paper as follows:

LLM Agent:Following ReAct\(Yao et al\.,[2022](https://arxiv.org/html/2606.06523#bib.bib44)\), we define an LLM agent as the model that can perform the reasoning\-acting loop, where the model interleaves internal reasoning with task\-specific actions\. Reasoning enables the models to formulate, track, and revise their plan, while actions allow them to interact with external tools or information sources\.

Agent Workflow:We define agent workflow as an explicit, structured specification of how an LLM agent approaches a task\. Formally, we represent a workflow as a heterogeneous graph𝒢:=⟨V,E⟩\\mathcal\{G\}:=\\langle V,E\\rangle, whereV:=\{vi\}i=1nV:=\\\{v\_\{i\}\\\}\_\{i=1\}^\{n\}is the set of execution nodes andE⊆V×VE\\subseteq V\\times Vis the set of transitions\. Each node is represented asvi:=⟨ri,wi,ti,τi⟩v\_\{i\}:=\\langle r\_\{i\},w\_\{i\},t\_\{i\},\\tau\_\{i\}\\rangle, whererir\_\{i\}, andwiw\_\{i\}are the set of variables read and written by the node,tit\_\{i\}is the natural language \(NL\) instruction, andτi\\tau\_\{i\}is its execution type\. In our implementation, we use the YAML workflow format provided by AgentSPEX\(Wang et al\.,[2026](https://arxiv.org/html/2606.06523#bib.bib36)\)because it offers a clear type system for execution steps and transitions\. However, our formulation can be adapted to general workflow specifications with the control\-flow graph foundation\.

Execution Trajectory:We define an execution trajectory as the actual rollout produced when an LLM agent runs on a workflow\. It can be viewed as a valued path over𝒢\\mathcal\{G\}, formally, it is𝒯:=s0→s1→⋯→sl\\mathcal\{T\}:=s\_\{0\}\\rightarrow s\_\{1\}\\rightarrow\\cdots\\rightarrow s\_\{l\}, wheresi:=⟨p​r​ei,vji,g​e​ni,p​o​si⟩s\_\{i\}:=\\langle pre\_\{i\},v\_\{j\_\{i\}\},gen\_\{i\},pos\_\{i\}\\ranglewithp​r​eipre\_\{i\}andp​o​sipos\_\{i\}as pre\- and post\-execution state,vji∈Vv\_\{j\_\{i\}\}\\in Vis the workflow node executed at that transition, andg​e​nigen\_\{i\}records the LLM reasoning and tool\-call trace for a single ReAct\-style step\.

### 2\.2FormalAgentLib

We now detail the design ofFormalAgentLib, an extensible Lean4 library for uniformly modeling and verifying LLM\-agent workflows and trajectories\. To the best of our knowledge, it is the first effort to use expressive dependent\-type FL to verify agent behaviors\.FormalAgentLibis organized into three complementary layers: structural verification \(Section[2\.2\.1](https://arxiv.org/html/2606.06523#S2.SS2.SSS1)\), semantic verification \(Section[2\.2\.2](https://arxiv.org/html/2606.06523#S2.SS2.SSS2)\), and trajectory\-level analysis \(Section[2\.2\.3](https://arxiv.org/html/2606.06523#S2.SS2.SSS3)\)\.

#### 2\.2\.1Layer 1: Structural Verification

This layer provides the foundation for verifying LLM\-independent structural properties of agent workflows\. It defines a basic type system for variables, execution nodes, and graph transitions, enabling verification of the workflow’s structural well\-formedness\. Due to the space constraints, the full definitions are presented in Appendix[B\.1](https://arxiv.org/html/2606.06523#A2.SS1)\.

We construct this layer by first defining data types for workflow variables\. Specifically, we introduce the Lean inductive typeBaseTypeand implement compatibility relations following the ideas inSiek and Taha \([2006](https://arxiv.org/html/2606.06523#bib.bib31)\); Flanagan \([2006](https://arxiv.org/html/2606.06523#bib.bib10)\)\. We further defineStepType, an inductive type for modeling different kinds of execution nodes\. Among these,stepandtaskare most central, wherestepperforms an LLM query with conversation history, whereastaskexecutes without such history\. Together,BaseTypeandStepTypedefineWorkflowNode, the Lean modeling of an agent step\. For a nodevi=⟨ri,wi,ti,τi⟩v\_\{i\}=\\langle r\_\{i\},w\_\{i\},t\_\{i\},\\tau\_\{i\}\\rangle, we representri=\{rij\}j=1\|ri\|,wi=\{wij\}j=1\|wi\|r\_\{i\}=\\\{r\_\{i\_\{j\}\}\\\}\_\{j=1\}^\{\|r\_\{i\}\|\},w\_\{i\}=\\\{w\_\{i\_\{j\}\}\\\}\_\{j=1\}^\{\|w\_\{i\}\|\}, whererij,wijr\_\{i\_\{j\}\},w\_\{i\_\{j\}\}are typed variables andτi:StepType\\tau\_\{i\}:\\texttt\{StepType\}\.

We next defineWorkflowEdgeto model node\-transition patterns, including sequential execution, branching, and looping\. Using these foundation types, we formally model an agent workflow as:

𝒲=\(V,E,ve​n​t​r​y,X,P\)\\mathcal\{W\}=\(V,E,v\_\{entry\},X,P\)whereVVandEEare finite sets of typed nodes and edges,ve​n​t​r​y∈Vv\_\{entry\}\\in Vis the entry node,X⊆VX\\subseteq Vdenotes the exit nodes, andPPis the list of typed variables representing initial parameters in the context\.

The layer 1 modeling enables structural verification, such as node reachability, edge validity, and read/write consistency, analogous to simple compiler\-level verifications for programs\. For instance, we can detect read inconsistency when a node reads a variable that is neither an initial parameter nor produced by a reachable predecessor\. Appendix[B\.1\.6](https://arxiv.org/html/2606.06523#A2.SS1.SSS6)provides a detailed example of such an error\.

#### 2\.2\.2Layer 2: Static Semantic Verification for Agent Workflow

The second layer models and verifies the static semantic soundness of the agent workflow under explicit assumptions about the local LLM’s correctness\. To achieve this, we introduce a predicate\-based semantic verification system with three components: aPredicate Systemthat formally models the semantic properties of explicit and implicit variables, aSemantic Workflow Graphthat organizes these predicates across the workflow, and averification procedurethat verifies whether each step’s preconditions are entailed by previously established predicates\. Due to the space constraints, we provide the full formal details in Appendix[B\.2](https://arxiv.org/html/2606.06523#A2.SS2)\.

##### Predicate System

To verify the semantic soundness of a workflow, the first step is to translate the ambiguous NL description into concrete and verifiable constraints\. In particular, we define a predicate system on explicit and implicit variables to model such properties

A predicate denotes a decidable property of a variable\. We implement the core predicates in Lean as an inductive type, namedPredicateTypeor𝒫\\mathcal\{P\}\. Each base predicate is associated with an interpretation function,toProp, which maps the predicate to a Lean proposition specifying its behaviors\. For example,matchesJsonSchematakes a variable and a JSON schema, then verifies whether the variable provides a valid JSON value conforming to the given schema\. To support task\-specific predicates, we introduceext, which can be associated with aPredicateKeyand register user\-defined predicates to the predicate universe without modifying the existing definition ofPredicateType\. For predicates without a clear definition, we model them using thecustompredicate, with basic variable\-name existence verification and NL explanations for future LLM checks\.

Because not all semantic requirements correspond to explicit workflow variables, we also introduce implicit variables and graph\-level predicates\. For instance, our information\-flow predicates track which information each step consumes and produces, while context\-managing predicates specify which prior contexts a step may observe\. These graph\-level constraints help us detect non\-trivial errors, especially context\-management\-related inconsistencies that even humans can miss\.

##### Semantic Workflow Graph

The predicate system defines basic semantic constraints, while the semantic workflow graph organizes them across the agent workflow\. Its key idea is to constrain each LLM step as a Hoare\-style pre\- and post\-condition pair and then propagate those contracts through formal reasoning over the graph\.

We specify the semantics of an agent step using a predicate over its variables, with preconditions describing the properties that must hold before the step, and postconditions stating the properties expected to hold afterward\. Formally, we represent the Hoare\-style contract of an LLM step as a semantic \(workflow\) node:si=⟨ρi\(p​r​e\),vi,ρi\(p​o​s​t\)⟩s\_\{i\}=\\langle\\rho^\{\(pre\)\}\_\{i\},v\_\{i\},\\rho\_\{i\}^\{\(post\)\}\\ranglewherevi∈Vv\_\{i\}\\in Vis the base node in the workflow graph,ρi\(p​r​e\)\\rho\_\{i\}^\{\(pre\)\}is the list of required variable predicates, andρi\(p​o​s​t\)\\rho\_\{i\}^\{\(post\)\}is the list of variable predicates the step is intended to establish\. Beyond sequential execution steps, we also define loop and conditional semantic nodes to capture the contracts of iterative and branching behaviors following the principles inPratt \([1976](https://arxiv.org/html/2606.06523#bib.bib25)\)\.

We then organize these semantic nodes into a semantic \(workflow\) graph:

𝒮=⟨𝒢,sp​a​r​a,S,L,C⟩\\mathcal\{S\}=\\langle\\mathcal\{G\},s\_\{para\},S,L,C\\ranglewheresp​a​r​as\_\{para\}is a synthetic parameter node whose postconditions record predicates over the input parameters,SSis the set of ordinary semantic nodes,LLis the set of loop nodes, andCCis the set of conditional nodes\. The graph𝒮\\mathcal\{S\}is linked to the Layer\-1 workflow graph by the following well\-formedness invariant:

∀vi∈𝒢\.V,vi\.needSemanticSpec⇒∃sj∈S,s\.t\.​i=j\\forall v\_\{i\}\\in\\mathcal\{G\}\.V,v\_\{i\}\.\\texttt\{needSemanticSpec\}\\Rightarrow\\exists s\_\{j\}\\in S,\\text\{ s\.t\. \}i=j
This representation can also model submodule workflows by treating its postconditions insp​a​r​as\_\{para\}as its input contract and the return nodes’ preconditions as its output contract\. It allows submodules to be integrated into larger workflows\. In practice, we use LLMs to annotate the pre\- and post\- conditions from NL step instructions\.

##### Verification Procedure

We verify static semantic soundness under theLLMExecassumption: if an LLM step is executed in a predicate context satisfying its preconditions, then the execution can produce a context satisfying its postconditions\. Formally

∀si∈𝒮,∀Π,Π⊧ρi\(p​r​e\)⇒∃Π′=L​L​M​\(vi,Π\)∧Π′⊧ρi\(p​o​s​t\)\\forall s\_\{i\}\\in\\mathcal\{S\},\\forall\\Pi,\\Pi\\models\\rho\_\{i\}^\{\(pre\)\}\\Rightarrow\\exists\\Pi^\{\\prime\}=LLM\(v\_\{i\},\\Pi\)\\land\\Pi^\{\\prime\}\\models\\rho\_\{i\}^\{\(post\)\}whereΠ\\Pidenotes the current predicate context andΠ′\\Pi^\{\\prime\}denotes the context after executing stepviv\_\{i\}\. This assumption follows the previous analysis that LLMs can typically perform short\-horizon tasks well\(Lin et al\.,[2025a](https://arxiv.org/html/2606.06523#bib.bib16); Team et al\.,[2026b](https://arxiv.org/html/2606.06523#bib.bib33)\)and is also the reason why we can use LLMs to annotate predicates for individual steps\.

UnderLLMExec, layer\-2 verifies the local semantic soundness by ensuring that every node’s preconditions are satisfied before execution\. For example, explicit variables’ predicates can detect when a step refers to a JSON field that no predecessor establishes\. Appendix[B\.2\.5](https://arxiv.org/html/2606.06523#A2.SS2.SSS5)provides a concrete case\. We further analyze the graph\-level predicates in Section[3\.5\.1](https://arxiv.org/html/2606.06523#S3.SS5.SSS1)\.

Passing Layer\-2’s verification indicates that the workflow is semantically self\-contained with respect to the specified predicates and assumptions\. When a workflow fails, this layer identifies which step violates which requirements\. But such a failure does not imply that the workflow can never produce a correct answer\. Rather, it shows that the specification is not self\-contained\. In this way, Layer\-2 can better support correct\-by\-construction workflow design\.

#### 2\.2\.3Layer 3: Execution Trajectory Verification

The goal of this layer is to check whether theLLMExecassumption holds on particular trajectories\. For base predicates𝒫\\mathcal\{P\}, and their compositions, we can directly evaluate through corresponding Lean propositions\. For predicates that may be outside Lean’s decidable core, such as the URL connective check, we use external Python validators to add an additional layer of verification\. For variables that only have NL definitions, we use LLM\-as\-judge modules as complementary runtime checkers\. The LLM judge can consider comprehensive environment feedback, such as the SWE test\-case error messages, to support its assessments\. By analyzing the trajectory states against step\-level postconditions, Layer\-3 localizes the failure\-inducing steps, enabling runtime self\-checking and formal\-guided workflow evolution\.

Overall,FormalAgentLibprovides a foundation library for using Lean4 formal language to model and verify agent workflows\. It also enables localization of execution\-time failures by trajectories\.

### 2\.3LeanEvolve

Building onFormalAgentLib, we proposeLeanEvolve, a dual\-mode approach for refining agent workflows using execution trajectories, task outcomes, and verification diagnostics\.LeanEvolveis applied when a workflow passes Layer\-2 semantic verifications but produces incorrect or uncertain results on a particular execution\. In this setting, the goal is to revise the workflow so that future runs avoid the localized failure\.

The first mode isformal\-guided evolve\. It uses Layer\-3’s trajectory analysis fromFormalAgentLib, together with optional environment feedback, to localize the likely failure\-inducing step and the violated predicates\. We provide an LLM agent with that information to revise the corresponding part of the workflow\. If such feedback is unavailable, as in AI paper understanding tasks, the method relies solely on trajectory\-level verification\. For tasks that permit multiple attempts per instance,LeanEvolvealso includes apure\-LLM evolveadd\-on mode\. This mode performs a stepwise rewrite of the workflow using the trajectory and any available environmental feedback, without formal guidance\. It complements formal\-guided evolution by allowing broader exploration\. After the above refinement, we rerun the evolved workflow on the same problem to test whether it solves the instance\.

## 3Experiment

We evaluateLean4Agenton SWE\-Bench\-Verified\(Jimenez et al\.,[2024](https://arxiv.org/html/2606.06523#bib.bib11)\)and ELAIP\-Bench\(Dai et al\.,[2025](https://arxiv.org/html/2606.06523#bib.bib6)\)to assess the effectiveness ofFormalAgentLibverification andLeanEvolve\-based workflow refinement\. Section[3\.1](https://arxiv.org/html/2606.06523#S3.SS1)and[3\.2](https://arxiv.org/html/2606.06523#S3.SS2)describe the experiment setup, Section[3\.3](https://arxiv.org/html/2606.06523#S3.SS3)presents the main results, and Section[3\.4](https://arxiv.org/html/2606.06523#S3.SS4)and[3\.5](https://arxiv.org/html/2606.06523#S3.SS5)conduct ablation studies and case studies\.

### 3\.1Experiment Setup

#### 3\.1\.1Task and Benchmark

We assessLean4Agentacross two challenging agentic tasks: software engineering \(SWE\) and AI paper understanding task\. These tasks stress different aspects of agent execution, where SWE typically uses relatively direct workflows but requires substantial self\-directed exploration, debugging, and code modification with many implicit constraints\. In contrast, paper understanding benefits from fine\-grained workflow design that guides the model to systematically read, retrieve evidence, and answer questions\. Thus, the two settings respectively represent the LLM\-intensive and workflow\-intensive agent tasks\.

For the SWE task, we use SWE\-Bench\-Verified\(Jimenez et al\.,[2024](https://arxiv.org/html/2606.06523#bib.bib11)\), a benchmark for solving real\-world GitHub issues\. It also offers rich feedback from unit tests forLeanEvolve\. Following\(Robeyns et al\.,[2025](https://arxiv.org/html/2606.06523#bib.bib29); Xia et al\.,[2025](https://arxiv.org/html/2606.06523#bib.bib41)\), we randomly select a 50\-problem hard problem subset from the 500 problems in SWE\-Bench\-Verified to reduce experiment cost\. Those problems would typically take a human engineer more than 1 hour to solve\(Jimenez et al\.,[2024](https://arxiv.org/html/2606.06523#bib.bib11)\)\. For the paper understanding task, we use ELAIP\-Bench\(Dai et al\.,[2025](https://arxiv.org/html/2606.06523#bib.bib6)\), which is a benchmark of 403 multiple\-choice questions derived from recently published AI papers\. We randomly select 100 problems from the benchmark for the experiment\.

#### 3\.1\.2Experiment Methods

Because no prior experimental methods directly evaluate the formal modeling and verification of the workflows and trajectories of LLM agents, we design the following two experiments\. The first assesses the effectiveness ofFormalAgentLib’s semantic verification\. We prompt an LLM to independently generate multiple candidate workflows, filter out those that failed the linter verification in workflow language\. Then automatically generate the Layer\-2 specifications and run verification for those workflows\. From this set, we randomly select 3 verification\-passing workflows and 3 verification\-failing workflows for evaluation\. We measure the value of semantic verification by comparing the average task\-pass rate across benchmarks between the two groups\.

The second experiment we design evaluates Layer\-3’s trajectory verification andLeanEvolve\-based refinement\. For SWE, where test results provide rich environment feedback, we enable the pure\-LLM evolution add\-on inLeanEvolveand report the accumulated solved rate after refinement\. For paper understanding, where detailed feedback is unavailable, we compare formal\-guided evolution against pure\-LLM evolution on a 20\-problem subset of trajectories that initially fail, thereby directly evaluating the effect of verification\-guided localization\.

### 3\.2Implementation Details

In our implementation, we use Lean v4\.20\.0\. We generate 40 workflows and their Layer\-2 verification using Claude\-Opus\-4\.6\(Anthropic,[2026](https://arxiv.org/html/2606.06523#bib.bib1)\)\. To evaluate the cross\-model robustness of our framework, we run experiments on 5 leading LLMs, including GPT\-5\.2\(OpenAI,[2025](https://arxiv.org/html/2606.06523#bib.bib23)\), GLM\-5\(Zeng et al\.,[2026](https://arxiv.org/html/2606.06523#bib.bib46)\), Kimi\-K2\.5\(Team et al\.,[2026a](https://arxiv.org/html/2606.06523#bib.bib32)\), Qwen\-3\.5\-27B\(Qwen Team,[2026](https://arxiv.org/html/2606.06523#bib.bib26)\), and Gemma\-4\-31B\-it\(Farabet and Lacombe,[2026](https://arxiv.org/html/2606.06523#bib.bib9)\)111Due to the high cost of Claude\-Opus, we are unable to run full experiments on this model; we only evaluate it on the Layer\-2 SWE\-Bench experiment and report it in Appendix[A\.1](https://arxiv.org/html/2606.06523#A1.SS1)\.\.As described in Section[2](https://arxiv.org/html/2606.06523#S2), we apply AgentSPEX\(Wang et al\.,[2026](https://arxiv.org/html/2606.06523#bib.bib36)\)as the workflow execution engine, setting the temperature to 1\.0 and context length to 163,840\.

### 3\.3Main Results

Table 1:Main experimental results ofFormalAgentLib\-Layer 2 verification\.ModelSWE\-Bench\-VerifiedELAIP\-BenchAvg\. PassedAvg\. FailedDiff\.Avg\. PassedAvg\. FailedDiff\.Large ModelsGPT\-5\.262\.67%50\.00%12\.67%32\.00%20\.33%11\.67%GLM\-558\.00%50\.67%7\.33%37\.33%25\.00%10\.83%Kimi\-K2\.561\.33%46\.00%15\.33%36\.00%28\.33%7\.67%Small ModelsGemma\-4\-31B60\.00%32\.67%27\.33%35\.67%27\.33%8\.34%Qwen\-3\.5\-27B49\.33%38\.00%11\.33%42\.00%36\.67%5\.33%Average58\.27%43\.47%14\.80%36\.60%27\.53%9\.07%Table 2:LeanEvolveenhanced performance of SWE\-Bench hard problem subset\.
Table 3:Formal\-guided evolve compare with pure\-LLM evolve in ELAIP\-Bench subset\.

#### 3\.3\.1FormalAgentLibVerification Results

Table[1](https://arxiv.org/html/2606.06523#S3.T1)compares the performance of workflows that pass Layer\-2 verification with those that fail across 5 different models and 2 benchmarks\. On the hard subset of SWE\-Bench\-Verified, passing workflows outperform failing ones by14\.80%on average with a 95% bootstrap CI of\[10\.00%,19\.60%\]\[10\.00\\%,19\.60\\%\]\. On the ELAIP\-Bench subset, they achieve an average gain of9\.07%with 95% CI of\[5\.66%,13\.07%\]\[5\.66\\%,13\.07\\%\]\. These statistically significant improvements support the effectiveness ofFormalAgentLib’s semantic verification\.

On detailed analysis of the results, we observe that the gains are generally larger for smaller models, suggesting that weaker agents are more sensitive to workflow quality\. A closer analysis suggests that passing\-verification SWE workflows typically include more precise variable specifications, well\-structured retry loops, and more reasonable context management\. In contrast, failing workflows often contain unsatisfied preconditions, lack valid retry mechanisms, or use context\-insensitive execution steps cause break information flow\. For paper understanding, we also observed similar patterns, with an additional failure mode: some workflows split unified answer\-choice evaluation into separate per\-choice nodes with context awareness, which may affect later choices’ evaluation by earlier ones, violatingevaluateChoicesIndependentpredicate\. These results and findings highlight the effectiveness ofFormalAgentLibin supporting the correct\-by\-construction agent workflow design\.

#### 3\.3\.2LeanEvolveEnhancement Results

The results for two settings of evaluation forLeanEvolveare presented in Table[3](https://arxiv.org/html/2606.06523#S3.T3)and[3](https://arxiv.org/html/2606.06523#S3.T3)\. The Table[3](https://arxiv.org/html/2606.06523#S3.T3)shows that fullLeanEvolveimproves the performance of all evaluated models, adding7\.47%solved instances on average and raising the hard problem subset of SWE\-Bench’s accuracy rate from 56\.93% to 64\.40%\. Further analysis suggests that formal\-guided refinement is especially helpful for fixes that require understanding edge cases or cross\-file modifications, where localized diagnostics provide fine\-grained guidance\. Pure\-LLM evolution, on the other hand, contributes to broader exploration and is useful for instances that benefit from trial\-and\-error or non\-standard solutions\. Table[3](https://arxiv.org/html/2606.06523#S3.T3)indicates that formal\-guided evolution solves7\.00%more initially failed cases on average than pure\-LLM evolution\. The additional solved instances suggest that predicate\-based diagnostics can provide more fine\-grained modification, while pure\-LLM revisions typically do not accurately locate the correct step to modify\. These findings further support the effectiveness of formal\-guided workflow evolution\.

### 3\.4Ablation Studies

#### 3\.4\.1Ablation of Graph\-level predicates

We evaluate the contribution of graph\-level predicates by removing them from Layer\-2 semantic verification and measuring how many originally failing workflows flip to passing\. On ELAIP\-Bench, 21 out of 40 workflows originally fail the full Layer\-2 verification\. After removing graph\-level predicates, only 8 still fail, indicating that many defects are detected exclusively by graph\-level constraints\. The most common violation involvesmakeUnifiedJudgementandunifiedLoopBack, which capture workflow\-level consistency requirements that a local predicate alone is unable to model\. This result demonstrates the importance of our Layer\-2 verification\.

Table 4:Enhancement after we drop pure\-LLM evolve
#### 3\.4\.2Ablation of Pure\-LLM evolve

Another experiment we perform is to remove the pure\-LLM evolve add\-on from the fullLeanEvolveon SWE\-Bench to assess its contribution\. As shown in Table[4](https://arxiv.org/html/2606.06523#S3.T4),LeanEvolvestill improves the performance by 5\.07% on average without this component, but the gain is 2\.40% lower than that of the full system\. Inspection of the trajectories suggests that pure\-LLM add\-on contributes broad exploratory revisions that are not always captured by formal feedback\. Nevertheless, the remaining improvements confirm that formal\-guided evolution is the primary driver ofLeanEvolve’s performance\.

### 3\.5Case Studies

#### 3\.5\.1Workflow Errors identified byFormalAgentLib

This case study illustrates howFormalAgentLib’s semantic verification detects non\-trivial context management errors before the workflow’s roll\-out\. We present the example YAML workflow in Appendix[C\.1](https://arxiv.org/html/2606.06523#A3.SS1)\. Appendix[C\.1\.1](https://arxiv.org/html/2606.06523#A3.SS1.SSS1)demonstrates a SWE workflow composed entirely of context\-isolatedtasksteps\. Although the instructions repeatedly refer to information from previous execution turns, the execution type does not present the conversational context\. In particular,verify\_fixrequires thefix\_implementation\_evidence, whose full details are not available in the context\.FormalAgentLibidentifies this information\-flow error using the implicit variable’s predicate system\. Appendix[C\.1\.2](https://arxiv.org/html/2606.06523#A3.SS1.SSS2)presents another non\-trivial error in ELAIP\-Bench’s results\. In the workflow, each answer is evaluated by a context\-awarestep, so later option judgments may be influenced by the earlier ones\. This violates theevaluateChoicesIndependentpredicate, which requires independent or uniform evaluation of choices\. These two cases show thatFormalAgentLib’s verification can distinguish between completed context and information management cases\. They also demonstrateFormalAgentLib’s potential to support correct\-by\-construction workflow design\.

#### 3\.5\.2Workflow evolve study

This case study illustrates the error localization and repair capabilities of formal\-guided evolution inLeanEvolve\. We usedjango\_15098from SWE\-Bench running on the verified plan using GPT\-5\.2 as a representative example\. The base workflow is shown in Appendix[D\.1](https://arxiv.org/html/2606.06523#A4.SS1), and the evolution results are demonstrated in Appendix[C\.2](https://arxiv.org/html/2606.06523#A3.SS2)\. In the original execution, the model identifies only a top\-level symptom and fails to trace the root cause through import chains, resulting in an incorrect program fix\. The layer\-3 trajectory verification successfully localizes the failure to theverify\_fixstep, the workflow incorrectly treats the fix as verified even though failing tests remain\. Guided by this diagnosis,LeanEvolverevises the step instruction to require tracing the full error chain and validating the fix against the relevant tests, rather than stopping at the first apparent cause\. In the next round of execution, the new fix from the revised plan passes\. This example shows how trajectory\-level verification can pinpoint workflow flaws and guide the targeted repairs\.

## 4Related Work

### 4\.1Verification for agentic system

As agentic systems mature and are increasingly deployed in high\-stakes domains, there is a growing need to model and verify their behavior, especially in long\-horizon executions\. Existing work on agent verification spans several threads\. Among them, agent workflow languages and systems\(Chase,[2022](https://arxiv.org/html/2606.06523#bib.bib2); LangChain,[2024](https://arxiv.org/html/2606.06523#bib.bib13); Zeng and Yan,[2025](https://arxiv.org/html/2606.06523#bib.bib47); Vaziri et al\.,[2024](https://arxiv.org/html/2606.06523#bib.bib35); Wang et al\.,[2026](https://arxiv.org/html/2606.06523#bib.bib36)\)themselves provide a form of structural validation by organizing agent execution into typed or graph\-based workflows\. But they offer only limited guarantees of semantic correctness, and current advanced LLMs seldom make structural mistakes, making the workflow language linter less useful\. Another line of work verifies the tool or tool\-generated artifacts\(Miculicich et al\.,[2025](https://arxiv.org/html/2606.06523#bib.bib21); Liu et al\.,[2026](https://arxiv.org/html/2606.06523#bib.bib19); Doshi et al\.,[2026](https://arxiv.org/html/2606.06523#bib.bib8)\), which is crucial for reliable LLM agents but typically targets specific behaviors\. To the best of our knowledge, no existing framework formally models and verifies agent workflow and trajectory in a unified manner\.

### 4\.2LLMs for Formal Theorem Proving

Using LLMs for formal reasoning has recently become an active research direction\. Early work trained neural theorem provers to prove formalized mathematical theorems\(Wang et al\.,[2024](https://arxiv.org/html/2606.06523#bib.bib37); Xin et al\.,[2024](https://arxiv.org/html/2606.06523#bib.bib42); Wang et al\.,[2025b](https://arxiv.org/html/2606.06523#bib.bib39); Ren et al\.,[2025](https://arxiv.org/html/2606.06523#bib.bib28); Lin et al\.,[2025b](https://arxiv.org/html/2606.06523#bib.bib17),[c](https://arxiv.org/html/2606.06523#bib.bib18); Wang et al\.,[2025c](https://arxiv.org/html/2606.06523#bib.bib40); Chen et al\.,[2025](https://arxiv.org/html/2606.06523#bib.bib3)\)\. They establish the basis for modern LLMs’ formal reasoning capabilities\. Subsequent studies extend formal methods to broader settings, including NL math\(Yao et al\.,[2025](https://arxiv.org/html/2606.06523#bib.bib43); Wang et al\.,[2025a](https://arxiv.org/html/2606.06523#bib.bib38)\)and physics\(Li et al\.,[2025](https://arxiv.org/html/2606.06523#bib.bib14); community,[2024](https://arxiv.org/html/2606.06523#bib.bib4)\)\. Recent work also applies Lean to verify algorithms and programs\(Ye et al\.,[2025](https://arxiv.org/html/2606.06523#bib.bib45); Li et al\.,[2026](https://arxiv.org/html/2606.06523#bib.bib15); Zhao et al\.,[2026](https://arxiv.org/html/2606.06523#bib.bib48)\)\. However, these efforts largely focus on domains with precise specifications and well\-defined proof obligations\. LLM\-agent behavior is different, involving black\-box LLM executions, implicit information flows, and trajectory\-dependent outcomes\. To the best of our knowledge, no prior work has used expressive dependent\-type languages to model agent behaviors\.

## 5Conclusion

This paper presentsLean4Agent, to the best of our knowledge, the first comprehensive framework that applies dependent\-type formal language to uniformly model and verify LLM\-agent workflow and execution trajectories\.Lean4AgentlaunchesFormalAgentLib, an extensible Lean4 library for formally modeling and verifying agent workflows’ semantic consistency under explicit assumptions\. It also enables localization of execution\-time failures revealed by trajectories\. Based onFormalAgentLib, we developLeanEvolve, which refines agent workflows usingFormalAgentLib’s verification and optional environment feedback to further improve the task performance\. Extensive experiments on SWE and paper understanding tasks across 5 leading models indicate verification\-passing workflows outperform failing ones by an average of11\.94%\. In addition, workflows refined byLeanEvolveachieve a further average improvement of7\.47%on the SWE task\. Furthermore,Lean4Agentprovides a promising foundation for verifiable, self\-improving LLM\-agent systems through dependent type formal languages\.

## References

- Anthropic \[2026\]Anthropic\.Introducing Claude Opus 4\.6\.[https://www\.anthropic\.com/news/claude\-opus\-4\-6](https://www.anthropic.com/news/claude-opus-4-6), February 2026\.Accessed: 2026\-05\-03\.
- Chase \[2022\]Harrison Chase\.Langchain: Building applications with llms through composability\.[https://github\.com/langchain\-ai/langchain](https://github.com/langchain-ai/langchain), 2022\.
- Chen et al\. \[2025\]Jiangjie Chen, Wenxiang Chen, Jiacheng Du, Jinyi Hu, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Wenlei Shi, et al\.Seed\-prover 1\.5: Mastering undergraduate\-level theorem proving via learning from experience\.*arXiv preprint arXiv:2512\.17260*, 2025\.
- community \[2024\]The Physlib community\.Physlib: The lean physics library\.[https://github\.com/leanprover\-community/physlib](https://github.com/leanprover-community/physlib), 2024\.
- Coq \[1996\]Projet Coq\.The coq proof assistant\-reference manual\.*INRIA Rocquencourt and ENS Lyon, version*, 5, 1996\.
- Dai et al\. \[2025\]Xinbang Dai, Huikang Hu, Yongrui Chen, Jiaqi Li, Rihui Jin, Yuyang Zhang, Xiaoguang Li, Lifeng Shang, and Guilin Qi\.Elaipbench: A benchmark for expert\-level artificial intelligence paper understanding\.*arXiv preprint arXiv:2510\.10549*, 2025\.
- De Moura et al\. \[2015\]Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer\.The lean theorem prover \(system description\)\.In*Automated Deduction\-CADE\-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1\-7, 2015, Proceedings 25*, pages 378–388\. Springer, 2015\.
- Doshi et al\. \[2026\]Aarya Doshi, Yining Hong, Congying Xu, Eunsuk Kang, Alexandros Kapravelos, and Christian Kästner\.Towards verifiably safe tool use for llm agents\.*arXiv preprint arXiv:2601\.08012*, 2026\.
- Farabet and Lacombe \[2026\]Clement Farabet and Olivier Lacombe\.Gemma 4: Byte for byte, the most capable open models\.Google Keyword Blog\.[https://blog\.google/innovation\-and\-ai/technology/developers\-tools/gemma\-4/](https://blog.google/innovation-and-ai/technology/developers-tools/gemma-4/), April 2026\.Accessed: 2026\-05\-03\.
- Flanagan \[2006\]Cormac Flanagan\.Hybrid type checking\.In*Conference record of the 33rd ACM SIGPLAN\-SIGACT symposium on Principles of programming languages*, pages 245–256, 2006\.
- Jimenez et al\. \[2024\]Carlos E Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, and Karthik R Narasimhan\.SWE\-bench: Can language models resolve real\-world github issues?In*The Twelfth International Conference on Learning Representations*, 2024\.URL[https://openreview\.net/forum?id=VTF8yNQM66](https://openreview.net/forum?id=VTF8yNQM66)\.
- Kwon et al\. \[2023\]Woosuk Kwon, Zhuohan Li, Siyuan Zhuang, Ying Sheng, Lianmin Zheng, Cody Hao Yu, Joseph E\. Gonzalez, Hao Zhang, and Ion Stoica\.Efficient memory management for large language model serving with pagedattention\.In*Proceedings of the ACM SIGOPS 29th Symposium on Operating Systems Principles*, 2023\.
- LangChain \[2024\]LangChain\.Langgraph: Build resilient language agents as graphs\.[https://github\.com/langchain\-ai/langgraph](https://github.com/langchain-ai/langgraph), 2024\.
- Li et al\. \[2025\]Yuxin Li, Minghao Liu, Ruida Wang, Wenzhao Ji, Zhitao He, Rui Pan, Junming Huang, Tong Zhang, and Yi R Fung\.Lean4physics: Comprehensive reasoning framework for college\-level physics in lean4\.*arXiv preprint arXiv:2510\.26094*, 2025\.
- Li et al\. \[2026\]Zenan Li, Ziran Yang, Haoyu Zhao, Andrew Zhao, Shange Tang, Kaiyu Yang, Aarti Gupta, Zhendong Su, Chi Jin, et al\.Goedel\-code\-prover: Hierarchical proof search for open state\-of\-the\-art code verification\.*arXiv preprint arXiv:2603\.19329*, 2026\.
- Lin et al\. \[2025a\]Xixun Lin, Yucheng Ning, Jingwen Zhang, Yan Dong, Yilong Liu, Yongxuan Wu, Xiaohua Qi, Nan Sun, Yanmin Shang, Kun Wang, et al\.Llm\-based agents suffer from hallucinations: A survey of taxonomy, methods, and directions\.*arXiv preprint arXiv:2509\.18970*, 2025a\.
- Lin et al\. \[2025b\]Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin\.Goedel\-prover: A frontier model for open\-source automated theorem proving, 2025b\.URL[https://arxiv\.org/abs/2502\.07640](https://arxiv.org/abs/2502.07640)\.
- Lin et al\. \[2025c\]Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui\-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, et al\.Goedel\-prover\-v2: Scaling formal theorem proving with scaffolded data synthesis and self\-correction\.*arXiv preprint arXiv:2508\.03613*, 2025c\.
- Liu et al\. \[2026\]Yanming Liu, Xinyue Peng, Jiannan Cao, Xinyi Wang, Songhang Deng, Jintao Chen, Jianwei Yin, and Xuhong Zhang\.Toolgate: Contract\-grounded and verified tool execution for llms\.*arXiv preprint arXiv:2601\.04688*, 2026\.
- Martin\-Löf and Sambin \[1984\]Per Martin\-Löf and Giovanni Sambin\.*Intuitionistic type theory*, volume 9\.Bibliopolis Naples, 1984\.
- Miculicich et al\. \[2025\]Lesly Miculicich, Mihir Parmar, Hamid Palangi, Krishnamurthy Dj Dvijotham, Mirko Montanari, Tomas Pfister, and Long T Le\.Veriguard: Enhancing llm agent safety via verified code generation\.*arXiv preprint arXiv:2510\.05156*, 2025\.
- Moura and Ullrich \[2021\]Leonardo de Moura and Sebastian Ullrich\.The lean 4 theorem prover and programming language\.In*Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28*, pages 625–635\. Springer, 2021\.
- OpenAI \[2025\]OpenAI\.Introducing GPT\-5\.2\.[https://openai\.com/index/introducing\-gpt\-5\-2/](https://openai.com/index/introducing-gpt-5-2/), December 2025\.Accessed: 2026\-05\-03\.
- OpenAI \[2026\]OpenAI\.Introducing GPT\-5\.5, April 2026\.URL[https://openai\.com/index/introducing\-gpt\-5\-5/](https://openai.com/index/introducing-gpt-5-5/)\.Accessed: 2026\-05\-04\.
- Pratt \[1976\]Vaughan R Pratt\.Semantical considerations on floyd\-hoare logic\.In*17th Annual Symposium on Foundations of Computer Science \(sfcs 1976\)*, pages 109–121\. IEEE, 1976\.
- Qwen Team \[2026\]Qwen Team\.Qwen3\.5: Towards native multimodal agents, February 2026\.URL[https://qwen\.ai/blog?id=qwen3\.5](https://qwen.ai/blog?id=qwen3.5)\.
- Ramani et al\. \[2025\]Keshav Ramani, Vali Tawosi, Salwa Alamir, and Daniel Borrajo\.Bridging llm planning agents and formal methods: A case study in plan verification\.In*2025 40th IEEE/ACM International Conference on Automated Software Engineering Workshops \(ASEW\)*, pages 39–42\. IEEE, 2025\.
- Ren et al\. \[2025\]ZZ Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, et al\.Deepseek\-prover\-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition\.*arXiv preprint arXiv:2504\.21801*, 2025\.
- Robeyns et al\. \[2025\]Maxime Robeyns, Martin Szummer, and Laurence Aitchison\.A self\-improving coding agent\.*arXiv preprint arXiv:2504\.15228*, 2025\.
- Seshia et al\. \[2022\]Sanjit A Seshia, Dorsa Sadigh, and S Shankar Sastry\.Toward verified artificial intelligence\.*Communications of the ACM*, 65\(7\):46–55, 2022\.
- Siek and Taha \[2006\]Jeremy G Siek and Walid Taha\.Gradual typing for functional languages\.In*Scheme and functional programming workshop*, volume 6, pages 81–92, 2006\.
- Team et al\. \[2026a\]Kimi Team, Tongtong Bai, Yifan Bai, Yiping Bao, SH Cai, Yuan Cao, Y Charles, HS Che, Cheng Chen, Guanduo Chen, et al\.Kimi k2\. 5: Visual agentic intelligence\.*arXiv preprint arXiv:2602\.02276*, 2026a\.
- Team et al\. \[2026b\]MiroMind Team, S Bai, L Bing, L Lei, R Li, X Li, X Lin, E Min, L Su, B Wang, et al\.Mirothinker\-1\.7 & h1: Towards heavy\-duty research agents via verification\.*arXiv preprint arXiv:2603\.15726*, 2026b\.
- Tran et al\. \[2025\]Khanh\-Tung Tran, Dung Dao, Minh\-Duong Nguyen, Quoc\-Viet Pham, Barry O’Sullivan, and Hoang D Nguyen\.Multi\-agent collaboration mechanisms: A survey of llms\.*arXiv preprint arXiv:2501\.06322*, 2025\.
- Vaziri et al\. \[2024\]Mandana Vaziri, Louis Mandel, Claudio Spiess, and Martin Hirzel\.Pdl: a declarative prompt programming language\.*arXiv preprint arXiv:2410\.19135*, 2024\.
- Wang et al\. \[2026\]Pengcheng Wang, Jerry Huang, Jiarui Yao, Rui Pan, Peizhi Niu, Yaowenqi Liu, Ruida Wang, Renhao Lu, Yuwei Guo, and Tong Zhang\.Agentspex: An agent specification and execution language\.*arXiv preprint arXiv:2604\.13346*, 2026\.
- Wang et al\. \[2024\]Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang\.Theoremllama: Transforming general\-purpose llms into lean4 experts\.*arXiv preprint arXiv:2407\.03203*, 2024\.
- Wang et al\. \[2025a\]Ruida Wang, Yuxin Li, Yi R Fung, and Tong Zhang\.Let’s reason formally: Natural\-formal hybrid reasoning enhances llm’s math capability\.*arXiv preprint arXiv:2505\.23703*, 2025a\.
- Wang et al\. \[2025b\]Ruida Wang, Rui Pan, Yuxin Li, Jipeng Zhang, Yizhen Jia, Shizhe Diao, Renjie Pi, Junjie Hu, and Tong Zhang\.Ma\-lot: Model\-collaboration lean\-based long chain\-of\-thought reasoning enhances formal theorem proving\.*arXiv preprint arXiv:2503\.03205*, 2025b\.
- Wang et al\. \[2025c\]Ruida Wang, Jiarui Yao, Rui Pan, Shizhe Diao, and Tong Zhang\.Gar: Generative adversarial reinforcement learning for formal theorem proving\.*arXiv preprint arXiv:2510\.11769*, 2025c\.
- Xia et al\. \[2025\]Chunqiu Steven Xia, Zhe Wang, Yan Yang, Yuxiang Wei, and Lingming Zhang\.Live\-swe\-agent: Can software engineering agents self\-evolve on the fly?*arXiv preprint arXiv:2511\.13646*, 2025\.
- Xin et al\. \[2024\]Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al\.Deepseek\-prover\-v1\. 5: Harnessing proof assistant feedback for reinforcement learning and monte\-carlo tree search\.*arXiv preprint arXiv:2408\.08152*, 2024\.
- Yao et al\. \[2025\]Jiarui Yao, Ruida Wang, and Tong Zhang\.Fans–formal answer selection for natural language math reasoning using lean4\.*arXiv preprint arXiv:2503\.03238*, 2025\.
- Yao et al\. \[2022\]Shunyu Yao, Jeffrey Zhao, Dian Yu, Nan Du, Izhak Shafran, Karthik Narasimhan, and Yuan Cao\.React: Synergizing reasoning and acting in language models\.*arXiv preprint arXiv:2210\.03629*, 2022\.
- Ye et al\. \[2025\]Zhe Ye, Zhengxu Yan, Jingxuan He, Timothe Kasriel, Kaiyu Yang, and Dawn Song\.Verina: Benchmarking verifiable code generation\.*arXiv preprint arXiv:2505\.23135*, 2025\.
- Zeng et al\. \[2026\]Aohan Zeng, Xin Lv, Zhenyu Hou, Zhengxiao Du, Qinkai Zheng, Bin Chen, Da Yin, Chendi Ge, Chenghua Huang, Chengxing Xie, et al\.Glm\-5: from vibe coding to agentic engineering\.*arXiv preprint arXiv:2602\.15763*, 2026\.
- Zeng and Yan \[2025\]Sirui Zeng and Xifeng Yan\.Adl: A declarative language for agent\-based chatbots\.*arXiv preprint arXiv:2504\.14787*, 2025\.
- Zhao et al\. \[2026\]Haoyu Zhao, Ziran Yang, Jiawei Li, Deyuan He, Zenan Li, Chi Jin, Venugopal V Veeravalli, Aarti Gupta, and Sanjeev Arora\.Algoveri: An aligned benchmark for verified code generation on classical algorithms\.*arXiv preprint arXiv:2602\.09464*, 2026\.
- Zheng et al\. \[2023\]Lianmin Zheng, Wei\-Lin Chiang, Ying Sheng, Siyuan Zhuang, Zhanghao Wu, Yonghao Zhuang, Zi Lin, Zhuohan Li, Dacheng Li, Eric Xing, et al\.Judging llm\-as\-a\-judge with mt\-bench and chatbot arena\.*Advances in neural information processing systems*, 36:46595–46623, 2023\.

## Appendix AAdditional Experiment Results

This section presents additional experimental results omitted from the main paper due to space constraints\.

### A\.1Additional results on Claude

Due to the high evaluation cost of Claude models, we evaluate Claude 4\.5 Opus only on the 50\-hard\-problem subset of SWE\-Bench\-Verified\[Jimenez et al\.,[2024](https://arxiv.org/html/2606.06523#bib.bib11)\]\. The results indicate workflows that pass verification achieve an average accuracy of 67\.33%, whereas those that fail verification are only 56\.67% on average, yielding a 10\.67% absolute improvement\. This result provides additional evidence that the workflows selected by our verification procedure transfer across models\.

### A\.2Main results with 95% CI

To assess statistical significance, we report 95% paired bootstrap confidence intervals \(CIs\) computed from 10,000 resamples for both benchmarks across the five evaluated models\. The intervals are shown in Tables[5](https://arxiv.org/html/2606.06523#A1.T5)and[6](https://arxiv.org/html/2606.06523#A1.T6)\. In nearly all model\-task pairs, verification\-passing workflows significantly outperform verification\-failing ones\. The only exception is Qwen\-3\.5\-27B on ELAIP\-Bench, where the 95% CI includes zero; this suggests that the workflow\-quality gain is less pronounced for this setting, possibly because the model already achieves comparatively strong baseline performance on the task\.

Table 5:SWE\-BenchJimenez et al\. \[[2024](https://arxiv.org/html/2606.06523#bib.bib11)\]subset’s results with 95% CIModelAvg\. PassedAvg\. FailedDiff\.Lower CIUpper CILarge ModelsGPT\-5\.262\.67%50\.00%12\.67%5\.33%20\.67%GLM\-558\.00%50\.67%7\.33%0\.67%14\.00%Kimi\-K2\.561\.33%46\.00%15\.33%6\.00%24\.67%Small ModelsGemma\-4\-31B60\.00%32\.67%27\.33%18\.67%36\.00%Qwen\-3\.5\-27B49\.33%38\.00%11\.33%2\.67%20\.00%Average58\.27%43\.47%14\.80%10\.00%19\.60%Table 6:ELAIP\-Bench\-VerifiedDai et al\. \[[2025](https://arxiv.org/html/2606.06523#bib.bib6)\]subset’s results with 95% CIModelAvg\. PassedAvg\. FailedDiff\.Lower CIUpper CILarge ModelsGPT\-5\.232\.00%20\.33%11\.67%5\.00%18\.67%GLM\-537\.33%25\.00%10\.83%6\.33%18\.33%Kimi\-K2\.536\.00%28\.33%7\.67%1\.33%14\.00%Small ModelsGemma\-4\-31B35\.67%27\.33%8\.34%2\.33%14\.33%Qwen\-3\.5\-27B42\.00%36\.67%5\.33%\-0\.33%10\.67%Average36\.60%27\.53%9\.07%5\.66%13\.07%
### A\.3LLM\-as\-judge workflow quality analysis

Table 7:LLM\-as\-judge results for SWE\-Bench workflows
Table 8:LLM\-as\-judge results for ELAIP\-Bench workflows

To further evaluate the effectiveness of Layer\-2 semantic verification, we compareFormalAgentLibagainst the LLM\-as\-judge baseline using the strong GPT\-5\.5\[OpenAI,[2026](https://arxiv.org/html/2606.06523#bib.bib24)\]\. The judge is prompted with similar workflow descriptions and semantic requirements used for Lean\-based verification; the full prompts are provided inLLM\_as\_judge\_prompt\_SWE/ELAIP\.md\. Results are reported in Tables[8](https://arxiv.org/html/2606.06523#A1.T8)and[8](https://arxiv.org/html/2606.06523#A1.T8)\. On paper\-understanding tasks, where workflow quality is relatively easier to assess, the LLM judge largely agrees withFormalAgentLib’s verification\. In contrast, on SWE tasks, whose success criteria are more ambiguous and execution\-dependent, LLM\-based judgments show weak alignment with both Lean verification and empirical workflow performance\. This suggests that pure LLM\-based judgment is especially valuable in domains where workflow correctness is difficult to judge from surface\-level descriptions alone\. A closer inspection reveals that the LLM judge often captures only explicit workflow behavior, while missing implicit information flows, visible context information, and graph\-level predicate constraints\.

### A\.4Layer\-2 guided workflow refinement

To show that Layer\-2 semantic verification can guide workflow repair rather than merely select among existing candidates, we conduct an additional refinement experiment\. Starting from the failed\-1 workflow analyzed in Appendix[C\.1\.1](https://arxiv.org/html/2606.06523#A3.SS1.SSS1), Layer\-2 verification identifies a lack of context continuity across execution steps\. We therefore replace the context\-isolatedtasknodes with context\-awarestepnodes, which makes the workflow pass layer\-2 verification\. Re\-evaluation of the refined workflow using GPT\-5\.2 on the 50\-problem hard subset of SWE\-Bench\-Verified\[Jimenez et al\.,[2024](https://arxiv.org/html/2606.06523#bib.bib11)\]indicates an accuracy improvement from 52% to 62%, yielding a 10% absolute gain\. It further demonstrates the practical utility of Layer\-2 formal modeling and verification\.

## Appendix BDetails ofFormalAgentLibimplementation

TheFormalAgentLibcurrently contains 151 types and 611 functions to formally model the workflow, along with 41 theorems that help prove properties of agent workflows\. The core ofFormalAgentLibis almost entirely written by humans and verified to ensure correctness\. We use Lean code to detail the implementation of the type system in this section\.

### B\.1Layer 1’s details

#### B\.1\.1BaseTypeFull Definition

The full definition ofBaseTypeis as follows:

inductiveBaseTypewhere

\|TUnit:BaseType–Unitordefaulttype

\|TString:BaseType–stringvalue

\|TInt:BaseType–integervalue

\|TFloat:BaseType–floatvalue

\|TBool:BaseType–booleanvalue

\|TJson:BaseType–unstructuredjsondatavalue

\|TList:BaseType→BaseType–listofbasetypes

\|TDict:BaseType\-\>BaseType\-\>BaseType–dictionarytypewithkeyandvaluetypes

\|TSet:BaseType→BaseType–setofbasetypes

\|TOption:BaseType\-\>BaseType–optionalbasetype

\|TRecord:List\(String×BaseType\)\-\>BaseType–structuredrecordtype

\|TUnknown:BaseType–unknowntypeforgradualtyping

derivingRepr,Hashable,Inhabited

Additionally, we add the proof of DecidableEq for theBaseTypeto make the proof easier\.

#### B\.1\.2StepTypeFull Definition

The full definition ofStepTypeis as follows:

inductiveStepTypewhere

–PureYAMLsemantics,noLLMinvolved\.

\|forEachLoop–\(3\)Loopoveralist

\|whileLoop–\(4\)Loopwithacondition

\|conditional–\(5\)Conditionalbranch

\|setVariable–\(7\)Setavariable

\|incrementVariable–\(8\)Incrementavariable

\|switchBranch–\(13\)Switch/casestatement

\|returnValue–\(16\)Returnathevaluefromsubmoduletoparentworkflow

\|save–\(10\)Saveliteralcontenttoafile,expectedthefilesystemtochangebytheLLM

\|input–\(9\)Collectuserinput→TString

–LLMstepswithstructuredoutput

\|discover–\(5\)Extractstructuredlistsfromtextoutputforuseinloopsandothersteps,outputcantypicallybelistorjson

\|evaluate–\(11\)QualityscoringexpectedtoproduceaTFloat

\|validate–\(12\)Criteriacheck→TBool\(PASS/FAIL\)

–LLMstepswithunstructuredoutput

\|task–\(1\)Basicagentaction→TString

\|step–\(2\)Agentactionwithconversationhistory→TString

\|parallel–\(15\)Parallelexecution→TList\(modulereturntype\)

–Thecompositionsubmodule,whichiscomplicatedbehaviorthatcannotbedetermineduntilruntime,sowetreatitasunstructured\.

\|call–\(14\)Callsub\-module→dependsonmodule’sreturntype

\|gather–\(15\)Parallelheterogeneous→TListTJson

\|synthesize–\(6\)LLMwillcreatecomprehensiveoutputsandsavetofiles\.

derivingRepr,BEq,Inhabited

#### B\.1\.3WorkflowNodeFull Definition

The full definition ofWorkflowNodeis as follows:

structureWorkflowNodewhere

/–Uniquenumericidentifier\-/

id:NodeId

/–Optionalhuman\-readablename\-/

name:OptionString

/–WhichoftheYAMLsteptypes\-/

stepType:StepType

/–Variablesreadfromcontext,withexpectedtypes\-/

reads:ListTypedVar

/–Variableswrittentocontext,withtheirtypes\-/

writes:ListTypedVar

/–Theinstruction/promotstringforLLMsteps,foropwithoutLLM,thisisNone\.The\{\{var\}\}referencesinsideareextractedinto‘reads‘\.\-/

llmInstruction:OptionString

derivingRepr,BEq,Inhabited

#### B\.1\.4WorkflowEdgeFull Definition

TheWorkflowEdge’s type definitions are as follows, whereNodeIdis the unique identifier of aWorkflowNode, which is theiiinviv\_\{i\}\.

inductiveWorkflowEdgewhere

\|seqEdge:\(fromNode:NodeId\)\-\>\(toNode:NodeId\)\-\>WorkflowEdge–sequentialexecutionfrom\-\>to

\|branchEdge:\(cond:NodeId\)\-\>\(thenEntry:NodeId\)\-\>\(elseEntry:NodeId\)\-\>WorkflowEdge–conditional

\|loopEdge:\(header:NodeId\)\-\>\(bodyEntry:NodeId\)\-\>\(exit:NodeId\)\-\>WorkflowEdge–loopedge

\|loopBackEdge:\(bodyEnd:NodeId\)\-\>\(header:NodeId\)\-\>WorkflowEdge–whentheloopbodyends,backtotheheadertochecktheloopconditionagain

\|forkEdge:\(forkNode:NodeId\)\-\>\(branches:ListNodeId\)\-\>WorkflowEdge–parallelfork:forknode→parallelbranchentries

\|joinEdge:\(branches:ListNodeId\)\-\>\(joinNode:NodeId\)\-\>WorkflowEdge–Paralleljoin:parallelbranchexits→joinnode

\|switchEdge:\(switchNode:NodeId\)\-\>\(cases:ListNodeId\)\-\>\(defaultCase:OptionNodeId\)\-\>WorkflowEdge–Switch:switchnode→caseentries\+optionaldefault

derivingRepr,BEq,Inhabited

#### B\.1\.5WorkflowGraphFull Definition

The full definition ofWorkflowGraphis as follows:

structureWorkflowGraphwhere

nodes:ListWorkflowNode–Allnodesintheworkflow

edges:ListWorkflowEdge–Allcontrolflowedges

entry:NodeId–Entrynodeid\(whereexecutionstarts\)

exits:ListNodeId–Exitnodeids\(maybemultipleduetobranches\)

parameters:ListTypedVar–InitialparametersfromYAML"parameters"section

#### B\.1\.6Error case that layer 1 can identify\.

Layer\-1 verification detects structural errors in the workflow shown in Figure[2](https://arxiv.org/html/2606.06523#A2.F2)and[3](https://arxiv.org/html/2606.06523#A2.F3)\. In this example, the workflow uses aparallelstep to run four LLM branches and produce multiple intermediate results\. However, because nogatherstep propagates these branch\-local outputs back to the outer scope, downstream nodes cannot read the variables produced inside the parallel branches\. This scoping violation leads to a read\-consistency error\.

![Refer to caption](https://arxiv.org/html/2606.06523v1/x2.png)Figure 2:The workflow graph for layer\-1 failurename:"xxx"

goal:"xxx"

parameters:

\#omitted

config:

\#omitted

workflow:

\-parallel:

\-task:

\#Detailomitted

\-task:

\#Detailomitted

save\_as:"results\_q1"

\-task:

\#Detailomitted

save\_as:"results\_q2"

\-task:

\#Detailomitted

save\_as:"results\_q3"

\-task:

\#Detailomitted

save\_as:"results\_q4"

\-task:

name:"merge\_dedupe\_select\_candidates"

instruction:\|

YouaregivenfourJSONarraysofpaperrecords:\{\{results\_q1\}\},\{\{results\_q2\}\},\{\{results\_q3\}\},\{\{results\_q4\}\}\.

\#Detailomitted

save\_as:"candidate\_list"

Figure 3:Workflow with layer\-1 verified errors

### B\.2Layer 2’s details

#### B\.2\.1PredicateTypeFull Definition

inductivePredicateTypewhere

\|nameExists–Thebasepredicatecheckswhetheravariablenameexistsintheenvironment\.

\|isNonEmptyString–Thebasepredicatecheckswhetheravariableisanon\-emptystring\.

\|isNonEmptyList–Thebasepredicatecheckswhetheravariableisanon\-emptylist\.

\|isValidURL–WhethertheURLisvalid,correcpondingtothe‘isValidURL‘predicateinSemanticPredicates

\|isValidFilePath–Whetherthefilepathisvalid,correspondingtothe‘isValidFilePath‘predicateinSemanticPredicates

\|isValidPath–Whetherthepath\(fileorURL\)isvalid,correspondingtothe‘isValidPath‘predicateinSemanticPredicates

\|isValidBibtex–WhethertheBibtexentryisvalid,correspondingtothe‘isValidBibtex‘predicateinSemanticPredicates

\|isValidLatex–WhethertheLaTeXstringisvalid,correspondingtothe‘isValidLatex‘predicateinSemanticPredicates

\|isValidJson–WhethertheJSONstringisvalid,correspondingtothe‘isValidJson‘predicateinSemanticPredicates

\|isValidList–Whetherthevalueisavalidlist,correspondingtothe‘isValidList‘predicateinSemanticPredicates

\|toolExists–Whetherthetoolexistsintheenvironment,correspondingtothe‘toolExists‘predicateinSemanticPredicates

\|moduleExists–Whetherthemoduleexistsintheenvironment,correspondingtothe‘moduleExists‘predicateinSemanticPredicates

\|isInt–Whetherthevariableisaninteger,correspondingtothe‘isInt‘predicateintemp\_SemanticPredicatesExtended

\|matchesJsonSchema\(schema:JsonSchema\)–Whethertheprovidedjsonschemamatches,weperformrecursivechecking\.

\|isJsonWithFields\(fields:ListJsonFieldSpec\)–Whethertheprovidedjsonvaluehasthespecifiedfields,itissuedforcompatibility

\|containsSubstring\(substring:String\)–Whetherthestringvariablecontainsthegivensubstring\(forsentineldetection\)

\|fileExistsAtPath–Whetherthevariablerepresentsapathtoanexistingfile\(runtimecheck,staticjusttracksintent\)

\|taskCompleted–Markerpredicate:taskhasbeencompleted\(semanticintent,notruntimeverified\)

\|custom\(name:String\)–Thebasetypeforuserdefinedpredicates

\|ext\(key:PredicateKey\)–Thebasetypeforextensiblepredicates,thesemanticsofwhicharedefinedintheregistry

–Propositionalconnectivesforcomposingpredicates

\|predicateAnd\(p₁p₂:PredicateType\)–LogicalANDoftwopredicates

\|predicateOr\(p₁p₂:PredicateType\)–LogicalORoftwopredicates

derivingRepr,Inhabited,Hashable

#### B\.2\.2SemanticWorkflowNodeFull Definition

/–Thesemanticenvironment:atotalfunctionfromvariablenamestooptionalvalues\.\-/

defSemanticEnv:=String→OptionValue

structureSemanticWorkflowNodewhere

/–TheLayer1nodethisspecannotates\-/

baseNode:WorkflowNode

/–Decidablepreconditionrequirements\-/

precondVariables:ListVariablePredicateRequirement:=\[\]

/–Decidablepostconditionfactsestablished\-/

postcondVariables:ListVariablePredicateRequirement:=\[\]

/–Propprecondition\(auto\-derived\)\-/

precond:SemanticEnv→Prop:=

funenv=\>∀predVar∈precondVariables,predVar\.toPropenv

/–Postcondition:Aftertheexecutionofthisnode,whatshouldbetrueintheenvironmentinferredfromtheLLMpromptorpythoncode\.\-/

postcond:SemanticEnv→SemanticEnv→Prop:=

fun\_env’=\>∀predVar∈postcondVariables,predVar\.toPropenv’

#### B\.2\.3SemanticWorkflowGraphFull Definition

structureSemanticWorkflowGraphwhere

/–TheunderlyingLayer1WorkflowGraph\-/

baseGraph:WorkflowGraph

/–Theinitialnodewiththeparameterinformation\.Itspreconditionshouldbeemptyandthepostconditionshouldbeallrequirementsontheparametersaswellastools\.\-/

paramNode:SemanticWorkflowNode

/–Semanticnodeswithpre/postconditions\-/

semanticNodes:ListSemanticWorkflowNode

/–Loopnodesthatcontainsloop\-invariants\-/

loopNodes:ListSemanticLoopNode:=\[\]

/–Conditionalnodeswithbranch\-awarepostconditions\-/

conditionalNodes:ListSemanticConditionalNode:=\[\]

#### B\.2\.4Definition of LLM execution axiom

/–Axiom:TheLLMperformexecutionsjustasitsinstructionspecifygiventhepreconditionholds,thisisthecoreassumptionforstaticsemanticreasoning\.\-/

axiomllmExecAxiom

\(semanticNode:SemanticWorkflowNode\)

\(env:SemanticEnv\)

\(precond:semanticNode\.precondenv\):

∃env’,semanticNode\.postcondenvenv’

#### B\.2\.5Error case external predicates can locate

This example shows how external\-variable predicates can detect semantic violations in workflow outputs\. The erroneous workflow is shown in Figure[B\.2\.5](https://arxiv.org/html/2606.06523#A2.SS2.SSS5), and the corresponding Lean verification result is shown in Figure[5](https://arxiv.org/html/2606.06523#A2.F5)\. The stepcompose\_answerexpects fields inevidence\_packthat were never produced by the preceding step: for example, it reads fields such aspassagesandsummary, while the producer emits a different JSON structure\. As a result, the required schema predicate is unsatisfied, causing the workflow to fail Lean\-based semantic verification\.

name: "xxx" goal: "xxx" parameters: \# omitted config: \# omitted workflow: \# – Node 0: parse\_paper —————————————————\- \- step: name: parse\_paper instruction: \| Read the paper below and produce a brief structural overview\. Identify the title and the main section headings in document order\. Paper: paper\_content Return JSON with EXACTLY these keys: "title": <string\>, "sections": \[<string\>, …\] save\_as: paper\_data \# – Node 1: extract\_keywords ———————————————– \- step: name: extract\_keywords instruction: \| Pull 3\-7 keywords from the question stem that you would search for in the paper\. Question: question Return JSON with EXACTLY these keys: "keywords": \[<string\>, …\] save\_as: keyword\_data \# – Node 2: find\_evidence – PRODUCER of the disputed JSON —————\- \- step: name: find\_evidence instruction: \| Using keyword\_data\.keywords as search terms, locate verbatim passages in the paper that bear on the question\. Each snippet must appear word\-for\-word in the paper\. Paper: paper\_content Paper structure: paper\_data Return JSON with EXACTLY these keys: "snippets": \[ "text": <string\>, "source": <string\>, … \] save\_as: evidence\_pack \# – Node 3: compose\_answer – CONSUMER expecting the WRONG shape ———\- \- step: name: compose\_answer instruction: \| Using the evidence packet, write the final answer to the question\. Cite each passage by quoting it and giving its page number, then end with the executive summary supplied alongside the passages\. Question: question Passages: \- "p\.quote" \(page p\.page\) Executive summary: evidence\_pack\.summary save\_as: final\_answer

Figure 4:Workflow with layer\-2 verified errors on external variables✗Nodecompose\_answer\(ID3\):missingpredicatematchesJsonSchema\(AgenticKernel\.JsonSchema\.jObject

\[\("passages",

AgenticKernel\.JsonSchema\.jArray

\(AgenticKernel\.JsonSchema\.jObject

\[\("quote",AgenticKernel\.JsonSchema\.jString\),\("page",AgenticKernel\.JsonSchema\.jNum\)\]\)\),

\("summary",AgenticKernel\.JsonSchema\.jString\)\]\)forvariable’evidence\_pack’

Availablepredicates\(13\):

paper\_content:nameExists

question:nameExists

paper\_content:isNonEmptyString

question:isNonEmptyString

paper\_data:isNonEmptyString

paper\_data:isValidJson

paper\_data:matchesJsonSchema\(AgenticKernel\.JsonSchema\.jObject

\[\("title",AgenticKernel\.JsonSchema\.jString\),

\("sections",AgenticKernel\.JsonSchema\.jArray\(AgenticKernel\.JsonSchema\.jString\)\)\]\)

keyword\_data:isNonEmptyString

keyword\_data:isValidJson

keyword\_data:matchesJsonSchema\(AgenticKernel\.JsonSchema\.jObject\[\("keywords",AgenticKernel\.JsonSchema\.jArray\(AgenticKernel\.JsonSchema\.jString\)\)\]\)

evidence\_pack:isNonEmptyString

evidence\_pack:isValidJson

evidence\_pack:matchesJsonSchema\(AgenticKernel\.JsonSchema\.jObject

\[\("snippets",

AgenticKernel\.JsonSchema\.jArray

\(AgenticKernel\.JsonSchema\.jObject

\[\("text",AgenticKernel\.JsonSchema\.jString\),\("source",AgenticKernel\.JsonSchema\.jString\)\]\)\)\]\)

Figure 5:Lean evaluation results of Fig[B\.2\.5](https://arxiv.org/html/2606.06523#A2.SS2.SSS5)
## Appendix CExamples for Case Study

### C\.1Workflow Errors identified byFormalAgentLib

#### C\.1\.1Failed verification in SWE task

The failed verification plan in SWE\-Bench:

name:"swe\_agent"

goal:"GivenaGitHubissue,reproducethebugandfixitbymodifyingsourcecode,thensubmitapatch"

\\parsystem\_prompt:\|

Youareahelpfulassistantwhocaninteractmultipletimeswithacomputershelltosolveprogrammingtasks\.

STRICTFORMATRULES:

\-YourresponsemustcontainATMOSTonecodeblock\.

\-Ifyouincludemorethanonecodeblock,yourresponsewillbeREJECTED\.

\-ThecodeblockmustcontainONEcommand\(orcommandsconnectedwith&&or\|\|\)\.

\-Thecodeblockmustbeeitherabashblock\(rawshellcommand\)orasubagentblock\(subagentnameasthefencelanguage\)\.

\-Ifyouhavenothingtoexecute,respondwithplaintextandNOcodeblock\.

IncludeaTHOUGHTsectionbeforeyourcommandwhereyouexplainyourreasoningprocess\.

<format\_example\>

THOUGHT:Youshouldfirstconsiderthetaskgoal,yourcurrentstate,andplanforyourfutureactions\.Thentelltheuserwhetheryouwanttorunabashcommandorcallasubagenttohelpwithataskandexplainindepthwhyorwhynot\.

\\par“‘bash

your\_command\_here

“‘

</format\_example\>

\\parconfig:

model:"$\{MODEL\_NAME\}"

temperature:1\.0

model\_kwargs:

reasoning\_effort:"high"

max\_tool\_calls\_per\_step:20

expose\_submodules\_as\_tools:false

enable\_inline\_tool\_calls:true

\\parparameters:

code\_path:"$\{CODE\_PATH:\-/workspace/tmp/repo\}"

problem\_statement:"$\{PROBLEM\_STATEMENT\}"

regression\_test\_cmd:""

\\parworkflow:

\#Step1:Presenttheproblemandorienttheagent

\-task:

name:"setup\_and\_explore"

instruction:\|

<pr\_description\>

ConsiderthefollowingPRdescription:

\{\{problem\_statement\}\}

</pr\_description\>

\\parYou’reasoftwareengineerinteractingcontinuouslywithacomputerbysubmittingcommands\.

You’llbehelpingimplementnecessarychangestomeetrequirementsinthePRdescription\.

Yourtaskisspecificallytomakechangestonon\-testfilesinthecurrentdirectoryinordertofixtheissuedescribedinthePRdescriptioninawaythatisgeneralandconsistentwiththecodebase\.

<IMPORTANT\>ThisisaninteractiveprocesswhereyouwillthinkandissueATLEASTONEcommandforeverystep,seetheresult,thenthinkandissueyournextcommand\(s\)\.</IMPORTANT\>

\\parForeachresponse:

1\.IncludeaTHOUGHTsectionexplainingyourreasoningandwhatyou’retryingtoaccomplish

2\.Provideoneormorebashtoolcallstoexecute

\\parIMPORTANTBOUNDARIES:

\-MODIFY:Regularsourcecodefilesin/testbed\(thisistheworkingdirectoryforallyoursubsequentcommands\)

\-DONOTMODIFY:Tests,configurationfiles\(pyproject\.toml,setup\.cfg,etc\.\)

\\parBeginbyexploringtherepositorystructuretounderstandthecodebase\.IdentifytherelevantsourcefilesthatmayneedtobechangedbasedonthePRdescription\.

\\parYouareoperatinginanenvironmentwhere:

1\.Youissueatleastonecommand

2\.Thesystemexecutesthecommand\(s\)inasubshell

3\.Youseetheresult\(s\)

4\.Youwriteyournextcommand\(s\)

Eachresponseshouldinclude:

1\.\*\*Reasoningtext\*\*whereyouexplainyouranalysisandplan

2\.Atleastonetoolcallwithyourcommand

\*\*CRITICALREQUIREMENTS:\*\*

\-YourresponseSHOULDincludereasoningtextexplainingwhatyou’redoing

\-YourresponseMUSTincludeATLEASTONEbashtoolcall\.YoucanmakeMULTIPLEtoolcallsinasingleresponsewhenthecommandsareindependent\(e\.g\.,searchingmultiplefiles,readingdifferentpartsofthecodebase\)\.

\-Directoryorenvironmentvariablechangesarenotpersistent\.Everyactionisexecutedinanewsubshell\.

\-However,youcanprefixanyactionwith‘MY\_ENV\_VAR=MY\_VALUEcd/path/to/working/dir&&…‘orwrite/loadenvironmentvariablesfromfiles

\\parEnvironmentdetails:

\-YouhaveafullLinuxshellenvironment

\-Alwaysusenon\-interactiveflags\(\-y,\-f\)forcommands

\-Avoidinteractivetoolslikevi,nano,oranythatrequireuserinput

\-Youcanusebashcommandsorinvokeanytoolthatisavailableintheenvironment

\-Youcanalsocreatenewtoolsorscriptstohelpyouwiththetask

\-Ifatoolisn’tavailable,youcanalsoinstallit

\\parStartnow\.Exploretherepositoryat\{\{code\_path\}\}tounderstandtheprojectstructure,findrelevantfiles,andunderstandthecodebaseorganization\.Usecommandslike‘find‘,‘ls‘,‘cat‘,‘grep‘tonavigateandunderstandthecode\.

\\par\#Step2:Reproducetheissue

\-task:

name:"reproduce\_issue"

instruction:\|

<pr\_description\>

ConsiderthefollowingPRdescription:

\{\{problem\_statement\}\}

</pr\_description\>

\\parBasedonyourexplorationofthecodebase,nowcreateascripttoreproducetheissuedescribedinthePRdescription\.WriteasmallPython\(orappropriatelanguage\)scriptthatdemonstratesthebug\.

\\parSteps:

1\.Createareproductionscriptat/testbed/reproduce\_issue\.py\(orappropriateextension\)

2\.Runthescripttoconfirmtheissueexists

3\.Analyzetheerroroutputtounderstandtherootcause

\\parIMPORTANT:

\-Theworkingdirectoryforallcommandsis/testbed

\-Directoryorenvironmentvariablechangesarenotpersistent

\-Prefixcommandswith‘cd/testbed&&…‘

\-YourresponseMUSTincludeATLEASTONEbashtoolcall

\\par\#Step3:Identifyandimplementthefix

\-task:

name:"implement\_fix"

instruction:\|

<pr\_description\>

ConsiderthefollowingPRdescription:

\{\{problem\_statement\}\}

</pr\_description\>

\\parNowthatyou’vereproducedtheissueandunderstandtherootcause,implementafix\.

\\parFollowthisworkflow:

1\.Identifytheexactsourcefile\(s\)andlocation\(s\)thatneedtobemodified

2\.Understandthesurroundingcodelogicbeforemakingchanges

3\.Implementtheminimal,targetedfixthataddressestheissue

4\.Makesureyourfixisgeneralandconsistentwiththeexistingcodebasepatterns

\\parIMPORTANTBOUNDARIES:

\-MODIFY:Regularsourcecodefilesin/testbed

\-DONOTMODIFY:Tests,configurationfiles\(pyproject\.toml,setup\.cfg,etc\.\)

\-Theworkingdirectoryforallcommandsis/testbed

\-Directoryorenvironmentvariablechangesarenotpersistent

\-Prefixcommandswith‘cd/testbed&&…‘

\-Use‘sed‘,‘python\-c‘,orheredoctoeditfiles\(nointeractiveeditors\)

\-YourresponseMUSTincludeATLEASTONEbashtoolcall

\\par\#Step4:Verifythefix

\-task:

name:"verify\_fix"

instruction:\|

<pr\_description\>

ConsiderthefollowingPRdescription:

\{\{problem\_statement\}\}

</pr\_description\>

\\parVerifyyourfixworkscorrectly:

1\.Runyourreproductionscriptagaintoconfirmtheissueisresolved

2\.Testedgecasestoensureyourfixisrobustanddoesn’tintroduceregressions

3\.Ifaregressiontestcommandisavailable\(\{\{regression\_test\_cmd\}\}\),runit

4\.Ifthefixdoesn’twork,iterate:analyzewhatwentwrong,adjust,andre\-test

\\parIMPORTANT:

\-Theworkingdirectoryforallcommandsis/testbed

\-Directoryorenvironmentvariablechangesarenotpersistent

\-Prefixcommandswith‘cd/testbed&&…‘

\-YourresponseMUSTincludeATLEASTONEbashtoolcall

\\par\#Step5:Submitthepatch

\-task:

name:"submit\_patch"

instruction:\|

Yourfixhasbeenverified\.Nowsubmityourchangesasagitpatch\.

\\parFollowthesestepsINORDER,withSEPARATEcommands:

\\parStep1:Createthepatchfile

Run‘cd/testbed&&gitdiff–path/to/file1path/to/file2\>patch\.txt‘listingonlythesourcefilesyoumodified\.

DoNOTcommityourchanges\.

<IMPORTANT\>

Thepatchmustonlycontainchangestothespecificsourcefilesyoumodifiedtofixtheissue\.

Donotsubmitfilecreationsorchangestoanyofthefollowingfiles:

\-testandreproductionfiles\(e\.g\.,reproduce\_issue\.py\)

\-helperscripts,tests,ortoolsthatyoucreated

\-installation,build,packaging,configuration,orsetupscriptsunlesstheyaredirectlypartoftheissueyouwerefixing\(youcanassumethattheenvironmentisalreadysetupforyourclient\)

\-binaryorcompiledfiles

</IMPORTANT\>

\\parStep2:Verifyyourpatch

Inspectpatch\.txttoconfirmitonlycontainsyourintendedchangesandheadersshow‘—a/‘and‘\+\+\+b/‘paths\.

\\parStep3:Submit\(EXACTcommandrequired\)

YouMUSTusethisEXACTcommandtosubmit:

“‘bash

echoCOMPLETE\_TASK\_AND\_SUBMIT\_FINAL\_OUTPUT&&catpatch\.txt

“‘

Ifthecommandfails\(nonzeroexitstatus\),itwillnotsubmit\.

\\par<CRITICAL\>

\-Creating/viewingthepatchandsubmittingitMUSTbeseparatecommands\(notcombinedwith&&\)\.

\-Ifyoumodifypatch\.txtafterverifying,youSHOULDverifyagainbeforesubmitting\.

\-YouCANNOTcontinueworking\(reading,editing,testing\)inanywayonthistaskaftersubmitting\.

\-Unlessyouthinkthetaskisfinishedandreadyforsubmission,youMUSTcontainatool\-callineveryresponse\.Whenyoumakenotoolcall,itwillbetreatedasasignalthatyouhavealreadycompletedthetaskandsubmittedyouranswer,andthesystemwillstopyoufrommakinganyfurthertoolcalls\.

</CRITICAL\>

#### C\.1\.2Failed verification in ELAIP\-Bench

name:"elaipbench\_agent\_bad\_plan\_4"

goal:"Answeranacademicpaperquestionbasedontheprovidedpassage"

system\_prompt:\|

Youareanexpertacademicresearcherskilledatreadingandunderstandingscientificpapers\.Youanswerquestionsaboutacademicpapersbycarefullyanalyzingtheprovidedpassage\.Bepreciseandselectonlytheanswer\(s\)thataresupportedbythepassage\.

config:

model:"$\{MODEL\_NAME\}"

temperature:1\.0

max\_tokens:163840

enabled\_tools:\[\]

enable\_inline\_tool\_calls:true

parameters:

question:""

paper\_content:""

question\_type\_instruction:""

question\_type:""

\\parworkflow:

\-step:

name:skim\_paper

instruction:\|

Readthepaperandproduceabriefoverview\.

\\parPaper:

\{\{paper\_content\}\}

\\parReturnJSON:

\{

"title":"",

"abstract\_summary":""

\}

save\_as:paper\_overview

\\par\-step:

name:extract\_section\_headings

instruction:\|

Fromthepaperbelow,listthemainsectionheadingsintheordertheyappear\.

\\parPaper:

\{\{paper\_content\}\}

\\parReturnaJSONarrayofstrings,e\.g\.\["Introduction","Method","Experiments","Conclusion"\]\.

save\_as:section\_headings

\\par\-step:

name:extract\_keywords

instruction:\|

Readthequestionstem\(doNOTyetlookatthefouransweroptions\)andextractthemost

discriminativekeywordsorphrasesthatshouldbeusedtofindtherelevantevidencein

thepaper\.

\\parAlsonoteexplicitlywhetherthequestioncontainsnegationcuessuchas

"NOT","incorrect","wrong","false","except",oranysimilarmarker\.

\\parPaperoverview:

\{\{paper\_overview\}\}

Sectionheadings:\{\{section\_headings\}\}

Question:

\{\{question\}\}

\\parReturnJSON:

\{

"keywords":\[\],

"negation":trueorfalse,

"stem\_summary":""

\}

save\_as:question\_analysis

\\par\-step:

name:classify\_question\_type

instruction:\|

Decidewhetherthequestionexpectsasinglecorrectoption\(Single\-answer\)or

multiplecorrectoptions\(Multiple\-answer\)\.

\\parQuestion:

\{\{question\}\}

\{\{question\_type\_instruction\}\}

\\parReturnoneofthestrings:"Single\-answer"or"Multiple\-answer"\.

save\_as:question\_kind

\\par\-step:

name:search\_keywords\_in\_paper

instruction:\|

Usingthekeywordsfromthequestionanalysis,locateeveryparagraphinthepaper

thatmentionsanyofthosekeywordsorcloselyrelatedconcepts\.

\\parKeywords:\{\{question\_analysis\.keywords\}\}

Paper:

\{\{paper\_content\}\}

\\parReturnJSON:

\{

"candidate\_paragraphs":\[

\{"text":"…","matched\_keywords":\[\]\}

\]

\}

save\_as:candidate\_paragraphs

\\par\-step:

name:filter\_relevant\_paragraphs

instruction:\|

Fromthecandidateparagraphsbelow,keeponlythosethatdirectlybearonthe

question’sstem\.Droptangentialmatches\.

\\parCandidateparagraphs:\{\{candidate\_paragraphs\}\}

Questionstemsummary:\{\{question\_analysis\.stem\_summary\}\}

\\parReturnatmost5evidencesnippets,copiedverbatimfromthepaper\.

\\parReturnJSON:

\{

"evidence\_snippets":\[

\{"text":"…","reason":""\}

\]

\}

save\_as:evidence

\\par\-step:

name:verify\_evidence\_quality

instruction:\|

Brieflyjudgewhethertheevidencebelowissufficienttodiscriminateamongthe

fouransweroptions\.Noteanyobviousgaps\.Donotyetlookattheoptionsthemselves\.

\\parQuestionstem:\{\{question\_analysis\.stem\_summary\}\}

Evidence:\{\{evidence\}\}

\\parReturnashortparagraphoffree\-formprose\.

save\_as:evidence\_check

\\par\-step:

name:evaluate\_A

instruction:\|

JudgeoptionAindependentlyofanyotheroption\.

Question:\{\{question\}\}

Evidence:\{\{evidence\}\}

ReturnJSON:

\{

"verdict":"supported/contradicted/not\_established",

"reason":"",

"evidence\_text":""

\}

save\_as:judgment\_A

\\par\-step:

name:evaluate\_B

instruction:\|

JudgeoptionBindependentlyofanyotheroption\.

Question:\{\{question\}\}

Evidence:\{\{evidence\}\}

ReturnJSON:

\{

"verdict":"supported/contradicted/not\_established",

"reason":"",

"evidence\_text":""

\}

save\_as:judgment\_B

\\par\-step:

name:evaluate\_C

instruction:\|

JudgeoptionCindependentlyofanyotheroption\.

Question:\{\{question\}\}

Evidence:\{\{evidence\}\}

ReturnJSON:

\{

"verdict":"supported/contradicted/not\_established",

"reason":"",

"evidence\_text":""

\}

save\_as:judgment\_C

\\par\-step:

name:evaluate\_D

instruction:\|

JudgeoptionDindependentlyofanyotheroption\.

Question:\{\{question\}\}

Evidence:\{\{evidence\}\}

ReturnJSON:

\{

"verdict":"supported/contradicted/not\_established",

"reason":"",

"evidence\_text":""

\}

save\_as:judgment\_D

\\par\-switch:

variable:"question\_type"

cases:

"MA\-MCQ":

\-set\_variable:

name:recheck\_count

value:0

\\par\-while:

condition:"recheck\_count<3"

max\_iterations:3

steps:

\-step:

name:aggregate\_and\_recheck

instruction:\|

Thequestionismulti\-answer\(typically2\-3correctoptions\)\.

Per\-optionjudgmentssofar:

A:\{\{judgment\_A\}\}

B:\{\{judgment\_B\}\}

C:\{\{judgment\_C\}\}

D:\{\{judgment\_D\}\}

\\parCounthowmanyoptionsweremarked"supported"\.

Iffewerthan2are"supported",revisittheborderlineoptionswith

aslightlymorelenientstandardandupdatetheirverdicts\.Otherwise,

keeptheverdictsastheyare\.

\\parReturnJSON:

\{

"selected\_options":\[\],

"selected\_count":0,

"notes":""

\}

save\_as:combined\_judgment

\\par\-increment:recheck\_count

\\par\-step:

name:finalize\_multi\_answer

instruction:\|

Basedonthecombinedjudgmentsbelow,writethefinalanswer\.

Question:\{\{question\}\}

Combinedjudgment:\{\{combined\_judgment\}\}

\{\{question\_type\_instruction\}\}

save\_as:final\_response

\\par"SA\-MCQ":

\-step:

name:finalize\_single\_answer

instruction:\|

Basedontheper\-optionjudgmentsbelow,selecttheONEcorrectanswer\.

Question:\{\{question\}\}

A:\{\{judgment\_A\}\}

B:\{\{judgment\_B\}\}

C:\{\{judgment\_C\}\}

D:\{\{judgment\_D\}\}

\{\{question\_type\_instruction\}\}

save\_as:final\_response

### C\.2Workflow evolve study example

This is an example of the workflow evolution study\. The Lean verification results for the falsified step are shown in Figure[6](https://arxiv.org/html/2606.06523#A3.F6), and the iterative workflow step is shown in Figure[7](https://arxiv.org/html/2606.06523#A3.F7)\.

Step3\(verify\_fix\)

trace:8LLMiter,7toolcall\(s\),tools:\[shell\_run\]

\\parLayer2postconditioncontract:5predicate\(s\)\(1runtime\+4sentinel\(s\)\)

\\par\[1\]\_\_step\_tag\_3:ext\(PredicateKey\(step\_tag,verificatory,\[\]\)\)

\(sentinel—Layer2metadatamarker;runtimeverificationnotapplicable\)

\\par\[2\]\_\_graph\_contrib\_3\_fix\_verified:ext\(PredicateKey\(graph\_level,subGoalContribution,\[str\(fix\_verified\)\]\)\)

\(sentinel—Layer2metadatamarker;runtimeverificationnotapplicable\)

\\par\[3\]\_\_graph\_verify\_3\_fix\_implemented:ext\(PredicateKey\(graph\_level,subGoalVerification,\[str\(fix\_implemented\)\]\)\)

\(sentinel—Layer2metadatamarker;runtimeverificationnotapplicable\)

\\par\[4\]\_\_node\_cap\_3\_implicit\_retry\_fix\_verified:ext\(PredicateKey\(node\_capability,implicitRetry,\[str\(fix\_verified\)\]\)\)

\(sentinel—Layer2metadatamarker;runtimeverificationnotapplicable\)

\\par\[5\]fix\_verification\_evidence:isNonEmptyString

\[Lean\]✓typed\-statepredicatesatisfied

\[Tool\]✗thispredicateclaimsverificationisdonebut2test\(s\)ultimatelyfailed

\[LLM\]✗EvalevidenceshowstheinstanceisunresolvedwithFAIL\_TO\_PASSfailuresini18n\.tests\.MiscTests\.test\_get\_language\_from\_path\_real\(assertionNone\!=de\-1996,etc\.\)andtest\_get\_supported\_language\_variant\_null,indicatingverificationdidnotsucceed\.Thestepitselfranthei18nsuite\(runtests\.pyi18n–failfast\)buttoolcall\#4returnedrc=1,consistentwithfailingtests\.

⇒✗FALSIFIED—\[Tool\]thispredicateclaimsverificationisdonebut2test\(s\)ultimatelyfailed\|\|\[LLM\]EvalevidenceshowstheinstanceisunresolvedwithFAIL\_TO\_PASSfailuresini18n\.tests\.MiscTests\.test\_get\_language\_from\_path\_real\(assertionNone\!=de\-1996,etc\.\)andtest\_get\_supported\_language\_variant\_null,indicatingverificationdidnotsucceed\.Thestepitselfranthei18nsuite\(runtests\.pyi18n–failfast\)buttoolcall\#4returnedrc=1,consistentwithfailingtests\.

\\par⇒STEPCOMPOSITE:✗FALSIFIEDonpredicate\(s\):fix\_verification\_evidence

RE\-ROLL:\[verify\_fix\]predicate\(s\)failed:fix\_verification\_evidence\.ModifytheYAMLinstructionto:replaceanykeyword\-filteredpytestwiththeexplicitFAIL\_TO\_PASStestpath;requirezeronewfailuresacrosstheaffectedtestclass;donotdismisscollectionerrorsas’unrelated’\.

Figure 6:Trajectory verification for workflow evolve exampleBefore

\{yamlblock\}\- step: name: "verify\_fix" instruction: \| Now verify that your fix resolves the issue\. Steps: 1\. Re\-run the reproduction script you created earlier to confirm the issue is fixed 2\. If there is a regression test command available, run it: regression\_test\_cmd\{yamlblockred\}2\. Run the regression test command: regression\_test\_cmd 3\. Examine the test output carefully\. If any tests fail, analyze whether they are: \- FAIL\_TO\_PASS tests that should now pass with your fix \- PASS\_TO\_PASS tests that were passing before but now fail \(regression\) 4\. If PASS\_TO\_PASS tests fail, your fix has introduced a regression\. A fix that breaks existing functionality is worse than no fix\. Revert and refine your approach\. 5\. Only proceed when all tests pass\{yamlblock\}Remember: \- Work in the /testbed directory \- Every response MUST include at least one bash tool call

After

\{yamlblock\}\- step: name: "verify\_fix" instruction: \| Now verify that your fix resolves the issue\. Steps: 1\. Re\-run the reproduction script you created earlier to confirm the issue is fixed 2\. If there is a regression test command available, run it: regression\_test\_cmd\{yamlblockgreen\}3\. Test edge cases to ensure your fix is robust and doesn’t break other functionality 4\. Avoid adding top\-level ‘import‘ statements to existing modules unless the imported name is unavoidably required at module load time\. Prefer function\-local imports to sidestep circular\-import and import\-time\-side\-effect pitfalls\. After any edit that touches imports, sanity\-check the module with ‘python \-c ’import <module\_path\>’‘ before running tests — if this fails, every downstream test will fail for reasons unrelated to your bug fix\. 5\. If anything fails, go back and refine your fix\{yamlblock\}Remember: \- Work in the /testbed directory \- Every response MUST include at least one bash tool call

Figure 7:Diff of theverify\_fixstep before and after refinement\.
## Appendix DExamples of Lean Verification System

This section demonstrates one representative workflow in SWE task to demonstrate the Lean verification in detail\.

### D\.1Original YAML workflow

The original YAML workflow for the SWE task is as follows:

name:"swe\_agent"

goal:"GivenaGitHubissue,reproduceitandfixitbyproducingaminimalgitpatch"

\\parsystem\_prompt:\|

Youareahelpfulassistantwhocaninteractmultipletimeswithacomputershelltosolveprogrammingtasks\.

STRICTFORMATRULES:

\-YourresponsemustcontainATMOSTonecodeblock\.

\-Ifyouincludemorethanonecodeblock,yourresponsewillbeREJECTED\.

\-ThecodeblockmustcontainONEcommand\(orcommandsconnectedwith&&or\|\|\)\.

\-Thecodeblockmustbeeitherabashblock\(rawshellcommand\)orasubagentblock\(subagentnameasthefencelanguage\)\.

\-Ifyouhavenothingtoexecute,respondwithplaintextandNOcodeblock\.

IncludeaTHOUGHTsectionbeforeyourcommandwhereyouexplainyourreasoningprocess\.

<format\_example\>

THOUGHT:Youshouldfirstconsiderthetaskgoal,yourcurrentstate,andplanforyourfutureactions\.Thentelltheuserwhetheryouwanttorunabashcommandorcallasubagenttohelpwithataskandexplainindepthwhyorwhynot\.

\\parconfig:

model:"$\{MODEL\_NAME\}"

temperature:1\.0

model\_kwargs:

reasoning\_effort:"high"

max\_tool\_calls\_per\_step:20

expose\_submodules\_as\_tools:false

enable\_inline\_tool\_calls:true

\\parparameters:

code\_path:"$\{CODE\_PATH:\-/workspace/tmp/repo\}"

problem\_statement:"$\{PROBLEM\_STATEMENT\}"

regression\_test\_cmd:""

\\parworkflow:

\#==========================================

\#PHASE1:Exploreandunderstandtheissue

\#==========================================

\-step:

name:"explore\_repository"

instruction:\|

<pr\_description\>

ConsiderthefollowingPRdescription:

\{\{problem\_statement\}\}

</pr\_description\>

\\parYou’reasoftwareengineerinteractingcontinuouslywithacomputerbysubmittingcommands\.

You’llbehelpingimplementnecessarychangestomeetrequirementsinthePRdescription\.

Yourtaskisspecificallytomakechangestonon\-testfilesinthecurrentdirectoryinordertofixtheissuedescribedinthePRdescriptioninawaythatisgeneralandconsistentwiththecodebase\.

<IMPORTANT\>ThisisaninteractiveprocesswhereyouwillthinkandissueATLEASTONEcommandforeverystep,seetheresult,thenthinkandissueyournextcommand\(s\)\.</IMPORTANT\>

Foreachresponse:

1\.IncludeaTHOUGHTsectionexplainingyourreasoningandwhatyou’retryingtoaccomplish

2\.Provideoneormorebashtoolcallstoexecute

\\par<boundaries\>

\-MODIFY:Regularsourcecodefilesin/testbed\(thisistheworkingdirectoryforallyoursubsequentcommands\)

\-DONOTMODIFY:Tests,configurationfiles\(pyproject\.toml,setup\.cfg,etc\.\)

</boundaries\>

\\par<environment\_info\>

\-YouhaveafullLinuxshellenvironment

\-Alwaysusenon\-interactiveflags\(\-y,\-f\)forcommands

\-Avoidinteractivetoolslikevi,nano,oranythatrequireuserinput

\-Youcanusebashcommandsorinvokeanytoolthatisavailableintheenvironment

\-Youcanalsocreatenewtoolsorscriptstohelpyouwiththetask

\-Ifatoolisn’tavailable,youcanalsoinstallit

</environment\_info\>

\\par<execution\_rules\>

Youareoperatinginanenvironmentwhere

1\.Youissueatleastonecommand

3\.Thesystemexecutesthecommand\(s\)inasubshell

4\.Youseetheresult\(s\)

5\.Youwriteyournextcommand\(s\)

Eachresponseshouldinclude:

1\.\*\*Reasoningtext\*\*whereyouexplainyouranalysisandplan

2\.Atleastonetoolcallwithyourcommand

\*\*CRITICALREQUIREMENTS:\*\*

\-YourresponseSHOULDincludereasoningtextexplainingwhatyou’redoing

\-YourresponseMUSTincludeATLEASTONEbashtoolcall\.YoucanmakeMULTIPLEtoolcallsinasingleresponsewhenthecommandsareindependent\(e\.g\.,searchingmultiplefiles,readingdifferentpartsofthecodebase\)\.

\-Directoryorenvironmentvariablechangesarenotpersistent\.Everyactionisexecutedinanewsubshell\.

\-However,youcanprefixanyactionwith‘MY\_ENV\_VAR=MY\_VALUEcd/path/to/working/dir&&…‘orwrite/loadenvironmentvariablesfromfiles

ExampleofaCORRECTresponse:

<example\_response\>

IneedtounderstandtheBuilder\-relatedcode\.Letmefindrelevantfilesandchecktheprojectstructure\.

\[Makesmultiplebashtoolcalls:\{"command":"ls\-la"\},\{"command":"findsrc\-name’\*\.java’\|grep\-ibuilder"\},\{"command":"catREADME\.md\|head\-50"\}\]

</example\_response\>

</execution\_rules\>

\\parNowbegin\.Startbyexploringtherepositorystructureat/testbedtounderstandthecodebase,focusingonfilesanddirectoriesmostrelevanttotheissuedescribedinthePRdescription\.

\\par\#==========================================

\#PHASE2:Reproducetheissue

\#==========================================

\-step:

name:"reproduce\_issue"

instruction:\|

Nowthatyou’veexploredtherepository,createascripttoreproducetheissuedescribedinthePRdescription\.

\\parSteps:

1\.BasedonthePRdescriptionandthecodeyou’veread,writeasmallreproductionscript\(e\.g\./testbed/reproduce\_issue\.pyor/testbed/reproduce\_issue\.sh\)thatdemonstratesthebugorfailure\.

2\.Runthescriptandconfirmtheissueisreproducible\.Showtheerroroutput\.

3\.Iftheissueisnotdirectlyreproduciblewithasimplescript\(e\.g\.,it’sabehavioralorlogicerror\),explainwhatyouobserveandhowitdiffersfromexpectedbehavior\.

\\parRemember:

\-Workinthe/testbeddirectory

\-Usenon\-interactivecommandsonly

\-EveryresponseMUSTincludeatleastonebashtoolcall

\\par\#==========================================

\#PHASE3:Locateandfixthesourcecode

\#==========================================

\-step:

name:"fix\_issue"

instruction:\|

Nowthatyou’vereproducedtheissue,locatetherelevantsourcecodeandimplementafix\.

\\parSteps:

1\.Identifytheexactsourcefilesandfunctionsthatneedtobechanged

2\.Understandtherootcauseoftheissuebyreadingtherelevantcodecarefully

3\.Implementafixthat:

\-Addressestherootcause,notjustthesymptoms

\-Isconsistentwiththeexistingcodebasestyleandpatterns

\-Isgeneralenoughtohandleedgecases

\-DoesNOTmodifyanytestfilesorconfigurationfiles\(pyproject\.toml,setup\.cfg,etc\.\)

4\.Usesed,pythonscripts,orheredocstomaketheedits—doNOTuseinteractiveeditors

\\parRemember:

\-Workinthe/testbeddirectory

\-EveryresponseMUSTincludeatleastonebashtoolcall

\-ONLYmodifyregularsourcecodefiles

\\par\#==========================================

\#PHASE4:Verifythefix

\#==========================================

\-step:

name:"verify\_fix"

instruction:\|

Nowverifythatyourfixresolvestheissue\.

\\parSteps:

1\.Re\-runthereproductionscriptyoucreatedearliertoconfirmtheissueisfixed

2\.Ifthereisaregressiontestcommandavailable,runit:\{\{regression\_test\_cmd\}\}

3\.Testedgecasestoensureyourfixisrobustanddoesn’tbreakotherfunctionality

4\.Ifanythingfails,gobackandrefineyourfix

\\parRemember:

\-Workinthe/testbeddirectory

\-EveryresponseMUSTincludeatleastonebashtoolcall

\\par\#==========================================

\#PHASE5:Submitthepatch

\#==========================================

\-step:

name:"create\_patch"

instruction:\|

Yourfixisverified\.Nowcreateandsubmitthefinalpatch\.

\\parFollowthesestepsINORDER,withSEPARATEcommands:

\\parStep1:Createthepatchfile

Run‘cd/testbed&&gitdiff–path/to/file1path/to/file2\>patch\.txt‘listingonlythesourcefilesyoumodified\.

DoNOTcommityourchanges\.

<IMPORTANT\>

Thepatchmustonlycontainchangestothespecificsourcefilesyoumodifiedtofixtheissue\.

Donotsubmitfilecreationsorchangestoanyofthefollowingfiles:

\-testandreproductionfiles

\-helperscripts,tests,ortoolsthatyoucreated

\-installation,build,packaging,configuration,orsetupscriptsunlesstheyaredirectlypartoftheissueyouwerefixing\(youcanassumethattheenvironmentisalreadysetupforyourclient\)

\-binaryorcompiledfiles

</IMPORTANT\>

\\parStep2:Verifyyourpatch

Inspectpatch\.txttoconfirmitonlycontainsyourintendedchangesandheadersshow‘—a/‘and‘\+\+\+b/‘paths\.

\\parStep3:Submit\(EXACTcommandrequired\)

YouMUSTusethisEXACTcommandtosubmit:

“‘bash

echoCOMPLETE\_TASK\_AND\_SUBMIT\_FINAL\_OUTPUT&&catpatch\.txt

“‘

Ifthecommandfails\(nonzeroexitstatus\),itwillnotsubmit\.

\\par<CRITICAL\>

\-Creating/viewingthepatchandsubmittingitMUSTbeseparatecommands\(notcombinedwith&&\)\.

\-Ifyoumodifypatch\.txtafterverifying,youSHOULDverifyagainbeforesubmitting\.

\-YouCANNOTcontinueworking\(reading,editing,testing\)inanywayonthistaskaftersubmitting\.

\-Unlessyouthinkthetaskisfinishedandreadyforsubmission,youMUSTcontainatool\-callineveryresponse\.Whenyoumakenotoolcall,itwillbetreatedasasignalthatyouhavealreadycompletedthetaskandsubmittedyouranswer,andthesystemwillstopyoufrommakinganyfurthertoolcalls\.

</CRITICAL\>

\\par

### D\.2Layer\-1 and 2 Lean file and its running results

The transformed Lean file for layer\-1 and layer\-2 verification is as follows:

importLean

importMathlib

importAgentVerifier\.StaticLayer

importAgentVerifier\.StaticSemanticLayer\.StaticSemanticLayer

importAgentVerifier\.StaticSemanticLayer\.WorkflowQualityAnalysis\.GraphLevelPredicates

\\parnamespaceAgenticKernel

\\par–NodeIDs

defgood\_plan\_1\_v2\_nodeId0:NodeId:=⟨0⟩

…

\\par–Node0:step"explore\_repository"

defgood\_plan\_1\_v2\_node0:WorkflowNode:=\{

id:=good\_plan\_1\_v2\_nodeId0,name:=some"explore\_repository"

stepType:=\.step

reads:=\[⟨"problem\_statement",\.TString⟩\],writes:=\[\]

llmInstruction:=some"…"

\}

\\par–SemanticNode0:step"explore\_repository"

defgood\_plan\_1\_v2\_semNode0:SemanticWorkflowNode:=\{

baseNode:=good\_plan\_1\_v2\_node0

precondVariables:=\[varIsValidTool"shell\_run",varIsNonEmptyString"problem\_statement"\]

postcondVariables:=\[markStepExploratorygood\_plan\_1\_v2\_nodeId0,markSubGoalContributiongood\_plan\_1\_v2\_nodeId0"repository\_explored",markImplicitRetrygood\_plan\_1\_v2\_nodeId0"repository\_explored",varIsNonEmptyString"repository\_understanding"\]

\}

\\par–Node1:step"reproduce\_issue"

defgood\_plan\_1\_v2\_node1:WorkflowNode:=\{

id:=good\_plan\_1\_v2\_nodeId1,name:=some"reproduce\_issue"

stepType:=\.step

reads:=\[\],writes:=\[\]

llmInstruction:=some"…"

\}

\\par–SemanticNode1:step"reproduce\_issue"

defgood\_plan\_1\_v2\_semNode1:SemanticWorkflowNode:=\{

baseNode:=good\_plan\_1\_v2\_node1

precondVariables:=\[varIsValidTool"shell\_run",varIsNonEmptyString"repository\_understanding"\]

postcondVariables:=\[markStepTransformativegood\_plan\_1\_v2\_nodeId1,markSubGoalContributiongood\_plan\_1\_v2\_nodeId1"issue\_reproduced",markImplicitRetrygood\_plan\_1\_v2\_nodeId1"issue\_reproduced",varIsNonEmptyString"reproduction\_evidence"\]

\}

\\par–Node2:step"fix\_issue"

defgood\_plan\_1\_v2\_node2:WorkflowNode:=\{

id:=good\_plan\_1\_v2\_nodeId2,name:=some"fix\_issue"

stepType:=\.step

reads:=\[\],writes:=\[\]

llmInstruction:=some"…"

\}

\\par–SemanticNode2:step"fix\_issue"

defgood\_plan\_1\_v2\_semNode2:SemanticWorkflowNode:=\{

baseNode:=good\_plan\_1\_v2\_node2

precondVariables:=\[varIsValidTool"shell\_run",varIsNonEmptyString"reproduction\_evidence",varIsNonEmptyString"repository\_understanding"\]

postcondVariables:=\[markStepTransformativegood\_plan\_1\_v2\_nodeId2,markSubGoalContributiongood\_plan\_1\_v2\_nodeId2"fix\_implemented",markImplicitRetrygood\_plan\_1\_v2\_nodeId2"fix\_implemented",varIsNonEmptyString"fix\_implementation\_evidence"\]

\}

\\par–Node3:step"verify\_fix"

defgood\_plan\_1\_v2\_node3:WorkflowNode:=\{

id:=good\_plan\_1\_v2\_nodeId3,name:=some"verify\_fix"

stepType:=\.step

reads:=\[⟨"regression\_test\_cmd",\.TString⟩\],writes:=\[\]

llmInstruction:=some"…"

\}

\\par–SemanticNode3:step"verify\_fix"

defgood\_plan\_1\_v2\_semNode3:SemanticWorkflowNode:=\{

baseNode:=good\_plan\_1\_v2\_node3

precondVariables:=\[varIsValidTool"shell\_run",varNameExists"regression\_test\_cmd",varIsNonEmptyString"fix\_implementation\_evidence",varIsNonEmptyString"reproduction\_evidence"\]

postcondVariables:=\[markStepVerificatorygood\_plan\_1\_v2\_nodeId3,markSubGoalContributiongood\_plan\_1\_v2\_nodeId3"fix\_verified",markSubGoalVerificationgood\_plan\_1\_v2\_nodeId3"fix\_implemented",markImplicitRetrygood\_plan\_1\_v2\_nodeId3"fix\_verified",varIsNonEmptyString"fix\_verification\_evidence"\]

\}

\\par–Node4:step"create\_patch"

defgood\_plan\_1\_v2\_node4:WorkflowNode:=\{

id:=good\_plan\_1\_v2\_nodeId4,name:=some"create\_patch"

stepType:=\.step

reads:=\[\],writes:=\[\]

llmInstruction:=some"…"

\}

\\par–SemanticNode4:step"create\_patch"

defgood\_plan\_1\_v2\_semNode4:SemanticWorkflowNode:=\{

baseNode:=good\_plan\_1\_v2\_node4

precondVariables:=\[varIsValidTool"shell\_run",varIsNonEmptyString"fix\_implementation\_evidence"\]

postcondVariables:=\[markStepTransformativegood\_plan\_1\_v2\_nodeId4,markSubGoalContributiongood\_plan\_1\_v2\_nodeId4"patch\_submitted",markImplicitRetrygood\_plan\_1\_v2\_nodeId4"patch\_submitted",varIsNonEmptyString"patch\_submission\_evidence"\]

\}

\\pardefgood\_plan\_1\_v2Graph:WorkflowGraph:=\{

nodes:=\[good\_plan\_1\_v2\_node0,good\_plan\_1\_v2\_node1,good\_plan\_1\_v2\_node2,good\_plan\_1\_v2\_node3,good\_plan\_1\_v2\_node4\]

edges:=\[

\.seqEdgegood\_plan\_1\_v2\_nodeId0good\_plan\_1\_v2\_nodeId1,

\.seqEdgegood\_plan\_1\_v2\_nodeId1good\_plan\_1\_v2\_nodeId2,

\.seqEdgegood\_plan\_1\_v2\_nodeId2good\_plan\_1\_v2\_nodeId3,

\.seqEdgegood\_plan\_1\_v2\_nodeId3good\_plan\_1\_v2\_nodeId4

\]

entry:=good\_plan\_1\_v2\_nodeId0

exits:=\[good\_plan\_1\_v2\_nodeId4\]

parameters:=\[⟨"code\_path",\.TString⟩,⟨"problem\_statement",\.TString⟩,⟨"regression\_test\_cmd",\.TString⟩\]

\}

\\par/–Othernodesaredefinedinsimilarmanner\-/

\\par/\-

========================================================================

PER\-NODESTRUCTURALDIAGNOSTICS

========================================================================

\-/

\\par\#evaldo

letg:=good\_plan\_1\_v2Graph

fornodeing\.nodesdo

letname:=node\.name\.getD"\(unnamed\)"

IO\.printlns\!"\\n—Node\{node\.id\}:\\"\{name\}\\"\[\{reprnode\.stepType\}\]—"

IO\.printlns\!"writesConsistent:\{node\.writesConsistent\}"

IO\.printlns\!"reachableFromEntry:\{g\.reachableg\.entrynode\.id\}"

forrvinnode\.readsdo

letfromParam:=g\.parameters\.any\(funp=\>

p\.name==rv\.name&&p\.type\.compatiblerv\.type\)

letfromPred:=g\.nodes\.any\(funo=\>

o\.id\!=node\.id&&g\.reachableo\.idnode\.id&&

\(\!g\.isParallelScopedNodeo\.id\|\|g\.isParallelScopedNodenode\.id\)&&

o\.writes\.any\(funw=\>w\.name==rv\.name&&w\.type\.compatiblerv\.type\)\)

letstatus:=iffromParam\|\|fromPredthen"✓"else"✗UNRESOLVED"

IO\.printlns\!"read\\"\{rv\.name\}\\"\(\{reprrv\.type\}\):\{status\}"

forwvinnode\.writesdo

IO\.printlns\!"write\\"\{wv\.name\}\\"\(\{reprwv\.type\}\)"

\\par/\-

========================================================================

GRAPH\-LEVELSTRUCTURALCHECKS

========================================================================

\-/

\\par\#evalgood\_plan\_1\_v2Graph\.allWritesConsistent

\#evalgood\_plan\_1\_v2Graph\.allReadResolvable

\#evalgood\_plan\_1\_v2Graph\.edgesValid

\#evalgood\_plan\_1\_v2Graph\.entryNodeValid

\#evalgood\_plan\_1\_v2Graph\.exitNodesValid

\#evalgood\_plan\_1\_v2Graph\.allExitsReachable

\#evalgood\_plan\_1\_v2Graph\.noOrphanNodes

\#evalgood\_plan\_1\_v2Graph\.returnType

\\par/\-

========================================================================

THEOREMS

========================================================================

\-/

\\partheoremgood\_plan\_1\_v2\_writesConsistent:good\_plan\_1\_v2Graph\.allWritesConsistent=true:=bynative\_decide

theoremgood\_plan\_1\_v2\_readsResolvable:good\_plan\_1\_v2Graph\.allReadResolvable=true:=bynative\_decide

theoremgood\_plan\_1\_v2\_edgesValid:good\_plan\_1\_v2Graph\.edgesValid=true:=bynative\_decide

theoremgood\_plan\_1\_v2\_entryValid:good\_plan\_1\_v2Graph\.entryNodeValid=true:=bynative\_decide

theoremgood\_plan\_1\_v2\_exitsValid:good\_plan\_1\_v2Graph\.exitNodesValid=true:=bynative\_decide

theoremgood\_plan\_1\_v2\_exitsReachable:good\_plan\_1\_v2Graph\.allExitsReachable=true:=bynative\_decide

theoremgood\_plan\_1\_v2\_noOrphans:good\_plan\_1\_v2Graph\.noOrphanNodes=true:=bynative\_decide

\\partheoremgood\_plan\_1\_v2\_seqPath\_typeChecks:

∃ctx,typeCheckSequence\[good\_plan\_1\_v2\_node0,good\_plan\_1\_v2\_node1,good\_plan\_1\_v2\_node2,good\_plan\_1\_v2\_node3,good\_plan\_1\_v2\_node4\]\[⟨"code\_path",\.TString⟩,⟨"problem\_statement",\.TString⟩,⟨"regression\_test\_cmd",\.TString⟩\]=\.okctx:=byexact⟨\_,rfl⟩

\\partheoremgood\_plan\_1\_v2\_specCount:good\_plan\_1\_v2Graph\.nodesNeedingSpecs\.length=5:=bynative\_decide

\\par\\par/\-

========================================================================

SEMANTICVERIFICATION

========================================================================

\-/

\\pardefgood\_plan\_1\_v2\_paramNode:SemanticWorkflowNode:=\{

baseNode:=\{id:=⟨20041122⟩,name:=some"parameters",stepType:=\.setVariable,reads:=\[\],writes:=\[\],llmInstruction:=none\}

precondVariables:=\[\]

postcondVariables:=\[

varNameExists"code\_path",

varNameExists"problem\_statement",

varNameExists"regression\_test\_cmd",

varIsValidFilePath"code\_path",

varIsNonEmptyString"problem\_statement",

varIsValidTool"shell\_run"

\]

\}

\\pardefgood\_plan\_1\_v2SemanticGraph:SemanticWorkflowGraph:=\{

baseGraph:=good\_plan\_1\_v2Graph

paramNode:=good\_plan\_1\_v2\_paramNode

semanticNodes:=\[good\_plan\_1\_v2\_semNode0,good\_plan\_1\_v2\_semNode1,good\_plan\_1\_v2\_semNode2,good\_plan\_1\_v2\_semNode3,good\_plan\_1\_v2\_semNode4\]

loopNodes:=\[\]

conditionalNodes:=\[\]

specInvariant:=bydecide

\}

\\par/\-

========================================================================

SEMANTICSTATESPACEAFTEREACHNODE

========================================================================

\-/

\\par\#evaldo

letsemNodes:=good\_plan\_1\_v2SemanticGraph\.semanticNodes

letparamPost:=good\_plan\_1\_v2SemanticGraph\.paramNode\.postcondVariables

IO\.println"\\n============================================================"

IO\.println"SEMANTICSTATESPACETRACE"

IO\.println"============================================================"

IO\.println"\\n—InitialState\(fromparameters\)—"

forpinparamPostdo

IO\.printlns\!"✓\{p\}"

letmutstate:ListVariablePredicateRequirement:=paramPost

fornodeinsemNodesdo

letname:=node\.baseNode\.name\.getD"\(unnamed\)"

letnodeId:=node\.baseNode\.id

IO\.printlns\!"\\n—AfterNode\{nodeId\}:\\"\{name\}\\"—"

–Checkpreconditionsagainstcurrentstate

IO\.println"Preconditions:"

forpinnode\.precondVariablesdo

letsatisfied:=state\.any\(funs=\>s\.satisfiesp\)

letmark:=ifsatisfiedthen"✓"else"✗"

IO\.printlns\!"\{mark\}requires:\{p\}"

–Shownewfactsestablished

IO\.println"Postconditions\(newfacts\):"

forpinnode\.postcondVariablesdo

IO\.printlns\!"\+establishes:\{p\}"

–Updatecumulativestate:addnewpostconditions

forpinnode\.postcondVariablesdo

unlessstate\.any\(funs=\>s==p\)do

state:=state\+\+\[p\]

IO\.printlns\!"CumulativeState\(\{state\.length\}predicates\):"

forpinstatedo

IO\.printlns\!"\{p\}"

IO\.printlns\!"\\n============================================================"

IO\.printlns\!"Finalstate:\{state\.length\}predicatesestablished"

IO\.println"============================================================"

\\par/\-

========================================================================

SEMANTICVERIFICATION

========================================================================

\-/

\\par\#eval\!do

letresult:=good\_plan\_1\_v2SemanticGraph\.verifyemptyRegistry

IO\.println\(describeGraphVerificationResultresult\)

\\partheoremgood\_plan\_1\_v2\_semantically\_sound:

good\_plan\_1\_v2SemanticGraph\.isSemanticallySoundBoolemptyRegistry=true:=by

native\_decide

\\par/\-

========================================================================

GRAPH\-LEVELWORKFLOWQUALITYANALYSIS

========================================================================

\-/

\\pardefgood\_plan\_1\_v2\_goalSpec:GoalSpecification:=\{

originalGoal:="GivenaGitHubissue,reproduceitandfixitbyproducingaminimalgitpatch"

subGoals:=\[

\{name:="repository\_explored"

variableName:="repository\_understanding"

requiredPredicate:=\.isNonEmptyString

description:="EvidencethattherepositorystructurewasexploredandrelevantsourcefileswereidentifiedbasedontheGitHubissue\."

requiredGraphPredicates:=\[GraphLevelPredicateKeys\.pathCoverage\]\},

\{name:="issue\_reproduced"

variableName:="reproduction\_evidence"

requiredPredicate:=\.isNonEmptyString

description:="Evidencethatareproductionscriptwascreatedandthebugwasreproduced\.ContextcontinuityPASSESbecausestepchainprovidesconversationhistory\."

requiredGraphPredicates:=\[GraphLevelPredicateKeys\.pathCoverage,GraphLevelPredicateKeys\.contextContinuity\]\},

\{name:="fix\_implemented"

variableName:="fix\_implementation\_evidence"

requiredPredicate:=\.isNonEmptyString

description:="Evidencethatsourcecodewasmodifiedtofixtheissue\.Contextflowsviastepchain\.unifiedLoopBackPASSESduetomarkImplicitRetryonstepnodes\."

requiredGraphPredicates:=\[GraphLevelPredicateKeys\.pathCoverage,GraphLevelPredicateKeys\.contextContinuity,GraphLevelPredicateKeys\.informationSufficiency,GraphLevelPredicateKeys\.unifiedLoopBack,GraphLevelPredicateKeys\.verificationCoverage\]\},

\{name:="fix\_verified"

variableName:="fix\_verification\_evidence"

requiredPredicate:=\.isNonEmptyString

description:="Evidencethatthefixwasverifiedbyrerunningreproductionandregressiontests\.ContextcontinuityPASSESviastepchain\."

requiredGraphPredicates:=\[GraphLevelPredicateKeys\.pathCoverage,GraphLevelPredicateKeys\.contextContinuity\]\},

\{name:="patch\_submitted"

variableName:="patch\_submission\_evidence"

requiredPredicate:=\.isNonEmptyString

description:="Evidencethatagitpatchwascreatedandsubmitted\.Contextflowsviastepchainbutnofail\-safeexists\."

requiredGraphPredicates:=\[GraphLevelPredicateKeys\.pathCoverage,GraphLevelPredicateKeys\.contextContinuity,GraphLevelPredicateKeys\.failSafe\]\}

\]

\}

\\par\#evaldo

letreport:=analyzeGoalCoveragegood\_plan\_1\_v2SemanticGraphgood\_plan\_1\_v2\_goalSpec

IO\.println\(formatGoalCoverageReportreport\)

\\par\\parendAgenticKernel

## Appendix ELimitations

Despite the promising results, several limitations remain\. First, although theLean4Agentaims to verify the full agent execution cycle, black\-box LLM behavior cannot be fully inspected\. Our framework instead decomposes agent behavior into structured steps and abstracts natural\-language requirements into checkable predicates, thereby leaving some semantic ambiguity outside the formal system\. Second, because workflows are complex and tasks are numerous, the predicate annotations used in our experiments are generated by LLMs\. This may introduce mis\-specified predicates or annotation errors, even though the resulting Lean checks are formal\. Third, modern LLMs often generate workflows with few structural mistakes or explicit variable mismatches, making it difficult to quantitatively evaluate some components beyond targeted case studies\.

## Appendix FExperiment Costs

For large models, including GPT\-5\.2, GLM\-5, Kimi\-K2\.5, and Claude, the experiments are conducted through their official API calls; the costs for the experiments are around $4,000\. For small models, including Qwen\-3\.5\-27B and Gemma\-4\-31B, we run them on 4xGH200 VLLMKwon et al\. \[[2023](https://arxiv.org/html/2606.06523#bib.bib12)\]GPUs; the experiments cost around 1,500 GPU hours\.

## Appendix GBroader Impacts

This paper contributes to society by providing a more reliable foundation for the LLM agent systems\. However, it also has the potential to be used in reverse to cause harmful effects using LLM systems\.

## NeurIPS Paper Checklist

1. 1\.Claims
2. Question: Do the main claims made in the abstract and introduction accurately reflect the paper’s contributions and scope?
3. Answer:\[Yes\]
4. Justification: The claims in the abstract and introduction are detailed and explained by the following sections\.
5. Guidelines: - •The answer\[N/A\]means that the abstract and introduction do not include the claims made in the paper\. - •The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations\. A\[No\]or\[N/A\]answer to this question will not be perceived well by the reviewers\. - •The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings\. - •It is fine to include aspirational goals as motivation as long as it is clear that these goals are not attained by the paper\.
6. 2\.Limitations
7. Question: Does the paper discuss the limitations of the work performed by the authors?
8. Answer:\[Yes\]
9. Justification: The limitation is discussed in Appendix[E](https://arxiv.org/html/2606.06523#A5)
10. Guidelines: - •The answer\[N/A\]means that the paper has no limitation while the answer\[No\]means that the paper has limitations, but those are not discussed in the paper\. - •The authors are encouraged to create a separate “Limitations” section in their paper\. - •The paper should point out any strong assumptions and how robust the results are to violations of these assumptions \(e\.g\., independence assumptions, noiseless settings, model well\-specification, asymptotic approximations only holding locally\)\. The authors should reflect on how these assumptions might be violated in practice and what the implications would be\. - •The authors should reflect on the scope of the claims made, e\.g\., if the approach was only tested on a few datasets or with a few runs\. In general, empirical results often depend on implicit assumptions, which should be articulated\. - •The authors should reflect on the factors that influence the performance of the approach\. For example, a facial recognition algorithm may perform poorly when image resolution is low or images are taken in low lighting\. Or a speech\-to\-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon\. - •The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size\. - •If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness\. - •While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren’t acknowledged in the paper\. The authors should use their best judgment and recognize that individual actions in favor of transparency play an important role in developing norms that preserve the integrity of the community\. Reviewers will be specifically instructed to not penalize honesty concerning limitations\.
11. 3\.Theory assumptions and proofs
12. Question: For each theoretical result, does the paper provide the full set of assumptions and a complete \(and correct\) proof?
13. Answer:\[N/A\]
14. Justification: We don’t have theoretical results
15. Guidelines: - •The answer\[N/A\]means that the paper does not include theoretical results\. - •All the theorems, formulas, and proofs in the paper should be numbered and cross\-referenced\. - •All assumptions should be clearly stated or referenced in the statement of any theorems\. - •The proofs can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged to provide a short proof sketch to provide intuition\. - •Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material\. - •Theorems and Lemmas that the proof relies upon should be properly referenced\.
16. 4\.Experimental result reproducibility
17. Question: Does the paper fully disclose all the information needed to reproduce the main experimental results of the paper to the extent that it affects the main claims and/or conclusions of the paper \(regardless of whether the code and data are provided or not\)?
18. Answer:\[Yes\]
19. Justification: We provide information to reproduce our experiments in the methodology and experiment section
20. Guidelines: - •The answer\[N/A\]means that the paper does not include experiments\. - •If the paper includes experiments, a\[No\]answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not\. - •If the contribution is a dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable\. - •Depending on the contribution, reproducibility can be accomplished in various ways\. For example, if the contribution is a novel architecture, describing the architecture fully might suffice, or if the contribution is a specific model and empirical evaluation, it may be necessary to either make it possible for others to replicate the model with the same dataset, or provide access to the model\. In general\. releasing code and data is often one good way to accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model \(e\.g\., in the case of a large language model\), releasing of a model checkpoint, or other means that are appropriate to the research performed\. - •While NeurIPS does not require releasing code, the conference does require all submissions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution\. For example 1. \(a\)If the contribution is primarily a new algorithm, the paper should make it clear how to reproduce that algorithm\. 2. \(b\)If the contribution is primarily a new model architecture, the paper should describe the architecture clearly and fully\. 3. \(c\)If the contribution is a new model \(e\.g\., a large language model\), then there should either be a way to access this model for reproducing the results or a way to reproduce the model \(e\.g\., with an open\-source dataset or instructions for how to construct the dataset\)\. 4. \(d\)We recognize that reproducibility may be tricky in some cases, in which case authors are welcome to describe the particular way they provide for reproducibility\. In the case of closed\-source models, it may be that access to the model is limited in some way \(e\.g\., to registered users\), but it should be possible for other researchers to have some path to reproducing or verifying the results\.
21. 5\.Open access to data and code
22. Question: Does the paper provide open access to the data and code, with sufficient instructions to faithfully reproduce the main experimental results, as described in supplemental material?
23. Answer:\[No\]
24. Justification: We will open\-source the code in the near future, but not with the submission\.
25. Guidelines: - •The answer\[N/A\]means that paper does not include experiments requiring code\. - • - •While we encourage the release of code and data, we understand that this might not be possible, so\[No\]is an acceptable answer\. Papers cannot be rejected simply for not including code, unless this is central to the contribution \(e\.g\., for a new open\-source benchmark\)\. - •The instructions should contain the exact command and environment needed to run to reproduce the results\. See the NeurIPS code and data submission guidelines \([https://neurips\.cc/public/guides/CodeSubmissionPolicy](https://neurips.cc/public/guides/CodeSubmissionPolicy)\) for more details\. - •The authors should provide instructions on data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc\. - •The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines\. If only a subset of experiments are reproducible, they should state which ones are omitted from the script and why\. - •At submission time, to preserve anonymity, the authors should release anonymized versions \(if applicable\)\. - •Providing as much information as possible in supplemental material \(appended to the paper\) is recommended, but including URLs to data and code is permitted\.
26. 6\.Experimental setting/details
27. Question: Does the paper specify all the training and test details \(e\.g\., data splits, hyperparameters, how they were chosen, type of optimizer\) necessary to understand the results?
28. Answer:\[Yes\]
29. Justification: We provide the details of experiments in Section[3\.2](https://arxiv.org/html/2606.06523#S3.SS2)
30. Guidelines: - •The answer\[N/A\]means that the paper does not include experiments\. - •The experimental setting should be presented in the core of the paper to a level of detail that is necessary to appreciate the results and make sense of them\. - •The full details can be provided either with the code, in appendix, or as supplemental material\.
31. 7\.Experiment statistical significance
32. Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
33. Answer:\[Yes\]
34. Justification: We provide the details of 95% CI in Section[3\.3](https://arxiv.org/html/2606.06523#S3.SS3)and Appendix[A\.2](https://arxiv.org/html/2606.06523#A1.SS2)\.
35. Guidelines: - •The answer\[N/A\]means that the paper does not include experiments\. - •The authors should answer\[Yes\]if the results are accompanied by error bars, confidence intervals, or statistical significance tests, at least for the experiments that support the main claims of the paper\. - •The factors of variability that the error bars are capturing should be clearly stated \(for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions\)\. - •The method for calculating the error bars should be explained \(closed form formula, call to a library function, bootstrap, etc\.\) - •The assumptions made should be given \(e\.g\., Normally distributed errors\)\. - •It should be clear whether the error bar is the standard deviation or the standard error of the mean\. - •It is OK to report 1\-sigma error bars, but one should state it\. The authors should preferably report a 2\-sigma error bar than state that they have a 96% CI, if the hypothesis of Normality of errors is not verified\. - •For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that are out of range \(e\.g\., negative error rates\)\. - •If error bars are reported in tables or plots, the authors should explain in the text how they were calculated and reference the corresponding figures or tables in the text\.
36. 8\.Experiments compute resources
37. Question: For each experiment, does the paper provide sufficient information on the computer resources \(type of compute workers, memory, time of execution\) needed to reproduce the experiments?
38. Answer:\[Yes\]
39. Justification: We have provided the details of experiment costs in Appendix[F](https://arxiv.org/html/2606.06523#A6)\.
40. Guidelines: - •The answer\[N/A\]means that the paper does not include experiments\. - •The paper should indicate the type of compute workers CPU or GPU, internal cluster, or cloud provider, including relevant memory and storage\. - •The paper should provide the amount of compute required for each of the individual experimental runs as well as estimate the total compute\. - •The paper should disclose whether the full research project required more compute than the experiments reported in the paper \(e\.g\., preliminary or failed experiments that didn’t make it into the paper\)\.
41. 9\.Code of ethics
43. Answer:\[Yes\]
44. Justification: After the detailed evaluation of ethics guidelines, we consider that this paper follows the guidelines\.
45. Guidelines: - •The answer\[N/A\]means that the authors have not reviewed the NeurIPS Code of Ethics\. - •If the authors answer\[No\], they should explain the special circumstances that require a deviation from the Code of Ethics\. - •The authors should make sure to preserve anonymity \(e\.g\., if there is a special consideration due to laws or regulations in their jurisdiction\)\.
46. 10\.Broader impacts
47. Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
48. Answer:\[Yes\]
49. Justification: We discusses the broader impacts in Appendix[G](https://arxiv.org/html/2606.06523#A7)\.
50. Guidelines: - •The answer\[N/A\]means that there is no societal impact of the work performed\. - •If the authors answer\[N/A\]or\[No\], they should explain why their work has no societal impact or why the paper does not address societal impact\. - •Examples of negative societal impacts include potential malicious or unintended uses \(e\.g\., disinformation, generating fake profiles, surveillance\), fairness considerations \(e\.g\., deployment of technologies that could make decisions that unfairly impact specific groups\), privacy considerations, and security considerations\. - •The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments\. However, if there is a direct path to any negative applications, the authors should point it out\. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate Deepfakes for disinformation\. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster\. - •The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from \(intentional or unintentional\) misuse of the technology\. - •If there are negative societal impacts, the authors could also discuss possible mitigation strategies \(e\.g\., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of ML\)\.
51. 11\.Safeguards
52. Question: Does the paper describe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse \(e\.g\., pre\-trained language models, image generators, or scraped datasets\)?
53. Answer:\[N/A\]
54. Justification: Our paper poses no such risks\.
55. Guidelines: - •The answer\[N/A\]means that the paper poses no such risks\. - •Released models that have a high risk for misuse or dual\-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters\. - •Datasets that have been scraped from the Internet could pose safety risks\. The authors should describe how they avoided releasing unsafe images\. - •We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make a best faith effort\.
56. 12\.Licenses for existing assets
57. Question: Are the creators or original owners of assets \(e\.g\., code, data, models\), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
58. Answer:\[Yes\]
59. Justification: The usage of code, data, and models in the paper is properly credited, and the license terms are followed\.
60. Guidelines: - •The answer\[N/A\]means that the paper does not use existing assets\. - •The authors should cite the original paper that produced the code package or dataset\. - •The authors should state which version of the asset is used and, if possible, include a URL\. - •The name of the license \(e\.g\., CC\-BY 4\.0\) should be included for each asset\. - •For scraped data from a particular source \(e\.g\., website\), the copyright and terms of service of that source should be provided\. - •If assets are released, the license, copyright information, and terms of use in the package should be provided\. For popular datasets,[paperswithcode\.com/datasets](https://arxiv.org/html/2606.06523v1/paperswithcode.com/datasets)has curated licenses for some datasets\. Their licensing guide can help determine the license of a dataset\. - •For existing datasets that are re\-packaged, both the original license and the license of the derived asset \(if it has changed\) should be provided\. - •If this information is not available online, the authors are encouraged to reach out to the asset’s creators\.
61. 13\.New assets
62. Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
63. Answer:\[Yes\]
64. Justification: The library and evolution method presented are well documented and will be published alongside the assets\.
65. Guidelines: - •The answer\[N/A\]means that the paper does not release new assets\. - •Researchers should communicate the details of the dataset/code/model as part of their submissions via structured templates\. This includes details about training, license, limitations, etc\. - •The paper should discuss whether and how consent was obtained from people whose asset is used\. - •At submission time, remember to anonymize your assets \(if applicable\)\. You can either create an anonymized URL or include an anonymized zip file\.
66. 14\.Crowdsourcing and research with human subjects
67. Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well as details about compensation \(if any\)?
68. Answer:\[N/A\]
69. Justification: The paper does not involve crowdsourcing nor research with human subjects\.
70. Guidelines: - •The answer\[N/A\]means that the paper does not involve crowdsourcing nor research with human subjects\. - •Including this information in the supplemental material is fine, but if the main contribution of the paper involves human subjects, then as much detail as possible should be included in the main paper\. - •According to the NeurIPS Code of Ethics, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector\.
71. 15\.Institutional review board \(IRB\) approvals or equivalent for research with human subjects
72. Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board \(IRB\) approvals \(or an equivalent approval/review based on the requirements of your country or institution\) were obtained?
73. Answer:\[N/A\]
74. Justification: The paper does not involve crowdsourcing nor research with human subjects\.
75. Guidelines: - •The answer\[N/A\]means that the paper does not involve crowdsourcing nor research with human subjects\. - •Depending on the country in which research is conducted, IRB approval \(or equivalent\) may be required for any human subjects research\. If you obtained IRB approval, you should clearly state this in the paper\. - •We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurIPS Code of Ethics and the guidelines for their institution\. - •For initial submissions, do not include any information that would break anonymity \(if applicable\), such as the institution conducting the review\.
76. 16\.Declaration of LLM usage
77. Question: Does the paper describe the usage of LLMs if it is an important, original, or non\-standard component of the core methods in this research? Note that if the LLM is used only for writing, editing, or formatting purposes and does*not*impact the core methodology, scientific rigor, or originality of the research, a declaration is not required\.
78. Answer:\[N/A\]
79. Justification: The core method development in this research does not involve LLMs as any important, original, or non\-standard components\.
80. Guidelines: - •The answer\[N/A\]means that the core method development in this research does not involve LLMs as any important, original, or non\-standard components\. - •Please refer to our LLM policy in the NeurIPS handbook for what should or should not be described\.