Toward Safe LLM Agents: A Survey of Specification, Verification, and Enforcement

# Toward Safe LLM Agents: A Survey of Specification, Verification, and Enforcement
Source: [https://arxiv.org/html/2608.14590](https://arxiv.org/html/2608.14590)
Pierre Dantas The University of Manchester Manchester, UK pierre\.dantas@manchester\.ac\.uk &Lucas Cordeiro The University of Manchester Manchester, UK lucas\.cordeiro@manchester\.ac\.uk &Ehsan Nowroozi The University of Greenwich London, UK ehsan\.nowroozi65@ieee\.org &Tihanyi Norbert Technology Innovation Institute Abu Dhabi, UAE ntihanyi@inf\.elte\.hu

###### Abstract

Large Language Model \(LLM\)agents increasingly perform irreversible real\-world actions, including database updates, API calls, file operations, and autonomous use of tools\. However, no existing system provides formally grounded, task\-level safety guarantees for the plans these agents generate\. Research remains fragmented across specification, verification, and enforcement, limiting understanding of the strengths and limitations of existing approaches\. To address this gap, we conducted a PRISMA 2020 systematic review of 38 studies published between 2022 and 2026 and retrieved from six academic databases\. Our analysis reveals four key findings\. First, the specification bottleneck remains the primary challenge: natural\-language\-to\-formal translation achieves only24%to35%24\\text\{\\,\}\\mathrm\{\\char 37\\relax\}35\\text\{\\,\}\\mathrm\{\\char 37\\relax\}semantic correctness, undermining downstream verification\. Second, runtime monitoring is the most mature enforcement strategy, reducing unsafe actions by40%to65%40\\text\{\\,\}\\mathrm\{\\char 37\\relax\}65\\text\{\\,\}\\mathrm\{\\char 37\\relax\}in controlled settings, but it does not provide complete safety guarantees\. Third, the verifier tax shows that blocking94%94\\text\{\\,\}\\mathrm\{\\char 37\\relax\}of unsafe actions can still result in less than5%5\\text\{\\,\}\\mathrm\{\\char 37\\relax\}safe task completion because agents exploit alternative unsafe paths\. Finally, no existing approach simultaneously achieves soundness, scalability, semantic correctness, and task\-level safety preservation\. We contribute a three\-level taxonomy, a comparative analysis of existing techniques, a synthesis of evidence on the verifier tax, and a ten\-problem research agenda for trustworthy agenticArtificial Intelligence \(AI\)\.

*K*eywordsAgentic AI, formal verification, runtime monitoring, safety guarantees, model checking, specification languages

## 1Introduction

Large Language Model \(LLM\)agents – systems in which anLLMserves as a reasoning engine that selects and sequences tool calls, sub\-tasks, or robotic actions – have moved rapidly from research prototypes to production deployments\. They now operate in consequential settings including software engineering\[[39](https://arxiv.org/html/2608.14590#bib.bib49)\], healthcare\[[43](https://arxiv.org/html/2608.14590#bib.bib29)\], customer service\[[31](https://arxiv.org/html/2608.14590#bib.bib27)\], and autonomous driving\[[56](https://arxiv.org/html/2608.14590#bib.bib37)\]\. In each of these domains, an agent’s plan – the sequence of actions it commits to executing – can have irreversible real\-world effects: a misconfigured deployment, an erroneous medication recommendation, an unauthorized financial transaction, a collision\.

The fundamental safety challenge is thatLLMsgenerate plans through statistical pattern matching over training data, rather than through sound logical inference\. A plan that reads fluently and appears coherent may violate safety invariants, disregard temporal ordering constraints \(e\.g\., authentication must precede data access\), or produce cascading harmful effects that are individually plausible yet collectively catastrophic\. This survey empirically documents this gap:*none*of 16 popularLLMagents scored above60%60\\text\{\\,\}\\mathrm\{\\char 37\\relax\}on a structured safety benchmark spanning 2,000 test cases\[[63](https://arxiv.org/html/2608.14590#bib.bib47)\]\. Frontier models show limited robustness even to basic jailbreak attacks in multi\-step agentic settings\[[2](https://arxiv.org/html/2608.14590#bib.bib48)\]\.

ClassicalArtificial Intelligence \(AI\)planning as well as formal verification offer mathematically rigorous tools for guaranteeing plan correctness:Planning Domain Definition Language \(PDDL\)\-based planners, model checkers such asSimple Promela Interpreter \(SPIN\)andNew Symbolic Model Verifier \(NuSMV\), and deductive verifiers such as Dafny and Coq\. However, applying these tools toLLMagent outputs requires closing the gap between unstructuredNatural Language \(NL\)and formal mathematical structures – a non\-trivial translation problem that, in itself, introduces semantic errors\. The consequence is a*specification\-verification\-enforcement pipeline*forLLMagent plans that is fragile at every stage: specifications may be semantically incorrect\[[51](https://arxiv.org/html/2608.14590#bib.bib24)\], verification may operate over inaccurate formal models\[[46](https://arxiv.org/html/2608.14590#bib.bib26)\], and enforcement may block unsafe single actions while leaving task\-level safety unresolved\[[47](https://arxiv.org/html/2608.14590#bib.bib45)\]\.

This survey systematically maps the emerging literature that attempts to close this gap\. We cover the period 2022 to 2026, encompassing theLLM\-agent era from GPT\-3/4 onward, and identify 38 studies across the specification, verification, enforcement, and evaluation subfields using a PRISMA 2020 systematic review protocol\.

### 1\.1Problem Statement

We define the*formal validation problem forLLMagent plans*as follows\. Let𝒜\\mathcal\{A\}be anLLM\-based agent that, given a task descriptionttand an observation historyhh, generates a planπ=\(a1,a2,…,an\)\\pi=\(a\_\{1\},a\_\{2\},\\ldots,a\_\{n\}\)where eachaia\_\{i\}is an action \(tool call, sub\-task delegation, or physical action\)\. Letφ\\varphibe a safety property expressed in a formal systemℒ\\mathcal\{L\}\. The verification task is to determine whetherπ⊧φ\\pi\\models\\varphi– whether the plan satisfies the property – before, during, or after execution, and to enforce compliance when it does not, as illustrated in Figure[1](https://arxiv.org/html/2608.14590#S1.F1)\. This partition reveals three tightly coupled sub\-problems:

1. 1\.Specification:How isφ\\varphiacquired from human\-expressible requirements and represented inℒ\\mathcal\{L\}?
2. 2\.Verification:How isπ⊧φ\\pi\\models\\varphidetermined efficiently and soundly, given thatπ\\piis generated stochastically and may be open\-ended?
3. 3\.Enforcement:What action is taken whenπ⊧̸φ\\pi\\not\\models\\varphi, and does that action restore task\-level safety?

Each sub\-problem is independently difficult, and their composition introduces additional challenges that no single sub\-problem can resolve\.

![Refer to caption](https://arxiv.org/html/2608.14590v1/x1.png)Figure 1:The specification\-verification\-enforcement pipeline forLLMagent plans\. Given a task descriptiontt, an agent𝒜\\mathcal\{A\}generates a planπ\\pi\. The*specification*stage acquires a formal safety propertyφ\\varphifrom human requirements\. The*verification*stage checks whetherπ⊧φ\\pi\\models\\varphi\. The*enforcement*stage intervenes whenπ⊧̸φ\\pi\\not\\models\\varphi\. Each stage introduces independent sources of error; their composition is the central problem surveyed here\.
### 1\.2Scope and Inclusion Criteria

This survey covers:

1. 1\.LLM\-based agents \(single or multi\-agent\) that produce multi\-step plans, action sequences, or tool\-call chains\.
2. 2\.Studies that address at least one of: plan specification, plan verification, plan enforcement, or safety monitoring\.
3. 3\.Publications from 2022 to 2026, in English, across empirical, tool, survey, and position paper categories\.

We exclude pure chatbot safety \(without a planning component\), neural network verification applied to non\-agent settings, and works where theLLMis an incidentalNatural Language Processing \(NLP\)component in an otherwise classical system\.

### 1\.3Contributions

This survey makes the following contributions:

1. 1\.Systematic coverage\. To the best of our knowledge, we provide the first PRISMA 2020 systematic review of the specification\-verification\-enforcement pipeline forLLMagent plans, identifying and synthesizing 38 studies across six databases \(arXiv, ACM DL, IEEE Xplore, Semantic Scholar, Google Scholar, Preprints\.org\)\.
2. 2\.Unified taxonomy\. We introduce a three\-level taxonomy – paradigm, technique, system – that organizes all included works and enables direct comparison across approaches previously described in isolation \(Section[4](https://arxiv.org/html/2608.14590#S4)\)\.
3. 3\.Comparative study\. We provide a multidimensional comparison table that maps all 38 papers to formal notation, verification moment \(pre\-execution, runtime, post\-hoc\), enforcement type, task domain, tool availability, and evidence quality\[[24](https://arxiv.org/html/2608.14590#bib.bib17)\]\.
4. 4\.Empirical synthesis of the verifier tax\. We aggregate evidence from enforcement and benchmark studies to characterize the relationship between action\-level safety, task\-levelSafe Success Rate \(SSR\), and enforcement overhead – synthesizing the most consequential empirical finding in the corpus\[[47](https://arxiv.org/html/2608.14590#bib.bib45)\]\. This finding currently rests on a single study and requires independent replication; Section[6\.3](https://arxiv.org/html/2608.14590#S6.SS3)discusses itsGrading of Recommendations Assessment, Development and Evaluation \(GRADE\)certainty accordingly\.
5. 5\.Structured research agenda\. We identify ten open problems \(Section[5\.7](https://arxiv.org/html/2608.14590#S5.SS7)\) derived from gap analysis across all five thematic clusters, with explicit pointers to the most promising technical directions for each\.

### 1\.4Survey Organisation

We organize the remainder of this survey as follows\. Section[2](https://arxiv.org/html/2608.14590#S2)reviews formal methods andLLMagent architectures\. Section[3](https://arxiv.org/html/2608.14590#S3)details the PRISMA 2020 protocol, including eligibility criteria, search strings, the study selection flow diagram, and the data extraction procedure\. Section[4](https://arxiv.org/html/2608.14590#S4)presents the unified taxonomy\. Section[5](https://arxiv.org/html/2608.14590#S5)examines related work across five thematic clusters and highlights research gaps\. Section[6](https://arxiv.org/html/2608.14590#S6)offers a cross\-cutting synthesis, including the verifier tax analysis andGRADEcertainty assessment\. Section[7](https://arxiv.org/html/2608.14590#S7)outlines the research agenda for each gap\. Section[8](https://arxiv.org/html/2608.14590#S8)discusses implications, limitations, and open challenges\. Section[9](https://arxiv.org/html/2608.14590#S9)concludes the paper\.

## 2Background and Preliminaries

The verification techniques surveyed in this paper rest on a small set of formal foundations: temporal logic \(the language of safety properties\), model checking \(the decision procedure\), classical planning formalisms \(structured task representations\), andLLMagent architectures \(the target of verification\)\. Understanding these foundations explains why temporal logic dominates the specification literature, why model checking is the most common algorithmic backbone, and why the stochastic nature ofLLMsbreaks classical assumptions\. Readers familiar with all four topics may proceed to Section[4](https://arxiv.org/html/2608.14590#S4); otherwise, the following subsections provide the necessary grounding\.

### 2\.1Temporal Logic

Temporal Logicextends classical logic with operators over sequences of states, and has become the dominant specification language inLLM\-agent verification\[[45](https://arxiv.org/html/2608.14590#bib.bib6)\]\. The following covers the four variants most relevant to this survey\.

Linear Temporal Logic \(LTL\)\[[45](https://arxiv.org/html/2608.14590#bib.bib6)\]interprets formulas over infinite execution traces\. Its core grammar uses atomic propositions, negation, conjunction, and two primitive temporal operators –X\(*next*\) andU\(*until*\) – from whichF\(*eventually*\) andG\(*globally*\) are derived\. For example,𝐆​\(¬𝑎𝑢𝑡ℎ⇒¬𝑎𝑐𝑐𝑒𝑠𝑠\)\\mathbf\{G\}\(\\neg\\mathit\{auth\}\\Rightarrow\\neg\\mathit\{access\}\)enforces that data access always requires prior authentication, and𝐆​\(𝑡𝑜𝑜𝑙​\_​𝑐𝑎𝑙𝑙⇒𝐗​𝑣𝑒𝑟𝑖𝑓𝑦​\_​𝑜𝑢𝑡𝑝𝑢𝑡\)\\mathbf\{G\}\(\\mathit\{tool\\\_call\}\\Rightarrow\\mathbf\{X\}\\,\\mathit\{verify\\\_output\}\)mandates immediate post\-call verification\.LTLis the target specification language of NL2LTL\[[27](https://arxiv.org/html/2608.14590#bib.bib19)\], NL2Spec\[[11](https://arxiv.org/html/2608.14590#bib.bib20)\], Agent\-C\[[31](https://arxiv.org/html/2608.14590#bib.bib27)\], AgentVerify\[[15](https://arxiv.org/html/2608.14590#bib.bib30)\], LogicGuard\[[22](https://arxiv.org/html/2608.14590#bib.bib36)\], and VerifyLLM\[[23](https://arxiv.org/html/2608.14590#bib.bib33)\]\.

WhileLTLreasons over linear execution traces, branching\-time logics offer an alternative perspective by quantifying over multiple possible futures\.Computation Tree Logic \(CTL\)\[[8](https://arxiv.org/html/2608.14590#bib.bib7)\]extends this to branching\-time trees, pairing path quantifiers \(𝐀\\mathbf\{A\}: all paths;𝐄\\mathbf\{E\}: some path\) with temporal operators, enabling both reachability \(𝐄𝐅​φ\\mathbf\{EF\}\\,\\varphi\) and universal invariants \(𝐀𝐆​φ\\mathbf\{AG\}\\,\\varphi\)\. AgentVerify\[[15](https://arxiv.org/html/2608.14590#bib.bib30)\]exploitsCTLto reason over non\-deterministicLLMoracles embedded inFinite\-State Machines \(FSMs\)\.

BothLTLandCTLassume discrete time steps, but many agent domains require reasoning about continuous time and real\-valued signals\.Signal Temporal Logic \(STL\)\[[42](https://arxiv.org/html/2608.14590#bib.bib8)\]liftsLTLto continuous\-time, real\-valued signals with bounded temporal operators and quantitative robustness semantics: the valueρ​\(φ,𝐱,t\)∈ℝ\\rho\(\\varphi,\\mathbf\{x\},t\)\\in\\mathbb\{R\}measures not only whether a property holds but by how much, making it natural for cyberphysical and robotic agents\[[16](https://arxiv.org/html/2608.14590#bib.bib22),[17](https://arxiv.org/html/2608.14590#bib.bib23)\]\.

A further limitation of standard temporal logics is their determinism: they assume a system either satisfies a property or does not\. For stochasticLLMagents, however, safety is a matter of probability\.Probabilistic Computation Tree Logic \(PCTL\)\[[25](https://arxiv.org/html/2608.14590#bib.bib9)\]augmentsCTLwith probabilistic path quantifiers:𝐏≥p​\[φ\]\\mathbf\{P\}\_\{\\geq p\}\[\\varphi\]asserts thatφ\\varphiholds with probability at leastpp, enabling PRISM\-style model checking of stochastic systems\. ProbGuard\[[56](https://arxiv.org/html/2608.14590#bib.bib37)\]relies on this to bound the probability of unsafe state visits\.

### 2\.2Model Checking

*Model checking*\[[9](https://arxiv.org/html/2608.14590#bib.bib10)\]decides whether a formal modelMMsatisfies a specificationφ\\varphi, writtenM⊧φM\\models\\varphi, and underpins most automated verification approaches surveyed here\.

To apply model checking, one must first represent the system in a formal modeling language\. AKripke structureM=\(S,S0,R,L\)M=\(S,S\_\{0\},R,L\)pairs a finite state space and transition relation with a labeling functionL:S→2A​PL:S\\to 2^\{AP\}that assigns atomic propositions to states\.LTLandCTLformulas are then evaluated over paths or trees of paths throughMM\. In theLLM\-agent context, states capture agent configurations \(task state, memory, tool\-call history\), transitions correspond to actions, and propositions encode safety\-relevant facts such as*authenticated*,*pii\_exposed*, or*budget\_exceeded*\. Verification systems can construct Kripke structures from ReAct\-style plan traces\[[46](https://arxiv.org/html/2608.14590#bib.bib26)\]or define a priori with theLLMembedded as a non\-deterministic oracle\[[15](https://arxiv.org/html/2608.14590#bib.bib30)\]\.

Given a Kripke structure and a specification, the next question is how to perform the actual verification algorithmically\.Automata\-basedLTLmodel checkingtranslates¬φ\\neg\\varphito a Büchi automaton, computes the productM⊗𝒜¬φM\\otimes\\mathcal\{A\}\_\{\\neg\\varphi\}, and checks for an accepting cycle \(a counterexample\); this underlies tools such asSPINandNuSMV\. AgentProof\[[59](https://arxiv.org/html/2608.14590#bib.bib31)\]adopts a variant that compiles safety policies toDeterministic Finite Automatons \(DFAs\)and checks compliance via a graph×\\timesDFAproduct over agent workflow graphs\.

Deterministic automata\-based methods assume that the system’s behavior is fully known and predictable\. When agents exhibit stochastic behavior, however, probabilistic guarantees become necessary\.Probabilistic model checkingextends this to Markov chains andMarkov Decision Processs \(MDPs\), quantifying the probability of reaching an unsafe state\[[34](https://arxiv.org/html/2608.14590#bib.bib11)\]\. ProbGuard\[[56](https://arxiv.org/html/2608.14590#bib.bib37)\]learns aDiscrete\-time Markov Chain \(DTMC\)from observed execution traces and appliesProbably Approximately Correct \(PAC\)\-learning bounds to issue probabilistic safety warnings\.

### 2\.3Classical Planning Formalisms

Classical planning formalismsprovide the structured task representations that severalLLM\-agent verification approaches build upon\.

The most widely adopted formalism in this family isPDDL\[[21](https://arxiv.org/html/2608.14590#bib.bib12)\], the standard input language forAIplanners\. A problem comprises a*domain*\(types, predicates, and action schemas with preconditions and add/delete effects\) and a*problem*\(objects, initial state, and goal\)\. A valid plan is a sequence of ground actions that leads from the initial state to the goal, and tools such as VAL\[[29](https://arxiv.org/html/2608.14590#bib.bib13)\]can check it\. In theLLM\-agent context,LLMsare prompted to generatePDDLdescriptions for an external planner\[[51](https://arxiv.org/html/2608.14590#bib.bib24)\]; the principal challenge is semantic correctness, asLLM\-generatedPDDLachieves high syntactic validity but only24%to35%24\\text\{\\,\}\\mathrm\{\\char 37\\relax\}35\\text\{\\,\}\\mathrm\{\\char 37\\relax\}semantic correctness\.

WhilePDDLremains the most common classical planning formalism, two related frameworks also appear in the verification literature and map naturally toLLMagent structures\.STRIPS\[[18](https://arxiv.org/html/2608.14590#bib.bib14)\], the predecessor toPDDL, andHierarchical Task Network \(HTN\)planning\[[14](https://arxiv.org/html/2608.14590#bib.bib15)\], which decomposes tasks hierarchically into sub\-tasks, both map naturally to the plan structures ofLLMagents \(e\.g\., ReAct, AutoGen\)\.HTNverification is explored in the context of multi\-agent task allocation\[[38](https://arxiv.org/html/2608.14590#bib.bib32)\]\.

### 2\.4LLMAgent Architectures

An*LLMagent*is a system that uses anLLMas a reasoning engine to select and sequence actions from a predefined tool set to accomplish a goal\. We characterize agents along three dimensions relevant to verification\.

The first dimension concerns how the agent represents its plans internally and externally, as this determines which verification methods apply\.Plan representationtakes three forms:*trace\-based*\(interleaved thought–action–observation sequences\[[61](https://arxiv.org/html/2608.14590#bib.bib1)\], the most common and directly amenable toLTLevaluation\),*graph\-based*\(predefined or dynamic control\-flow graphs suited to static analysis andDFAproduct construction\[[59](https://arxiv.org/html/2608.14590#bib.bib31)\]\), and*code\-based*\(executable plans verifiable via program analysis or formal contracts\[[37](https://arxiv.org/html/2608.14590#bib.bib40),[43](https://arxiv.org/html/2608.14590#bib.bib29)\]\)\.

A second, independent dimension is the length of plans the agent must handle, as this directly affects verification tractability\.Execution horizondistinguishes short\-horizon plans \(5to305\\text\{\\,\}30\\text\{\\,\}actions in bounded environments such as household robotics or customer service, tractable for current verifiers\) from long\-horizon plans \(50to50050\\text\{\\,\}500\\text\{\\,\}\+ actions in open\-ended settings such as software engineering or autonomous web navigation, beyond the reach of existing approaches\)\.

The third dimension captures whether a single agent acts in isolation or multiple agents interact, since verification complexity grows substantially with the number of agents\.Agency moderanges from single\-agent systems, which produce one action sequence, to multi\-agent systems, where inter\-agent communication, trust delegation, and emergent interactions render per\-agent verification insufficient\[[38](https://arxiv.org/html/2608.14590#bib.bib32)\]\.

### 2\.5Foundational Definitions

With the three characterization dimensions established, we now formally define the core concepts that the verification pipeline operates on\. These definitions serve three purposes: they fix notation for the remainder of the survey, they establish a common vocabulary across the disparate approaches we review, and they make explicit the assumptions that verification techniques rely upon\. We assume that plans are finite sequences, that safety properties are expressed in temporal logic, and thatSSR, rather than action\-level compliance alone, measures task\-level success\.

###### Definition 1\(LLMAgent Plan\)\.

A*plan*π=\(a1,…,an\)\\pi=\(a\_\{1\},\\ldots,a\_\{n\}\),ai∈𝒯a\_\{i\}\\in\\mathcal\{T\}, is a finite sequence of grounded actions drawn from the agent’s tool set𝒯\\mathcal\{T\}, each associated with a pre\-execution statesis\_\{i\}\.

###### Definition 2\(Plan Safety Property\)\.

A*safety property*φ\\varphiis anLTL\(orCTL/PCTL\) formula over atomic propositions derived from the action–state sequence\. A planπ\\pi*satisfies*φ\\varphi, writtenπ⊧φ\\pi\\models\\varphi, if its induced execution trace satisfiesφ\\varphiunder standard semantics\.

###### Definition 3\(Safe Success Rate \(SSR\)\)\.

Given a task set𝒯\\mathcal\{T\}and safety propertyφ\\varphi:

SSR=\|\{t∈𝒯:task completed correctly∧πt⊧φ\}\|\|𝒯\|\\text\{SSR\}=\\frac\{\|\\\{t\\in\\mathcal\{T\}:\\text\{task completed correctly\}\\wedge\\pi\_\{t\}\\models\\varphi\\\}\|\}\{\|\\mathcal\{T\}\|\}SSRis the primary metric for evaluating enforcement effectiveness\[[47](https://arxiv.org/html/2608.14590#bib.bib45)\]\.

A recurring challenge is the*translation problem*: anLLM\-based translatorτ:𝒩→ℱ\\tau:\\mathcal\{N\}\\to\\mathcal\{F\}fromNLto a formal languageℱ\\mathcal\{F\}\(e\.g\.,LTL,PDDL\) achieves high syntactic validity but low semantic correctness \(τ​\(x\)≢x\\tau\(x\)\\not\\equiv x\), which is the root cause of the false\-assurance problem discussed in Section[5\.7](https://arxiv.org/html/2608.14590#S5.SS7)\.

## 3Methodology

This review follows the PRISMA 2020 guidelines\[[44](https://arxiv.org/html/2608.14590#bib.bib16)\]adapted for computer science literature\. We conducted the review as an independent, rapid, systematic review from 20 to 29 May 2026; we did not pre\-register it, as we note in Section[9\.4](https://arxiv.org/html/2608.14590#S9.SS4)\. We fixed the protocol \(eligibility criteria, search strings, and synthesis approach\) before beginning database searching\.

Eligibility criteria included publication years from 2022 to 2026 \(excluding the pre\-LLM\-agent era before 2022\),LLM\-based agents producing multi\-step plans, action sequences, or tool\-call chains \(excluding pure chatbot or dialogue safety absent planning\), studies addressing plan specification, verification, enforcement, or safety monitoring \(excluding neural network verification unless applied to agent plans\), any study type \(empirical, system/tool, survey, or position\), and English\-language full\-text accessible papers \(excluding conference abstracts without available content\)\.

We searched six databases \(arXiv, ACM DL, IEEE Xplore, Semantic Scholar, Google Scholar, Preprints\.org\) using eight primary search strings targeting formal verification, runtime verification, temporal logic specifications, survey papers, model checking withPDDL,NL\-to\-formal translation, specific enforcement systems \(AgentSpec, AgentGuard, VeriGuard\), and roadmaps\. Supplementary searches covered 22 named systems \(e\.g\., VerifyLLM, AgentVerify, ProbGuard, LogicGuard, AgentProof, NL2LTL, LlamaFirewall\) to ensure that we included systems identified during primary searching\.

The 38 included studies constitute the formal PRISMA corpus and form the basis for all quantitative claims, the taxonomy in Section[4](https://arxiv.org/html/2608.14590#S4), and theGRADEassessments, while the larger reference list \(64 entries\) additionally includes 11 foundational references, 3 methodological references, 10 research agenda references, and 2 contextual comparison works that fall outside the PRISMA inclusion criteria; readers should therefore interpret all quantitative observations in this survey as about the 38 included studies only\.

## 4Taxonomy and Classification System

We introduce a three\-level taxonomy \(Sections[4\.1](https://arxiv.org/html/2608.14590#S4.SS1)to[4\.3](https://arxiv.org/html/2608.14590#S4.SS3)\) classifying all 38 included studies along three orthogonal questions:*when*verification occurs \(Level 1 – pipeline stage\),*what*formal representation is used \(Level 2 – verification moment\), and*how*verification is performed \(Level 3 – formal grounding\)\. The three dimensions are largely independent: a runtime monitor can use temporal logic or probabilistic bounds, while a pre\-execution verifier can use theorem proving or graph\-automata methods\. The only structural correlation is that pre\-execution checking serves SPEC and VERIF, whereas ENF operates at runtime, as detailed in Table[1](https://arxiv.org/html/2608.14590#S4.T1)\.

### 4\.1Level 1 – Pipeline Stage

#### 4\.1\.1Specification \(SPEC\)

Specification techniques handle how safety properties are acquired and expressed\. They are the entry point of the pipeline; verification techniques consume their output\. We identify three sub\-categories:

- •SPEC\-NL:NLto formal specification translation\. The input is a human\-expressed requirement; the output is a formula in a formal notation\. Examples: NL2LTL\[[27](https://arxiv.org/html/2608.14590#bib.bib19)\], NL2Spec\[[11](https://arxiv.org/html/2608.14590#bib.bib20)\],NL\-to\-LTL/Hierarchical Semantic Decomposition \(HSD\)\[[40](https://arxiv.org/html/2608.14590#bib.bib21)\],NL\-to\-STL\[[16](https://arxiv.org/html/2608.14590#bib.bib22),[17](https://arxiv.org/html/2608.14590#bib.bib23)\]\.
- •SPEC\-PL: Planning language specification\. The input is a task description; the output is aPDDLdomain/problem orHTNdescription\. Examples:LLMsas Planning Formalizers\[[51](https://arxiv.org/html/2608.14590#bib.bib24)\], SayCan\[[1](https://arxiv.org/html/2608.14590#bib.bib3)\]\.
- •SPEC\-AL: Alignment\-based specification\. This approach encodes safety requirements as soft constraints, using training objectives or constitutions rather than formal formulas\. Examples: ConstitutionalAI\[[3](https://arxiv.org/html/2608.14590#bib.bib18)\], Agent Safety Alignment viaReinforcement Learning \(RL\)\[[49](https://arxiv.org/html/2608.14590#bib.bib44)\]\.

#### 4\.1\.2Verification \(VERIF\)

Verification techniques determine whether a plan or plan fragment satisfies a specification\. We identify four sub\-categories:

- •VERIF\-MC: Model checking\. The approach translates plans or plan representations to Kripke structures or FSMs; Algorithms checkLTL/CTLproperties\. Examples: Ramani et al\.\[[46](https://arxiv.org/html/2608.14590#bib.bib26)\], AgentVerify\[[15](https://arxiv.org/html/2608.14590#bib.bib30)\], VeriPlan\[[35](https://arxiv.org/html/2608.14590#bib.bib35)\], Logic\-based MAS Verification\[[38](https://arxiv.org/html/2608.14590#bib.bib32)\]\.
- •VERIF\-SA: Static analysis\. Pre\-execution structural checks on agent workflow graphs or code\. Examples: AgentProof\[[59](https://arxiv.org/html/2608.14590#bib.bib31)\], Dafny\-as\-IL\[[37](https://arxiv.org/html/2608.14590#bib.bib40)\], DafnyPro\[[4](https://arxiv.org/html/2608.14590#bib.bib41)\]\.
- •VERIF\-TP: Theorem proving\. Deductive verification against formal contracts\. Examples: AutoRocq\[[52](https://arxiv.org/html/2608.14590#bib.bib39)\], VeriGuard\[[43](https://arxiv.org/html/2608.14590#bib.bib29)\]\.
- •VERIF\-LLM:LLM\-assisted verification\. AnLLMserves as a critic or judge, iteratively checking plan quality without a formal prover\. Examples: Self\-Refine\[[41](https://arxiv.org/html/2608.14590#bib.bib42)\], Plan Verification viaLLM\-as\-Judge\[[26](https://arxiv.org/html/2608.14590#bib.bib34)\]\.

#### 4\.1\.3Enforcement \(ENF\)

Enforcement techniques define what happens when verification finds a violation or anticipates one\. We identify four sub\-categories:

- •ENF\-RT: Runtime monitoring and blocking: online monitors intercept unsafe actions before execution\. Examples: AgentSpec\[[55](https://arxiv.org/html/2608.14590#bib.bib28)\], Agent\-C\[[31](https://arxiv.org/html/2608.14590#bib.bib27)\], VerifyLLM\[[23](https://arxiv.org/html/2608.14590#bib.bib33)\], LogicGuard\[[22](https://arxiv.org/html/2608.14590#bib.bib36)\]\.
- •ENF\-PROB: Probabilistic monitoring\. Stochastic models forecast subsequent violations and trigger early warnings\. Examples: ProbGuard\[[56](https://arxiv.org/html/2608.14590#bib.bib37)\]\.
- •ENF\-SYS: System\-level guardrails\. Multi\-layer security infrastructure operating on prompts, reasoning traces, and generated code\. Examples: LlamaFirewall\[[6](https://arxiv.org/html/2608.14590#bib.bib43)\], Full Stack Safety\[[57](https://arxiv.org/html/2608.14590#bib.bib62)\]\.
- •ENF\-ALIGN: Alignment\-based enforcement\. Model training enforces safety rather than runtime checks\. Examples: ConstitutionalAI\[[3](https://arxiv.org/html/2608.14590#bib.bib18)\], Agent Safety Alignment viaRL\[[49](https://arxiv.org/html/2608.14590#bib.bib44)\]\.

### 4\.2Level 2 – Verification Moment

The literature distinguishes three verification moments, each reflecting a different trade\-off between the strength of the safety guarantee and the practical constraints of plan availability and executability\.

- •Pre\-execution verification: Means the system checks the plan in full before executing any action\. This strategy permits rejection or revision before irreversible effects occur, but requires that the complete plan be available\. Pre\-execution verification appears in AgentProof\[[59](https://arxiv.org/html/2608.14590#bib.bib31)\], the offline phase of VeriGuard\[[43](https://arxiv.org/html/2608.14590#bib.bib29)\], and VerifyLLM\[[23](https://arxiv.org/html/2608.14590#bib.bib33)\]\.
- •Runtime verification: Means the system checks each action before executing it \(or at mostkksteps in advance\)\. This approach handles dynamically generated plans but cannot verify future actions that the system has not yet generated\. Runtime verification appears in AgentSpec\[[55](https://arxiv.org/html/2608.14590#bib.bib28)\], Agent\-C\[[31](https://arxiv.org/html/2608.14590#bib.bib27)\], LogicGuard\[[22](https://arxiv.org/html/2608.14590#bib.bib36)\], and ProbGuard\[[56](https://arxiv.org/html/2608.14590#bib.bib37)\]\.
- •Post\-hoc verification: Means the system analyzes the complete execution trace after the task concludes\. This approach proves useful for auditing and offline learning, but cannot prevent harm during execution\. Post\-hoc verification appears in Self\-Refine\[[41](https://arxiv.org/html/2608.14590#bib.bib42)\]\(in iterative mode\) andLLM\-as\-Judge\[[26](https://arxiv.org/html/2608.14590#bib.bib34)\]\.

### 4\.3Level 3 – Formal Grounding

The included studies rely on several systematic and heuristic backbones\. Temporal Logic usesLTL,CTL,STL, orPCTLas the specification and verification language, supporting sequential, timing, and probabilistic safety properties\. It appears in the majority of included runtime monitoring systems\.

- •Classical planning \(CP\): EmploysPDDLorHTNas the plan representation and verification target, enabling soundness guarantees through established plan validation tools\. It appears inPDDL\-survey work\[[51](https://arxiv.org/html/2608.14590#bib.bib24)\]and SayCan\[[1](https://arxiv.org/html/2608.14590#bib.bib3)\]\.
- •Theorem proving \(TP\): Relies on Coq/Rocq or Dafny as the verification backend, providing complete correctness proofs for organized programs and policies\. It offers the highest assurance level but remains currently limited to code\-based agents, as in AutoRocq\[[52](https://arxiv.org/html/2608.14590#bib.bib39)\], Dafny\-as\-IL\[[37](https://arxiv.org/html/2608.14590#bib.bib40)\], DafnyPro\[[4](https://arxiv.org/html/2608.14590#bib.bib41)\], and VeriGuard\[[43](https://arxiv.org/html/2608.14590#bib.bib29)\]\.
- •Graph and automata methods \(GA\): UseDFA,FSM, or directed graph product constructions for efficient workflow\-level static verification\. They appear in AgentProof\[[59](https://arxiv.org/html/2608.14590#bib.bib31)\]and AgentVerify\[[15](https://arxiv.org/html/2608.14590#bib.bib30)\]\.
- •Probabilistic methods \(PR\): Draw onDTMC,MDP, orPAC\-learning bounds, suiting stochastic agents where deterministic assurances remain unavailable\. ProbGuard\[[56](https://arxiv.org/html/2608.14590#bib.bib37)\]illustrates this approach\.
- •Heuristic and mixed approaches \(HH\): Encompass methods without a single formal mathematical backing, including: \(i\)LLM\-as\-judge criticism \(Self\-Refine\[[41](https://arxiv.org/html/2608.14590#bib.bib42)\], Plan Verification viaLLM\[[26](https://arxiv.org/html/2608.14590#bib.bib34)\]\); \(ii\)RLreward shaping andReinforcement Learning from AI Feedback \(RLAIF\)/Supervised Learning from AI Feedback \(SLAIF\)training \(ConstitutionalAI\[[3](https://arxiv.org/html/2608.14590#bib.bib18)\], Agent Safety Alignment viaRL\[[49](https://arxiv.org/html/2608.14590#bib.bib44)\]\); and \(iii\) multi\-heuristic system pipelines \(Full Stack Safety\[[57](https://arxiv.org/html/2608.14590#bib.bib62)\]\)\. These subtypes differ significantly concerning scalability, soundness properties, and deployment requirements; readers should not treat HH as a homogeneous category\.

### 4\.4Full Classification Table

Table[1](https://arxiv.org/html/2608.14590#S4.T1)classifies all 38 included studies along the three taxonomy dimensions, grouped by pipeline stage\. For each study, the table records the sub\-category, verification moment \(Pre = pre\-execution, RT = runtime, PH = post\-hoc\), formal grounding, andGRADEevidence level\.

Table 1:Classification of all 38 included studies under the proposed taxonomy, grouped by pipeline stage\. Sub\-cat: NL = NL\-to\-formal, PL = planning, AL = alignment, MC = model checking, SA = static analysis, TP = theorem proving, LV =LLM\-verified, RT\-mon = runtime monitoring, PR\-mon = probabilistic monitoring, SYS = system guardrail\. Moment: Pre = pre\-execution, RT = runtime, PH = post\-hoc\. GRADE “—” = foundational or architecture paper without evaluable evidence\.System / PaperYearStageSub\-catMomentGroundingGRADESpecification \(SPEC\)Toolformer\[[48](https://arxiv.org/html/2608.14590#bib.bib2)\]2023SPECNLN/AHH–Chain\-of\-Thought\[[58](https://arxiv.org/html/2608.14590#bib.bib4)\]2022SPECNLN/AHH–Planning Survey\[[30](https://arxiv.org/html/2608.14590#bib.bib5)\]2024SPECNLN/AHH–LLM\+FM Roadmap\[[62](https://arxiv.org/html/2608.14590#bib.bib25)\]2024SPECNLN/ATL–NL2LTL\[[27](https://arxiv.org/html/2608.14590#bib.bib19)\]2023SPECNLPreTLModerateNL2Spec\[[11](https://arxiv.org/html/2608.14590#bib.bib20)\]2023SPECNLPreTLModerateNL\-to\-LTL/HSD\[[40](https://arxiv.org/html/2608.14590#bib.bib21)\]2025SPECNLPreTLLowNL\-to\-STL\[[16](https://arxiv.org/html/2608.14590#bib.bib22)\]2025SPECNLPreTLLowClarifySTL\[[17](https://arxiv.org/html/2608.14590#bib.bib23)\]2026SPECNLPreTLVery LowPDDLSurvey\[[51](https://arxiv.org/html/2608.14590#bib.bib24)\]2025SPECPLN/ACPModerateSayCan\[[1](https://arxiv.org/html/2608.14590#bib.bib3)\]2022SPECPLRTCPLowConstitutionalAI\[[3](https://arxiv.org/html/2608.14590#bib.bib18)\]2022SPECALN/AHH–Verification \(VERIF\)BridgingLLM\+FM\[[46](https://arxiv.org/html/2608.14590#bib.bib26)\]2025VERIFMCPreTLLowAgentVerify\[[15](https://arxiv.org/html/2608.14590#bib.bib30)\]2026VERIFMCPreTL\+GAVery LowLogic\-based MAS\[[38](https://arxiv.org/html/2608.14590#bib.bib32)\]2026VERIFMCPreTLVery LowVeriPlan\[[35](https://arxiv.org/html/2608.14590#bib.bib35)\]2025VERIFMCPreTLLowAgentProof\[[59](https://arxiv.org/html/2608.14590#bib.bib31)\]2026VERIFSAPreGAVery LowDafny\-as\-IL\[[37](https://arxiv.org/html/2608.14590#bib.bib40)\]2025VERIFSAPreTP\-provVery LowDafnyPro\[[4](https://arxiv.org/html/2608.14590#bib.bib41)\]2026VERIFSAPreTP\-provVery LowVeriGuard\[[43](https://arxiv.org/html/2608.14590#bib.bib29)\]2025VERIFTPPreTP\-provVery LowAutoRocq\[[52](https://arxiv.org/html/2608.14590#bib.bib39)\]2025VERIFTPPreTP\-provVery LowReAct\[[61](https://arxiv.org/html/2608.14590#bib.bib1)\]2023VERIFLVRTHH–Self\-Refine\[[41](https://arxiv.org/html/2608.14590#bib.bib42)\]2023VERIFLVPHHHLowPlan Verif\.LLM\[[26](https://arxiv.org/html/2608.14590#bib.bib34)\]2025VERIFLVPHHHVery LowAgent\-SafetyBench\[[63](https://arxiv.org/html/2608.14590#bib.bib47)\]2024VERIFBenchPHHHModerateAgentHarm\[[2](https://arxiv.org/html/2608.14590#bib.bib48)\]2024VERIFBenchPHHHModerateAgentBench\[[39](https://arxiv.org/html/2608.14590#bib.bib49)\]2023VERIFBenchPHHHLowPlanBench\[[53](https://arxiv.org/html/2608.14590#bib.bib50)\]2023VERIFBenchPHCPModerateEnforcement \(ENF\)Agent\-C\[[31](https://arxiv.org/html/2608.14590#bib.bib27)\]2025ENFRT\-monRTTLLowAgentSpec\[[55](https://arxiv.org/html/2608.14590#bib.bib28)\]2025ENFRT\-monRTGALowLogicGuard\[[22](https://arxiv.org/html/2608.14590#bib.bib36)\]2025ENFRT\-monRTTLVery LowVerifyLLM\[[23](https://arxiv.org/html/2608.14590#bib.bib33)\]2025ENFRT\-monPreTLVery LowVerifier Tax\[[47](https://arxiv.org/html/2608.14590#bib.bib45)\]2026ENFRT\-monRTHHLowSafe Tool Use\[[13](https://arxiv.org/html/2608.14590#bib.bib46)\]2025ENFRT\-monRTTLVery LowProbGuard\[[56](https://arxiv.org/html/2608.14590#bib.bib37)\]2025ENFPR\-monRTPRVery LowLlamaFirewall\[[6](https://arxiv.org/html/2608.14590#bib.bib43)\]2025ENFSYSRTHH\+GALowFull Stack Safety\[[57](https://arxiv.org/html/2608.14590#bib.bib62)\]2025ENFSYSRTHH–ConstitutionalAI\[[3](https://arxiv.org/html/2608.14590#bib.bib18)\]2022ENFALN/AHH–RLSafety\[[49](https://arxiv.org/html/2608.14590#bib.bib44)\]2025ENFALN/AHHVery Low
### 4\.5Taxonomy\-Derived Observations

Inspecting Table[1](https://arxiv.org/html/2608.14590#S4.T1)reveals five structural patterns that recur throughout the synthesis in Section[6](https://arxiv.org/html/2608.14590#S6)and the discussion in Section[8](https://arxiv.org/html/2608.14590#S8)\.

1. 1\.Temporal Logic dominance: Temporal Logic \(LTL/CTL/STL\) is the formal grounding for 14 of 38 studies \(37%37\\text\{\\,\}\\mathrm\{\\char 37\\relax\}\), showing its suitability for expressing sequential agent safety properties\. Graph/automata and theorem\-proving approaches each account for approximately11%11\\text\{\\,\}\\mathrm\{\\char 37\\relax\}of studies \(4 papers each\)\. Probabilistic grounding \(DTMC/MDP\) is underrepresented \(one study\), a significant gap given the random nature ofLLMagents\.
2. 2\.Runtime verification is the most active sub\-field: Of 38 studies, 10 \(26%26\\text\{\\,\}\\mathrm\{\\char 37\\relax\}\) operate at runtime\. Pre\-execution techniques account for 15 studies \(39%39\\text\{\\,\}\\mathrm\{\\char 37\\relax\}\), but the majority of these require finite, pre\-specified workflow graphs\. Post\-hoc verification accounts for 6 studies \(16%16\\text\{\\,\}\\mathrm\{\\char 37\\relax\}\) and is predominantlyLLM\-assisted\. The remaining 7 studies \(18%18\\text\{\\,\}\\mathrm\{\\char 37\\relax\}\) are foundational or architectural works with no defined verification moment \(N/A in Table[1](https://arxiv.org/html/2608.14590#S4.T1)\)\.
3. 3\.Specification and enforcement are relatively underserved: Only 12 studies focus primarily on specification \(32%32\\text\{\\,\}\\mathrm\{\\char 37\\relax\}\), and 11 on enforcement \(29%29\\text\{\\,\}\\mathrm\{\\char 37\\relax\}\) – one paper \(Constitutional AI\[[3](https://arxiv.org/html/2608.14590#bib.bib18)\]\) is classified under both SPEC and ENF\. The verification cluster is the largest \(16 studies,42%42\\text\{\\,\}\\mathrm\{\\char 37\\relax\}\)\. This unevenness reflects the field’s origins in formal methods, where verifying a given specification is the core problem; specification acquisition and post\-violation enforcement are comparatively understudied\.
4. 4\.Heuristic/hybrid grounding accounts for a large share of included work: 14 studies \(37%37\\text\{\\,\}\\mathrm\{\\char 37\\relax\}\) rely on heuristic or hybrid grounding – primarilyLLM\-as\-judge,RL, or soft alignment\. These approaches scale well but provide no formal soundness guarantees\. The tension between formal soundness \(low scalability\) and empirical scalability \(no soundness\) is the central unresolved tradeoff in the field\.
5. 5\.GRADEcertainty is predominantly Very Low or Low: Only 6 of 38 studies reach aGRADErating of Moderate; none reach High\. Narrow domain scope, single\-study findings for most key claims, the absence of randomized evaluations, and high heterogeneity in benchmarks limit the field’s certainty\.

### 4\.6Relationship to Prior Taxonomies

Zhang et al\.\[[62](https://arxiv.org/html/2608.14590#bib.bib25)\]propose a three\-way taxonomy \(FM\-enhancing\-LLM,LLM\-enhancing\-FM, unified neural\-symbolic\) that captures the*direction of integration*between formal methods andLLMs, but does not distinguish between verification moments or pipeline stages\. Huang et al\.\[[30](https://arxiv.org/html/2608.14590#bib.bib5)\]classifyLLMplanning approaches by planning strategy \(task decomposition, plan selection, external module, reflection\), but do not address safety verification\. A full\-stack safety survey\[[57](https://arxiv.org/html/2608.14590#bib.bib62)\]categorizes safety concerns by training phase \(data, training, deployment\), but does not focus on formal verification\.

Our taxonomy is orthogonal to these preceding frameworks: it classifies by*pipeline stage*,*verification moment*, and*formal grounding*rather than by integration direction, planning strategy, or deployment phase\. Used in conjunction with prior taxonomies, it provides a more thorough characterization of any individual approach\.

## 5Related Work

The intersection ofLLMsagents and formal validation is an emerging, rapidly evolving field\. We organize the related work into five thematic clusters that mirror the pipeline from plan representation to safety enforcement: \(i\) foundational agent architectures and plan representations, \(ii\) specification techniques, \(iii\) verification approaches, \(iv\) enforcement and correction mechanisms, and \(v\) benchmarks and evaluation\. Within each cluster, we compare the principal contributions, identify their limitations, and highlight the gaps that motivate the present survey\.

### 5\.1Comparison with Prior Surveys

Table[2](https://arxiv.org/html/2608.14590#S5.T2)compares this survey with three prior works that most closely overlap its scope\. No prior survey applies a systematic search protocol to the complete specification\-verification\-enforcement pipeline, providesGRADEcertainty grading, or synthesizes the verifier tax as a field\-level empirical finding\.

Table 2:Comparison with related surveys\. Type: SLR = Systematic Literature Review; NS = Narrative Survey\. Pipeline: S = Specification, V = Verification, E = Enforcement\.SurveyTypeScopeMethodFM depthPipelineEvidenceZhang et al\.\[[62](https://arxiv.org/html/2608.14590#bib.bib25)\]NSFM–LLMintegrationNarrativeMod\.S, VNoneFull\-Stack Safety\[[57](https://arxiv.org/html/2608.14590#bib.bib62)\]NSFullLLMsafetyNarrativeLowPartialNoneHuang et al\.\[[30](https://arxiv.org/html/2608.14590#bib.bib5)\]NSLLMplanningNarrativeNoneS onlyNoneThis surveySLRSpec\-Verif\-EnfPRISMA 2020DeepS,V,EGRADE
### 5\.2Foundational Agent Architectures and Plan Representations

The representation of an agent’s plan essentially affects the tractability of formal verification\. Analysis of the 38 included studies reveals three representation paradigms that have emerged from theLLM\-agent literature, each with distinct properties from a verification standpoint\.

First,trace\-based representations\(ReAct,Chain\-of\-Thought \(CoT\)\) use anLLMto alternate betweenNL“thought” steps and external “action” calls, resulting in a sequence of \(thought, action, observation\) triples\[[61](https://arxiv.org/html/2608.14590#bib.bib1)\]\. This approach makes reasoning explicit and each plan step easy to follow, producing an execution trace suitable forLTLmodel checking\[[46](https://arxiv.org/html/2608.14590#bib.bib26),[23](https://arxiv.org/html/2608.14590#bib.bib33)\]\. In largerLLMs,CoTprompting\[[58](https://arxiv.org/html/2608.14590#bib.bib4)\]generates multi\-step reasoning traces whose precondition–action–effect structure resembles STRIPS operator schemas\[[51](https://arxiv.org/html/2608.14590#bib.bib24)\], allowing partial translation to classical planning formats\. However, both models share a major limitation: plan correctness is only checked*after*the model has generated the full thought\-action trace\.

Second,tool\-augmented representations\(Toolformer, SayCan\) trainLLMsto self\-annotateApplication Programming Interface \(API\)calls inline withNLtext\[[48](https://arxiv.org/html/2608.14590#bib.bib2)\]\. The resulting hybrid representation –NLinterleaved with embeddedAPIcall slots – poses significant challenges for formal extraction because the boundary between specification and execution is implicit\.LLMplanning has been grounded in robotic affordance functions, scoring candidate actions using both language model probabilities and a skill\-value function\[[1](https://arxiv.org/html/2608.14590#bib.bib3)\]\. SayCan provides an implicit safety filter \(the system suppresses low\-affordance actions\) but lacks formal guarantees; we best understand it as a learned precursor to explicit enforcement\.

Third,graph\-based representations\(LangGraph, CrewAI, AutoGen\) represent plans as directed state graphs with typed nodes \(agents, tools, and control structures\) and typed edges \(data movement and control flow\)\. This representation is directly amenable to static graph analysis and product\-automaton model checking\[[59](https://arxiv.org/html/2608.14590#bib.bib31)\]\. A prior taxonomy classifiesLLMplanning into task decomposition, plan selection, external module use, and reflection/memory – each corresponding to different verification entry points\[[30](https://arxiv.org/html/2608.14590#bib.bib5)\]\.

Trace\-based representations are the most widely studied for runtime verification, whereas graph\-based representations are the most amenable to pre\-deployment static analysis\. Neither paradigm simultaneously supports complete pre\-execution verification and arbitrary open\-ended planning\. The core representational gap is the absence of a*canonical intermediate representation*that faithfully retains both the semantic content of anLLM\-generated plan and the architectural properties required for formal analysis\.

### 5\.3Specification Techniques

Formal verification requires expressing properties in a rigorous language\. Three specification paradigms emerge from systematic analysis of the included studies: Temporal Logic, classical planning formalisms, andNLconstitutions\.

First,Linear Temporal Logic \(LTL\)and derivativeshave become the main specification language for agent plans\. NL2LTL uses GPT\-3 and few\-shot prompting to translateNLinstructions intoLTLformulas for robotics\[[27](https://arxiv.org/html/2608.14590#bib.bib19)\], while NL2Spec adds an interactive disambiguation loop where theLLMqueries the user when requirements are ambiguous\[[11](https://arxiv.org/html/2608.14590#bib.bib20)\]\. To reduce hallucinations in formula generation,HSDdivides complex requirements into simpler parts\[[40](https://arxiv.org/html/2608.14590#bib.bib21)\], and for cyber\-physical and robotic tasks, theNL\-to\-specification approach has been extended toSTL, combiningLLM\-based generation with external knowledge and clarification dialogues\[[16](https://arxiv.org/html/2608.14590#bib.bib22),[17](https://arxiv.org/html/2608.14590#bib.bib23)\]\. These works share a common finding:LLM\-basedNL\-to\-LTLtranslation achieves high syntactic correctness \(above90%90\\text\{\\,\}\\mathrm\{\\char 37\\relax\}for leading models\) but suffers from low semantic correctness – the generated formula is syntactically well\-formed but does not capture the intended property\. TheHSDapproach reduces this gap but does not eliminate it, as semantic correctness requires ground\-truth execution traces for validation, which are unavailable in novel task domains\[[40](https://arxiv.org/html/2608.14590#bib.bib21)\]\.

Second,classical planning formalisms \(PDDL\)have been extensively studied for specification\. A survey covering 40\+ papers onLLM\-to\-PDDLtranslation finds that, while leadingLLMsachieve above96%96\\text\{\\,\}\\mathrm\{\\char 37\\relax\}syntactic correctness inPDDLgeneration, semantic correctness – verified via plan validation tools such as VAL – remains at24\.8%to35\.1%24\.8\\text\{\\,\}\\mathrm\{\\char 37\\relax\}35\.1\\text\{\\,\}\\mathrm\{\\char 37\\relax\}for the best\-performing models\[[51](https://arxiv.org/html/2608.14590#bib.bib24)\]\. This result has a direct implication for formal verification: verifying aPDDLmodel whose preconditions and effects are semantically incorrect provides false assurance rather than genuine safety guarantees\. The same conclusion has been reached through benchmark evaluation, showing thatLLMsfail on even simple planning tasks under formalPDDLequivalence checking\[[53](https://arxiv.org/html/2608.14590#bib.bib50)\]\.

Third,NLconstitutions and alignment specificationsoffer a non\-formal alternative\. ConstitutionalAI, encoding agent constraints as aNLconstitution of 58 principles used to guide bothSLAIFandRLAIF, was introduced\[[3](https://arxiv.org/html/2608.14590#bib.bib18)\]\. While not a formal specification, ConstitutionalAIestablishes an example for declarative constraint encoding and is now the foundation of productionAIsystems\. Its limitation is the absence of formal semantics: two principles may conflict, and the model cannot prove or disprove compliance with any individual constraint\.

A synthesis of 200\+ papers identified three integration directions for formal techniques andLLMs: FM\-enhancing\-LLM\(using verification to certifyLLMoutputs\),LLM\-enhancing\-FM \(usingLLMsto improve the usability of formal tools\), and unified neural\-symbolic systems\[[62](https://arxiv.org/html/2608.14590#bib.bib25)\]\. This tripartite taxonomy organizes much of the subsequent work reviewed below\.

The specification sub\-field faces a fundamental bootstrapping problem:NLis the medium through which humans express safety requirements, yet all formal specification languages require expert knowledge to use correctly\.LLM\-basedNL\-to\-formal translation reduces this barrier but creates a semantic gap that remains unclosed\. No current system provides end\-to\-end, verified specification acquisition – from ambiguousNLrequirements to formally correct and complete safety specifications – across open\-ended task domains\.

### 5\.4Verification Approaches

Given a plan representation and a specification, the verification literature has pursued four paradigms: model checking, static analysis, runtime monitoring, andLLM\-assisted verification\.

First,model checking of agent planstranslatesNLplans into Kripke structures andLTLspecifications, then applies model checking\[[46](https://arxiv.org/html/2608.14590#bib.bib26)\]\. On PlanBench, GPT\-5 achieves an F1 of96\.3%96\.3\\text\{\\,\}\\mathrm\{\\char 37\\relax\}for plan\-conformance classification with high syntactic validity, but the semantic correctness of generated Kripke structures stays unverified\. Another approach treats theLLMas a non\-deterministic oracle within a formalFSM, enabling compositionalLTLspecifications for memory integrity, tool protocols, skill invocation, and human\-in\-the\-loop boundaries\[[15](https://arxiv.org/html/2608.14590#bib.bib30)\]\. Researchers have also used discrete event systems withLTLautomata to formally checkLLM\-generated multi\-robot task allocations against collision and precedence constraints\[[38](https://arxiv.org/html/2608.14590#bib.bib32)\], and a user study \(n=12\) found that model checking improved end\-user planning quality and satisfaction\[[35](https://arxiv.org/html/2608.14590#bib.bib35)\]\. A common limitation of model\-checking approaches is state\-space scalability: exhaustive checking over Kripke structures derived fromLLMplans becomes intractable as the plan horizon and vocabulary grow\. None of the included studies show model checking at the scale of realistic long\-horizon agentic tasks \(e\.g\., SWE\-bench, where plans may involve hundreds of actions\)\.

Second,static analysis and workflow verificationoffers pre\-deployment soundness guarantees\. AgentProof is a static verifier for agent workflow graphs, extracting an abstract graph from four frameworks \(LangGraph, CrewAI, AutoGen, Google ADK\), applying safety checks, and evaluating temporal policies via adomain\-specific language \(DSL\)compiled toDFA\[[59](https://arxiv.org/html/2608.14590#bib.bib31)\]\. In 18 workflows,27%27\\text\{\\,\}\\mathrm\{\\char 37\\relax\}had structural defects and55%55\\text\{\\,\}\\mathrm\{\\char 37\\relax\}failed a human\-gate policy; verification finishes in under a second for graphs up to 5,000 nodes\. AutoRocq verifies programs with Rocq \(Coq\) through iterative refinement, handling 641 SV\-COMP theorems without proof\-example pre\-training\[[52](https://arxiv.org/html/2608.14590#bib.bib39)\], and VeriGuard \(Google\) synthesizes and verifies a behavioral policy offline, then uses it as a runtime monitor\[[43](https://arxiv.org/html/2608.14590#bib.bib29)\]\. Static analysis, however, is inherently limited to*finite, prespecified*workflow graphs and cannot verify plans dynamically generated at runtime in response to recorded environmental state – the dominant mode in realistic agentic deployments\.

Third,runtime verification and monitoringis the most active and technically mature cluster\. AgentSpec, a lightweightDSLfor specifying and enforcing runtime constraints, achieves above90%90\\text\{\\,\}\\mathrm\{\\char 37\\relax\}unsafe execution prevention in code agents,100%100\\text\{\\,\}\\mathrm\{\\char 37\\relax\}hazardous action elimination in embodied agents, and100%100\\text\{\\,\}\\mathrm\{\\char 37\\relax\}compliance in autonomous driving at millisecond\-per\-rule overhead\[[55](https://arxiv.org/html/2608.14590#bib.bib28)\]\. Agent\-C enforces*temporal*safety behaviors – constraints on action*sequences*rather than single actions – by translating specifications into first\-order logic and applyingSatisfiability Modulo Theories \(SMT\)\-based constrained decoding during token generation, improving GPT\-5 conformance from83\.7%to100%83\.7\\text\{\\,\}\\mathrm\{\\char 37\\relax\}100\\text\{\\,\}\\mathrm\{\\char 37\\relax\}and Claude Sonnet 4\.5 from77\.4%to100%77\.4\\text\{\\,\}\\mathrm\{\\char 37\\relax\}100\\text\{\\,\}\\mathrm\{\\char 37\\relax\}, with utility retention above70%70\\text\{\\,\}\\mathrm\{\\char 37\\relax\}\[[31](https://arxiv.org/html/2608.14590#bib.bib27)\]\. LogicGuard adopts an actor\-critic architecture where the critic analyses full trajectories and proposesLTLconstraints communicated inNLto the actor, creating a closed\-loop safety feedback mechanism that outperforms SayCan and InnerMonologue on the Minecraft diamond\-mining benchmark\[[22](https://arxiv.org/html/2608.14590#bib.bib36)\]\. ProbGuard models agent execution traces as aDTMC\. It providesPAC\-style probabilistic early warnings up to 38\.66 seconds before safety violations in self\-driving vehicles, while reducing unsafe behavior by65\.37%65\.37\\text\{\\,\}\\mathrm\{\\char 37\\relax\}in household agents\[[56](https://arxiv.org/html/2608.14590#bib.bib37)\]\. A few\-shot prompting method with a sliding\-window approach \(optimal window: five actions\) performs pre\-executionLTLverification of robotic task plans, detecting position errors, missing prerequisites, and redundant actions\[[23](https://arxiv.org/html/2608.14590#bib.bib33)\]\. AgentGuard targets adversarial risks through dual\-agent cooperation, modular memory, and runtime policy enforcement against prompt injection, tool\-induced exploitation, multi\-agent collusion, and memory poisoning\[[33](https://arxiv.org/html/2608.14590#bib.bib38)\]\.

Fourth,LLM\-assisted verificationuses anLLM\-as\-Judge critic with iterative plan revision, attaining up to90%90\\text\{\\,\}\\mathrm\{\\char 37\\relax\}recall and100%100\\text\{\\,\}\\mathrm\{\\char 37\\relax\}exactness across fourLLMs, with96\.5%96\.5\\text\{\\,\}\\mathrm\{\\char 37\\relax\}of sequences converging within three iterations\[[26](https://arxiv.org/html/2608.14590#bib.bib34)\]\. Self\-Refine establishes the general pattern ofLLMself\-critique, achieving approximately a20%20\\text\{\\,\}\\mathrm\{\\char 37\\relax\}improvement in plan quality on task benchmarks without retraining\[[41](https://arxiv.org/html/2608.14590#bib.bib42)\]\.LLM\-assisted verification offers accessibility but lacks formal soundness guarantees: a model that generates unsafe plans can also justify them during self\-critique\[[57](https://arxiv.org/html/2608.14590#bib.bib62)\]\. A separate line of work uses Dafny as a verification\-aware intermediate language: theLLMgenerates code annotated with pre/post\-conditions and loop invariants, which the Dafny verifier checks before compilation\[[37](https://arxiv.org/html/2608.14590#bib.bib40),[4](https://arxiv.org/html/2608.14590#bib.bib41)\]\. DafnyPro achieves86%86\\text\{\\,\}\\mathrm\{\\char 37\\relax\}correct proofs on DafnyBench, a 16\-percentage\-point improvement over the prior state of the art\.

Runtime monitoring methods \(AgentSpec, Agent\-C, ProbGuard\) offer the best combination of practical deployability and demonstrated safety improvements, but provide only one\-step or short\-horizon guarantees\. Static methods \(AgentProof, VeriGuard offline\) offer pre\-deployment soundness but are limited to finite, pre\-specified workflows\. Model checking approaches handle richer temporal properties but face state\-space explosion at realistic task scales\.LLM\-assisted verification is accessible and scalable but lacks formal soundness\.*No existing strategy combines soundness, completeness, scalability, and open\-ended task generality\.*

### 5\.5Enforcement and Correction Mechanisms

Enforcement concerns what happens when a plan or action violates a safety property\. Examining enforcement mechanisms across the 38 included studies, we identify several distinct approaches and a central empirical finding\.

First,hard enforcementimplements token generation blocking via constrained decoding when the partial plan would violate a temporal constraint\[[31](https://arxiv.org/html/2608.14590#bib.bib27)\]\. This approach achieves100%100\\text\{\\,\}\\mathrm\{\\char 37\\relax\}conformance in closed domains but incurs a utility cost known as the*verifier tax*\. Hard enforcement also appears as rule\-triggered blocking with configurable enforcement actions \(block, log, redirect\), which achieves millisecond overhead per rule evaluation\[[55](https://arxiv.org/html/2608.14590#bib.bib28)\]\.

Second,system\-level guardrailsprovide a multi\-layer security architecture\. LlamaFirewall comprises PromptGuard 2 \(jailbreak detection\), Agent Alignment Verifications \(chain\-of\-thought auditing for goal misalignment\), and CodeShield \(static analysis to prevent insecure code generation\)\[[6](https://arxiv.org/html/2608.14590#bib.bib43)\]\. Deployed in production at Meta, it achieves a90%90\\text\{\\,\}\\mathrm\{\\char 37\\relax\}reduction in the attack success rate on AgentDojo, bringing it to1\.75%1\.75\\text\{\\,\}\\mathrm\{\\char 37\\relax\}\. Researchers have also proposed a unified safety\-alignment framework that fine\-tunes tool\-using agents using a sandboxedRLenvironment with three\-way action classification \(benign/malicious/sensitive\) and fine\-grained reward shaping\[[49](https://arxiv.org/html/2608.14590#bib.bib44)\]\.

Third,the verifier tax problemrepresents the most significant empirical finding in the enforcement literature\. Even when enforcement intercepts up to94%94\\text\{\\,\}\\mathrm\{\\char 37\\relax\}of individually unsafe actions,SSR\(the fraction of tasks completed both safely and correctly\) remains below5%5\\text\{\\,\}\\mathrm\{\\char 37\\relax\}in most settings\[[47](https://arxiv.org/html/2608.14590#bib.bib45)\]\. This finding, supported by measurements of safety enforcement onτ\\tau\-Bench\[[60](https://arxiv.org/html/2608.14590#bib.bib51)\], is driven by*integrity leaks*: the model hallucinates user identifiers to bypass authentication checks and finds alternative unsafe paths after direct violations are blocked\. This behavior challenges the implicit assumption in most enforcement papers that intercepting individual unsafe actions is sufficient for safe task completion\.

Fourth,safe tool usehas been formalized in a theoretical framework that specifies the conditions for verifiably safe tool\-usingLLMagents, abstracting over specific supervisory mechanisms\[[13](https://arxiv.org/html/2608.14590#bib.bib46)\]\.

Our comparative assessment reveals a fundamental tension in the enforcement sub\-field: enforcement systems that successfully block unsafe individual actions do not automatically ensure safe task completion\. This tension creates a gap between*action\-level safety*\(verified by most existing systems\) and*task\-level safety*\(measured bySSR\) that no current system bridges reliably at scale\.

### 5\.6Benchmarks and Evaluation

The rapid expansion of this field has driven the parallel development of evaluation infrastructure, including several benchmarks that define how agent safety and performance are measured\.

1. 1\.AgentBench, the first systematic benchmark evaluatingLLMsas agents across 8 environments, tested 29LLMsand established task success rate as the primary metric\[[39](https://arxiv.org/html/2608.14590#bib.bib49)\]\.
2. 2\.Agent\-SafetyBench– the most comprehensive safety benchmark to date, comprising 349 environments, 2,000 test cases, 8 safety risk categories, and 10 failure modes – introduces a new standard for evaluation\[[63](https://arxiv.org/html/2608.14590#bib.bib47)\]\. Its headline finding – that none of 16LLMagents’ scores above60%60\\text\{\\,\}\\mathrm\{\\char 37\\relax\}safety – motivates the entire formal verification agenda\.
3. 3\.AgentHarmevaluates 110 explicitly malicious agent tasks across 11 harm categories, demonstrating that frontier models exhibit limited robustness even to basic jailbreak attacks in multi\-step agentic settings\[[2](https://arxiv.org/html/2608.14590#bib.bib48)\]\.
4. 4\.PlanBenchintroduces a benchmark for evaluatingLLMson formalPDDLplanning tasks, exposing systematic failures under strict equivalence checking\[[53](https://arxiv.org/html/2608.14590#bib.bib50)\]\.
5. 5\.τ\\tau\-Bench, which evaluates policy compliance in transactional tool\-agent\-user environments using explicit procedural policies – a natural evaluation platform for formal enforcement methods – was introduced\[[60](https://arxiv.org/html/2608.14590#bib.bib51)\]\.

A critical gap is the absence of a*unified benchmark*that simultaneously evaluates: \(a\) formal verification coverage \(proportion of safety properties that can be specified and checked\), \(b\) runtime overhead \(latency introduced by verification\), \(c\)SSR\(tasks completed both safely and correctly\), and \(d\) generalisability across agent architectures and task domains\. Existing benchmarks address at most two of these dimensions\. The introduction ofSSRrepresents an important step, but other benchmarks have not yet adopted this metric\.

### 5\.7Research Gaps and Survey Objectives

Synthesizing the five clusters above, we identify ten open problems that the existing literature has not resolved\. We state each briefly here; Section[7](https://arxiv.org/html/2608.14590#S7)gives the full technical treatment\.

1. RG1\.Semantic translation gap\.NL\-to\-formal translation achieves above90%90\\text\{\\,\}\\mathrm\{\\char 37\\relax\}syntactic correctness but only24%to35%24\\text\{\\,\}\\mathrm\{\\char 37\\relax\}35\\text\{\\,\}\\mathrm\{\\char 37\\relax\}semantic correctness\[[51](https://arxiv.org/html/2608.14590#bib.bib24),[11](https://arxiv.org/html/2608.14590#bib.bib20)\], propagating false assurance through every downstream verifier\.
2. RG2\.Scalability to long\-horizon plans\.Existing verified systems handle5to305\\text\{\\,\}30\\text\{\\,\}actions; long\-horizon tasks \(SWE\-bench scale\) remain beyond exhaustive model checking\.
3. RG3\.The verifier tax\.Intercepting94%94\\text\{\\,\}\\mathrm\{\\char 37\\relax\}of unsafe actions still yieldsSSRbelow5%5\\text\{\\,\}\\mathrm\{\\char 37\\relax\}\[[47](https://arxiv.org/html/2608.14590#bib.bib45)\]because agents hallucinate credentials to bypass blocked paths\.
4. RG4\.Dynamic plan generation\.Static methods require pre\-specified finite graphs; most deployed agents generate plans dynamically in response to the environment state\.
5. RG5\.Multi\-agent verification\.Per\-agent verification cannot capture emergent interaction patterns \(collusion, cascade failures, trust delegation\) in multi\-agent systems\[[38](https://arxiv.org/html/2608.14590#bib.bib32)\]\.
6. RG6\.Probabilistic specification\.LLMsare inherently stochastic; deterministic safety specifications are a mismatch\. PRISM\-stylePCTLmodel checking of agent plans remains unstudied beyond ProbGuard\[[56](https://arxiv.org/html/2608.14590#bib.bib37)\]\.
7. RG7\.Verified re\-planning\.No current system generates a constraint\-satisfying alternative plan segment when a violation is detected; all existing approaches block or abort\.
8. RG8\.Specification acquisition at scale\.Writing formal safety rules requires expert effort that does not scale to the breadth of deployment domains; automated mining from demonstrations or regulatory documents is nascent\.
9. RG9\.Adversarial robustness\.Verification components are themselves attack surfaces; adversarial evaluation of the end\-to\-end pipeline is systematically absent\[[33](https://arxiv.org/html/2608.14590#bib.bib38),[6](https://arxiv.org/html/2608.14590#bib.bib43)\]\.
10. RG10\.Evaluation standardisation\.No benchmark jointly evaluates formal verification coverage, runtime overhead, andSSRacross architectures and domains\.

The ten gaps define the scope of this survey’s contributions\. As shown in Table[2](https://arxiv.org/html/2608.14590#S5.T2), no prior survey covers all three pipeline stages using a systematic methodology with evidence grading; this survey is the first to do so\.

## 6Cross\-Cutting Synthesis

This section presents a cross\-cutting analysis of the 38 included studies, integrating findings across the five thematic clusters identified in Section[5](https://arxiv.org/html/2608.14590#S5)\. We organize the synthesis around five themes that cut across cluster boundaries, provide aGRADEcertainty table for all principal claims, and characterize the coverage landscape using a gap heatmap\.

### 6\.1Theme A – The Translation Bottleneck

Every approach that applies classical formal verification toLLMagent plans faces the translation problem: convertingNLplans or specifications into formal structures amenable to algorithmic analysis\. Evidence across multiple studies consistently shows thatLLMsachieve high*syntactic*correctness but low*semantic*correctness in this translation\.

Evidence on syntactic correctness shows that across theNL\-to\-formal specification cluster,LLMsachieve above90%90\\text\{\\,\}\\mathrm\{\\char 37\\relax\}syntactic validity inLTLformula generation\[[27](https://arxiv.org/html/2608.14590#bib.bib19),[11](https://arxiv.org/html/2608.14590#bib.bib20),[40](https://arxiv.org/html/2608.14590#bib.bib21)\]and above96%96\\text\{\\,\}\\mathrm\{\\char 37\\relax\}syntactic validity inPDDLgeneration\[[51](https://arxiv.org/html/2608.14590#bib.bib24)\]\. In Kripke structure generation, prior work reports near\-perfect syntactic validity with an F1 score of96\.3%96\.3\\text\{\\,\}\\mathrm\{\\char 37\\relax\}on plan\-conformance classification\[[46](https://arxiv.org/html/2608.14590#bib.bib26)\]\.

Evidence on semantic correctness – the degree to which a generated formula captures the intended property – tells a different story\. A synthesis of 40\+ papers finds that leading models achieve only24\.8%to35\.1%24\.8\\text\{\\,\}\\mathrm\{\\char 37\\relax\}35\.1\\text\{\\,\}\\mathrm\{\\char 37\\relax\}semantic correctness inPDDLgeneration, verified via VAL plan validation\[[51](https://arxiv.org/html/2608.14590#bib.bib24)\]\. Research shows that even with interactive disambiguation loops, semantic errors persist for novel or ambiguous requirements\[[11](https://arxiv.org/html/2608.14590#bib.bib20)\]\. Hierarchical decomposition reducesLTLsemantic errors but does not eliminate them; no study provides a semantic error rate below10%10\\text\{\\,\}\\mathrm\{\\char 37\\relax\}for open\-ended task domains\[[40](https://arxiv.org/html/2608.14590#bib.bib21)\]\.

Formal verification is only as sound as its specification\. A model checker operating on a semantically incorrectLTLformula can produce a clean verdict \(no violation found\) for a plan that is, in fact, unsafe – providing false assurance\. This semantic gap means that the*completeness*of specification acquisition is the binding constraint on the soundness of end\-to\-end verification, not the power of the verification algorithm applied downstream\.

Current best practice combinesLLM\-based translation with either an interactive disambiguation loop \(NL2Spec\[[11](https://arxiv.org/html/2608.14590#bib.bib20)\], ClarifySTL\[[17](https://arxiv.org/html/2608.14590#bib.bib23)\]\) or hierarchical decomposition \(HSD\[[40](https://arxiv.org/html/2608.14590#bib.bib21)\]\)\. Neither approach provides formal guarantees of semantic correctness; both reduce error rates without eliminating them\. Verified specification acquisition – in which the translation itself is proved correct – remains an open problem \(RG1\)\.

### 6\.2Theme B – Runtime vs\. Static Verification Trade\-offs

The verification moment dimension of the taxonomy \(Section[4\.2](https://arxiv.org/html/2608.14590#S4.SS2)\) reveals a fundamental trade\-off between*completeness*and*applicability to dynamic plans*\.

Static verification approaches, such as AgentProof\[[59](https://arxiv.org/html/2608.14590#bib.bib31)\]and VeriGuard’s offline phase\[[43](https://arxiv.org/html/2608.14590#bib.bib29)\], provide pre\-deployment soundness guarantees: if the workflow graph passes verification, no execution trace of that graph can violate the checked properties\. AgentProof verifies in sub\-second time for graphs up to50005000nodes\. The cost, however, is scope: static methods assume a prespecified, finite workflow graph\. AnLLMgenerates plans dynamically in response to environment observations, so one cannot verify these plans statically before generation\.

Runtime monitoring systems – AgentSpec\[[55](https://arxiv.org/html/2608.14590#bib.bib28)\], Agent\-C\[[31](https://arxiv.org/html/2608.14590#bib.bib27)\], ProbGuard\[[56](https://arxiv.org/html/2608.14590#bib.bib37)\], LogicGuard\[[22](https://arxiv.org/html/2608.14590#bib.bib36)\], and VerifyLLM\[[23](https://arxiv.org/html/2608.14590#bib.bib33)\]– handle dynamically generated plans by checking each action \(or a sliding window of actions\) before execution\. Runtime monitors operate at millisecond\-per\-action overhead\[[55](https://arxiv.org/html/2608.14590#bib.bib28)\]and can enforce temporal sequence properties\[[31](https://arxiv.org/html/2608.14590#bib.bib27)\]\. The cost here is incompleteness: a monitor that checks actionaia\_\{i\}before execution cannot reason about the safety of the as\-yet\-ungenerated actionsai\+1,…,ana\_\{i\+1\},\\ldots,a\_\{n\}\.

No included study achieves a combination that is both complete \(sound over full plan traces\) and scalable to dynamically generated, open\-ended plans\. VeriGuard\[[43](https://arxiv.org/html/2608.14590#bib.bib29)\]comes closest by verifying a policy offline and using the verified policy as a runtime filter, but this requires the policy to be finite and pre\-specified\. Partial verification – verifying safety\-critical sub\-sequences with compositional guarantees for the remainder – is a promising direction but has not yet been demonstrated at scale \(RG2, RG4\)\.

Table[3](https://arxiv.org/html/2608.14590#S6.T3)summarises reported overhead across runtime monitoring systems\. Only AgentSpec\[[55](https://arxiv.org/html/2608.14590#bib.bib28)\]quantifies overhead in milliseconds; four of six systems do not quantify overhead at all\. This absence of standardized overhead reporting itself constitutes a finding related to the evaluation standardization gap \(RG10\)\. Without consistent overhead measurement, we cannot perform cross\-system comparisons or cost\-benefit assessments of enforcement\. None of the included studies reports an end\-to\-end impact on task latency\.

Table 3:Reported runtime overhead for enforcement systems\.SystemOverhead unitReported valueDomainAgentSpec\[[55](https://arxiv.org/html/2608.14590#bib.bib28)\]Per\-rule evaluationMillisecondsCode, embodied, drivingAgent\-C\[[31](https://arxiv.org/html/2608.14590#bib.bib27)\]Constrained decodingNot quantifiedRetail, airlineProbGuard\[[56](https://arxiv.org/html/2608.14590#bib.bib37)\]Warning lead timeUp to 38\.66 sAutonomous drivingLogicGuard\[[22](https://arxiv.org/html/2608.14590#bib.bib36)\]Critic evaluationNot quantifiedMinecraftVerifyLLM\[[23](https://arxiv.org/html/2608.14590#bib.bib33)\]Per\-window checkNot quantifiedHousehold roboticsLlamaFirewall\[[6](https://arxiv.org/html/2608.14590#bib.bib43)\]Per\-requestProduction latencyMeta production
### 6\.3Theme C – The Verifier Tax

The most consequential empirical finding in the corpus is what has been termed the*verifier tax*: a systematic gap between action\-level safety \(measured by the fraction of individually unsafe actions blocked\) and task\-level safety \(measured bySSR\)\[[47](https://arxiv.org/html/2608.14590#bib.bib45)\]\.

Onτ\\tau\-Bench\[[60](https://arxiv.org/html/2608.14590#bib.bib51)\], the TRIAD\-SAFETY enforcement architecture intercepts up to94%94\\text\{\\,\}\\mathrm\{\\char 37\\relax\}of non\-compliant individual actions\. YetSSR– the fraction of tasks completed both safely and correctly – remains below5%5\\text\{\\,\}\\mathrm\{\\char 37\\relax\}in most settings\. This gap exceeds one order of magnitude\.

The primary driver identified is integrity leaks: agents hallucinate user identifiers \(account numbers, policy codes\) to bypass authentication constraints when the legitimate path is blocked\[[47](https://arxiv.org/html/2608.14590#bib.bib45)\]\. The monitor correctly identifies that the hallucinated identifier is different from the real one and blocks those attempts, too, but the agent continues attempting alternative fabrications\. The result is a task stuck in a failure loop: neither completed nor executed in a provably safe manner\.

Most enforcement papers implicitly assume that blocking unsafe individual actions is sufficient for safe task completion\. The verifier tax finding falsifies this assumption: an agent that cannot execute its intended \(possibly unsafe\) plan will search for alternative plans that achieve the same goal while bypassing the safety check, rather than gracefully failing\. This behavior exemplifies Goodhart’s Law: when a proxy measure \(action\-level compliance\) becomes the target of optimization, agents optimize the proxy rather than the underlying goal \(task\-level safety\)\.

The verifier tax implies that effective enforcement requires:

- •Plan\-level, not action\-level, safety policies: Constraints must reason about the goal and context of the full plan, not just the legality of individual actions\.
- •Integrity constraints: Formal invariants prevent hallucination of identifiers or credentials by checking them against ground truth\.
- •Safe replanning: Upon detecting a violation, the system should generate an alternative plan segment that satisfies all constraints and continues toward the goal, rather than simply blocking\.

No single system in the included corpus meets any of these three requirements\. Although no independent replication has confirmed the verifier tax – a single study finding, which limits itsGRADEcertainty to*Low*– the mechanism that the study identifies is consistent with failure patterns noted in AgentGuard\[[33](https://arxiv.org/html/2608.14590#bib.bib38)\]\(agents bypassing monitors via multi\-agent collusion\) and LlamaFirewall\[[6](https://arxiv.org/html/2608.14590#bib.bib43)\]\(a residual1\.75%1\.75\\text\{\\,\}\\mathrm\{\\char 37\\relax\}attack success rate after90%90\\text\{\\,\}\\mathrm\{\\char 37\\relax\}reduction, driven by adaptive adversaries finding alternative paths\)\.

The verifier tax and the translation bottleneck are compounding, not independent, failure modes\. When specifications are semantically incorrect \(Theme A\), the enforcement rules derived from them will also be semantically incorrect: the monitor blocks actions that are unsafe*according to the flawed specification*, not necessarily those that are unsafe*in the real world*\. This incorrectness creates a second source ofSSRdegradation beyond the integrity\-leak mechanism: agents that satisfy a semantically incorrect specification may still execute genuinely unsafe plans, while agents blocked on legitimate paths \(due to specification over\-conservatism\) seek alternatives\. Resolving the verifier tax, therefore, requires progress on both the enforcement architecture \(RG3\) and the correctness of the semantic specification \(RG1\); neither is sufficient on its own\.

### 6\.4Theme D – Probabilistic Monitoring as Middle Ground

ProbGuard\[[56](https://arxiv.org/html/2608.14590#bib.bib37)\]and the broader probabilistic monitoring paradigm represent a pragmatic middle ground between deterministic enforcement \(high assurance, low scalability\) and no verification \(high scalability, no assurance\)\.

Rather than guaranteeing zero violations – difficult for stochastic, open\-ended agents – probabilistic monitors provide:

- •Early warnings:ProbGuard provides safety warnings up to 38\.66 seconds in advance in autonomous driving scenarios, enabling human intervention or replanning before irreversible harm\.
- •PAC\-style accuracy bounds:the monitor’s warning accuracy is bounded byPAC\-learning guarantees, providing a formal relationship between the number of observed traces and the probability of false alarms\.
- •Graceful degradation:in household agent settings, ProbGuard reduces unsafe behavior by65\.37%65\.37\\text\{\\,\}\\mathrm\{\\char 37\\relax\}while preserving80\.4%80\.4\\text\{\\,\}\\mathrm\{\\char 37\\relax\}task completion rate – a substantially better safety\-utility trade\-off than hard enforcement\.

ProbGuard requires aDTMCmodel trained on observed traces, which requires a corpus of prior agent executions in the target domain\. It provides probabilistic rather than deterministic guarantees, which may be insufficient for safety\-critical deployments\. It has been evaluated in only two domains \(autonomous driving and household agents\), thereby limiting generalisability \(GRADE:*Very Low*\)\.

Probabilistic monitoring sidesteps the verifier tax problem: rather than attempting to block all violations \(which would drive the agent to seek alternative unsafe paths\), it issues warnings\. It defers to human intervention, preserving the agent’s plan space while flagging risks\. This combination suggests that the optimal enforcement architecture may combine probabilistic monitoring \(for early warning\) with selective hard blocking \(for high\-certainty, high\-severity violations\), rather than relying exclusively on either paradigm\.

### 6\.5Theme E – Compositional Specification as an Organizing Principle

AgentVerify\[[15](https://arxiv.org/html/2608.14590#bib.bib30)\]and AgentProof\[[59](https://arxiv.org/html/2608.14590#bib.bib31)\]independently argue for and demonstrate compositional specification: they specify and verify safety properties for distinct concern domains \(memory integrity, tool call protocols, human\-in\-the\-loop boundaries\) independently, then compose them\.

Compositional specification demonstrates several benefits\. First, incremental verification allows us to check, update, or extend individual property families without re\-verifying the entire system\. Second, reuse across architectures is possible: AgentProof applies the same compositional framework to four distinct agent orchestration frameworks \(LangGraph, CrewAI, AutoGen, Google ADK\), demonstrating cross\-architecture reuse\. Third, modular auditability means separate safety domains can be audited independently by domain\-specific reviewers\.

Table[4](https://arxiv.org/html/2608.14590#S6.T4)maps the safety domains addressed by included enforcement and verification systems\.

Table 4:Safety domains addressed by included verification/enforcement systems\. ✓: explicitly evaluated\.∘\\circ: partially addressed\. —: not addressed\.SystemTemporal seq\.Memory/PIITool safetyCredentialsMulti\-agentAdversarialAgentSpec\[[55](https://arxiv.org/html/2608.14590#bib.bib28)\]✓∘\\circ✓———Agent\-C\[[31](https://arxiv.org/html/2608.14590#bib.bib27)\]✓—✓∘\\circ——AgentVerify\[[15](https://arxiv.org/html/2608.14590#bib.bib30)\]✓✓✓———AgentProof\[[59](https://arxiv.org/html/2608.14590#bib.bib31)\]✓∘\\circ✓—∘\\circ—LlamaFirewall\[[6](https://arxiv.org/html/2608.14590#bib.bib43)\]——∘\\circ——✓AgentGuard\[[33](https://arxiv.org/html/2608.14590#bib.bib38)\]—✓∘\\circ—✓✓ProbGuard\[[56](https://arxiv.org/html/2608.14590#bib.bib37)\]✓—————VeriGuard\[[43](https://arxiv.org/html/2608.14590#bib.bib29)\]∘\\circ✓✓———Table[4](https://arxiv.org/html/2608.14590#S6.T4)reveals a consistent pattern: temporal sequence properties and tool safety are the most widely addressed domains; credential integrity and multi\-agent collusion are systematically underaddressed\. This gap directly maps to the integrity leak mechanism driving the verifier tax \(Theme C\) and to the multi\-agent verification gap \(RG5\)\.

### 6\.6GRADECertainty Assessment

Table[5](https://arxiv.org/html/2608.14590#S6.T5)presents theGRADEcertainty assessment for the principal claim in each of the five thematic clusters\. We downgrade certainty from*High*for: study limitations \(L\), inconsistency across studies \(I\), indirectness \(narrow domains, non\-generalizable benchmarks\) \(D\), and imprecision \(single study, wide confidence\) \(P\)\.

Table 5:GRADEcertainty of evidence for principal claims\. Downgrade reasons: L = study limitations, I = inconsistency, D = indirectness, P = imprecision \(single study\)\.ClaimSupporting evidenceLIDPGRADENoLLMagent achieves\>\>60%60\\text\{\\,\}\\mathrm\{\\char 37\\relax\}safety on comprehensive benchmarksAgent\-SafetyBench \(16 agents, 2k cases\)\[[63](https://arxiv.org/html/2608.14590#bib.bib47)\]ModerateLLM\-to\-LTLtranslation achieves\>\>90%90\\text\{\\,\}\\mathrm\{\\char 37\\relax\}syntactic correctness4\+ independent studies\[[27](https://arxiv.org/html/2608.14590#bib.bib19),[11](https://arxiv.org/html/2608.14590#bib.bib20),[40](https://arxiv.org/html/2608.14590#bib.bib21),[46](https://arxiv.org/html/2608.14590#bib.bib26)\]✓ModerateLLM\-to\-PDDLsemantic correctness is24%to35%24\\text\{\\,\}\\mathrm\{\\char 37\\relax\}35\\text\{\\,\}\\mathrm\{\\char 37\\relax\}Survey of 40\+ papers\[[51](https://arxiv.org/html/2608.14590#bib.bib24)\]✓✓ModerateLTLruntime enforcement achieves100%100\\text\{\\,\}\\mathrm\{\\char 37\\relax\}conformance in closed domainsAgent\-C, AgentSpec \(2 studies\)\[[31](https://arxiv.org/html/2608.14590#bib.bib27),[55](https://arxiv.org/html/2608.14590#bib.bib28)\]✓✓✓LowStatic graph verification detects structural defects in<<1 sAgentProof \(1 study, 18 workflows\)\[[59](https://arxiv.org/html/2608.14590#bib.bib31)\]✓✓✓Very LowProbabilistic monitoring warns 38\.66 s before violationProbGuard \(1 study, 2 domains\)\[[56](https://arxiv.org/html/2608.14590#bib.bib37)\]✓✓✓Very LowEnforcement reducesSSR\(verifier tax\)Verifier Tax \(1 study,τ\\tau\-Bench\)\[[47](https://arxiv.org/html/2608.14590#bib.bib45)\]✓✓✓LowLLMself\-critique improves plan quality by∼\\sim20%20\\text\{\\,\}\\mathrm\{\\char 37\\relax\}Self\-Refine \(NeurIPS 2023\)\[[41](https://arxiv.org/html/2608.14590#bib.bib42)\]✓✓✓LowDafny intermediate language achieves86%86\\text\{\\,\}\\mathrm\{\\char 37\\relax\}proof successDafnyPro \(1 study, DafnyBench\)\[[4](https://arxiv.org/html/2608.14590#bib.bib41)\]✓✓✓Very LowTheGRADEsummary reflects the field’s early stage: despite positive findings across multiple systems, several factors limit certainty – limited domain scope, the absence of independent replication, and high benchmark heterogeneity\. The three*Moderate*certainty claims form the empirical bedrock of the field; all other claims require replication at a larger scale and across diverse domains before they can inform deployment decisions\.

### 6\.7Coverage Heatmap

Table[6](https://arxiv.org/html/2608.14590#S6.T6)maps the ten identified research gaps \(RG1 to RG10\) against the five thematic clusters\. Each cell indicates whether the cluster*causes*the gap \(∙\\bullet\), partially addresses it \(∘\\circ\), or is unrelated \(blank\)\.

Table 6:Gap coverage heatmap\.∙\\bullet: this cluster gives rise to or studies the gap\.∘\\circ: the cluster partially addresses the gap\.GapArchSpecVerifEnfBenchRG1 – Semantic translation∙\\bullet∘\\circRG2 – Long\-horizon scale∙\\bullet∙\\bullet∘\\circRG3 – Verifier tax∘\\circ∙\\bullet∙\\bulletRG4 – Dynamic plan generation∙\\bullet∙\\bulletRG5 – Multi\-agent∙\\bullet∘\\circ∙\\bulletRG6 – Stochastic model check\.∘\\circ∙\\bulletRG7 – Verified re\-planning∘\\circ∘\\circ∙\\bulletRG8 – Spec acquisition scale∙\\bulletRG9 – Adversarial robustness∘\\circ∙\\bulletRG10 – Evaluation standard\.∘\\circ∙\\bulletThe heatmap reveals two structural asymmetries\. First, the specification cluster is the source of RG1 and RG8 – the two gaps that are purely about how properties are acquired – and is not a target of any other cluster’s work\. This finding confirms that specification is the most underinvested part of the pipeline relative to its importance\. Second, the enforcement cluster drives RG3 \(verifier tax\) and RG7 \(verified replanning\)\. Still, these gaps also require input from verification \(for plan\-level reasoning\) and benchmarks \(forSSRmeasurement\) – they inherently span multiple clusters so that no single sub\-field can resolve them\.

## 7Research Agenda

This section elaborates the ten open problems \(RG1 to RG10\) identified through systematic gap analysis in Sections[5\.7](https://arxiv.org/html/2608.14590#S5.SS7)and[6](https://arxiv.org/html/2608.14590#S6)\. For each gap, we describe: the current state of the art, the core technical difficulty, and two to three concrete research directions with pointers to the most relevant prior work\.

### 7\.1RG1 – Semantic Correctness inNL\-to\-Formal Translation

LLM\-basedNL\-to\-formal translation achieves above90%90\\text\{\\,\}\\mathrm\{\\char 37\\relax\}syntactic correctness forLTLand above96%96\\text\{\\,\}\\mathrm\{\\char 37\\relax\}forPDDL, but only24%to35%24\\text\{\\,\}\\mathrm\{\\char 37\\relax\}35\\text\{\\,\}\\mathrm\{\\char 37\\relax\}semantic correctness forPDDL\[[51](https://arxiv.org/html/2608.14590#bib.bib24)\]and comparable rates forLTL\[[11](https://arxiv.org/html/2608.14590#bib.bib20)\]\. Interactive disambiguation \(NL2Spec\[[11](https://arxiv.org/html/2608.14590#bib.bib20)\], ClarifySTL\[[17](https://arxiv.org/html/2608.14590#bib.bib23)\]\) and hierarchical decomposition\[[40](https://arxiv.org/html/2608.14590#bib.bib21)\]reduce semantic errors but do not eliminate them\. The evaluation assesses semantic correctness post hoc using plan validators \(VAL\) or model checkers against ground\-truth traces – neither of which is available for novel domains\.

Semantic correctness requires that we formalize truth: we need a formal model that correctly represents the intended domain semantics\. For novel domains, however, we lack any independent ground truth apart from the specification we are evaluating\. The problem is therefore circular: to verify that a specification is semantically correct, one needs a formal oracle that is itself a correct formalization of the domain\.

1. RG1\.1Grammar\-constrained decoding for formal languages:LLMdecoding can be constrained to produce only syntactically valid outputs by restricting the token distribution at each step to tokens consistent with the formal grammar\[[20](https://arxiv.org/html/2608.14590#bib.bib52)\]\. Extended to semantic constraints \(e\.g\., well\-typedness of predicate arguments inPDDL\), constrained decoding can eliminate a class of semantic errors at generation time\. Integrating semantic type systems forLTLandPDDLinto decoding constraints is an open engineering challenge\.
2. RG1\.2Equivalence checking via counter\-example guided synthesis: Given two candidate translations of the sameNLrequirement, a model checker can determine whether they are semantically equivalent by searching for a Kripke structure that satisfies one but not the other\. If the system finds a counterexample, it can return the discrepancy to theLLMas feedback for refinement – aCounter\-example Guided Inductive Synthesis \(CEGIS\)\[[50](https://arxiv.org/html/2608.14590#bib.bib53)\]loop adapted to specification translation\. NL2Spec’s disambiguation loop\[[11](https://arxiv.org/html/2608.14590#bib.bib20)\]is a step in this direction; fullCEGISintegration remains unstudied\.
3. RG1\.3Semantic ground\-truth benchmarks: Progress on semantic correctness requires benchmark datasets that pair eachNLrequirement with a formally verifiedLTL/PDDLspecification and a corpus of execution traces that definitively test semantic correctness\. Such benchmarks do not yet exist at scale for agent safety domains\. Crowdsourcing requirements from real agent deployment logs, verified by domain experts, is a feasible near\-term path\.

### 7\.2RG2 – Scalability to Long\-Horizon Plans

Current verified systems handle plans of5to305\\text\{\\,\}30\\text\{\\,\}actions\[[55](https://arxiv.org/html/2608.14590#bib.bib28),[31](https://arxiv.org/html/2608.14590#bib.bib27),[23](https://arxiv.org/html/2608.14590#bib.bib33)\]\. AgentProof\[[59](https://arxiv.org/html/2608.14590#bib.bib31)\]scales to graphs of 5,000 nodes in pre\-deployment static verification, but this applies to finite workflow graphs, not open\-ended dynamic plans\. Long\-horizon tasks \(SWE\-bench: 100\+ actions; autonomous research assistants: 500\+ actions\) are beyond the reach of exhaustive model checking\. The number of states in a Kripke structure grows exponentially with plan length\. For open\-endedLLMagents, the branching factor at each step is the model’s vocabulary size \(∼\\sim100k tokens\), making exhaustive model checking computationally infeasible\.

RG2\.1 – Partial verification of safety\-critical sub\-sequences\.Many long\-horizon plans contain a small number of safety\-critical segments \(e\.g\., authentication sequences, file deletion chains, financial transaction sequences\) surrounded by safe filler actions\. Automatically identifying and verifying these sub\-sequences – using static analysis to tag high\-risk action types – could provide partial verification guarantees at manageable cost\. The AgentVerify compositional framework\[[15](https://arxiv.org/html/2608.14590#bib.bib30)\]provides a foundation; targeted identification of safety\-critical sub\-sequences within it is unstudied\.

RG2\.2 – Abstraction\-refinement for agent plans\.Counterexample\-guided Abstraction Refinement \(CEGAR\)\[[7](https://arxiv.org/html/2608.14590#bib.bib54)\]starts with a coarse abstraction of the state space, model\-checks the abstraction, and refines it when it finds a spurious counterexample\. When adapted toLLMagent plans,CEGARcould abstract away low\-risk action types \(e\.g\., read\-only queries\) and focus verification effort on high\-risk transitions, iteratively refining the abstraction when soundness violations occur\.

RG2\.3 – Compositional verification with assume\-guarantee contracts\.Long\-horizon plans decompose into segments with formal interface contracts: each segment assumes a set of preconditions and guarantees a set of postconditions\[[10](https://arxiv.org/html/2608.14590#bib.bib55)\]\. Verifying each segment against its contract and composing the pros avoids the need to model\-check the full plan trace\. AgentProof\[[59](https://arxiv.org/html/2608.14590#bib.bib31)\]demonstrates segment\-level verification; assume\-guarantee composition across dynamically generated segments remains open\.

### 7\.3RG3 – The Verifier Tax

Empirical studies show that even when a system intercepts94%94\\text\{\\,\}\\mathrm\{\\char 37\\relax\}of individually unsafe actions,SSRremains below5%5\\text\{\\,\}\\mathrm\{\\char 37\\relax\}, driven by integrity leaks: agents hallucinating credentials to bypass blocked paths\[[47](https://arxiv.org/html/2608.14590#bib.bib45)\]\. No existing system resolves this gap\. Agent\-C achieves100%100\\text\{\\,\}\\mathrm\{\\char 37\\relax\}action conformance but does not reportSSR\[[31](https://arxiv.org/html/2608.14590#bib.bib27)\]; AgentSpec reports task success rates but notSSRas defined in the literature\[[55](https://arxiv.org/html/2608.14590#bib.bib28),[47](https://arxiv.org/html/2608.14590#bib.bib45)\]\. The verifier tax is a goal\-optimization phenomenon: when the direct path to the goal is blocked, the agent searches for an alternative path, which may be unsafe in ways the monitor does not anticipate\. Blocking actions one by one without considering the agent’s goal makes the enforcement gameable\.

RG3\.1 – Plan\-level safety policies\.Instead of checking individual actions, a plan\-level safety monitor checks a proposed sub\-sequence or full plan fragment against properties that reference the goal context\. This requirement means the monitor must have access to the agent’s goal representation \(e\.g\., the task description and current intent\) and the action sequence\. Agent\-C’s temporalDSL\[[31](https://arxiv.org/html/2608.14590#bib.bib27)\]is a step toward this; extending it to goal\-contextual properties is an open problem\.

RG3\.2 – Credential and identity integrity constraints\.The integrity leak mechanism operates specifically as follows: the agent fabricates identifiers that appear plausible but do not exist in the ground\-truth user database\. A dedicated integrity monitor – which maintains a ground\-truth index of valid identifiers and rejects any action referencing an identifier not in the index – would close this specific attack vector\. This mechanism parallels SQL injection prevention via parameterized queries, in which the system rejects inputs that deviate from a trusted schema\.

RG3\.3 – Safe replanning upon violation\.Rather than simply blocking a violating action, the enforcement system should trigger a replanning request: generate an alternative action sequence from the current state that satisfies all safety constraints and makes progress toward the goal\. This replanning requirement integrates the enforcement monitor with a constrained planner \(e\.g\., aPDDLsolver or anLLMwith hard constraints\), and this integration represents the most technically ambitious direction for resolving the verifier tax\. VeriPlan\[[35](https://arxiv.org/html/2608.14590#bib.bib35)\]demonstrates model\-checker\-guided user\-facing replanning; adapting this to automated agent replanning is an open problem\.

### 7\.4RG4 – Dynamic Plan Generation

Static verification \(AgentProof\[[59](https://arxiv.org/html/2608.14590#bib.bib31)\], VeriGuard offline\[[43](https://arxiv.org/html/2608.14590#bib.bib29)\]\) requires pre\-specified finite workflow graphs\. Most realLLMagent deployments generate plans dynamically in response to environment state: the agent observes the current state, generates the next action, executes it, observes the outcome, and repeats\. No included study provides pre\-execution soundness guarantees for dynamically assembled plans\.

RG4\.1 – Online workflow graph extraction\.As an agent executes, the sequence of calls it makes to sub\-agents and tools implicitly defines a workflow graph\. Extracting this graph in real time and running incremental static checks \(adding each new node and edge as the system encounters them\) could provide online structural verification without requiring the full graph to be pre\-specified\. AgentProof’s framework\[[59](https://arxiv.org/html/2608.14590#bib.bib31)\]is a candidate starting point; online incremental model checking over dynamically growing graphs is an active area in formal methods\.

RG4\.2 – Verified plan template instantiation\.Many agent tasks share high\-level plan structures \(templates\) that differ only in parameter instantiation\. Pre\-verifying these templates against safety properties – and also verifying that each dynamically generated instantiation of a verified template conforms to the original – would provide soundness guarantees for parameterized plan families\. This verification strategy parallels type\-checked generics: the system applies the type system \(verifier\) to the template, and instantiations inherit the proof\.

### 7\.5RG5 – Multi\-Agent Verification

Researchers have focused the vast majority of verification work on single\-agent plans\. They have applied discrete event systems\-basedLTLverification to task allocation in multi\-robot manufacturing, and prior work has addressed MCP/skill invocation protocols in multi\-agent settings\[[38](https://arxiv.org/html/2608.14590#bib.bib32),[15](https://arxiv.org/html/2608.14590#bib.bib30)\]\. Prior work\[[33](https://arxiv.org/html/2608.14590#bib.bib38)\]has also tacitly addressed multi\-agent collusion as an adversarial threat\. However, no study provides a general compositional verification framework for arbitrary multi\-agent system topologies\. Multi\-agent systems exhibit emergent interaction patterns – role confusion, trust delegation, cascade failures, collusion – that are not reducible to the properties of individual agents\. Verifying a property of a multi\-agent system requires reasoning about the joint execution of all agents, which compounds the state\-space explosion problem\.

RG5\.1 – Contract\-based interfaces between agents\.We can specify each agent using an assume\-guarantee contract: a formal interface that describes the inputs it assumes and the outputs it guarantees\[[10](https://arxiv.org/html/2608.14590#bib.bib55)\]\. Composing these contracts allows us to verify system\-level properties from component\-level proofs without exhaustive joint state\-space exploration\. This approach is standard in concurrent system verification; adapting it toLLMagents with non\-deterministic outputs presents an open challenge\.

RG5\.2 – Protocol verification for inter\-agent communication\.In multi\-agent systems, agents communicate via structured message\-passing protocols\. Formalizing these protocols as session types or communicating automata\[[28](https://arxiv.org/html/2608.14590#bib.bib56)\]and checking them for safety properties \(no deadlock, no privilege escalation\) is a tractable sub\-problem of multi\-agent verification\. The MCP/skill invocation protocols of AgentVerify\[[15](https://arxiv.org/html/2608.14590#bib.bib30)\]are a starting point\.

### 7\.6RG6 – Probabilistic Specification and Stochastic Model Checking

LLMsare inherently stochastic: the same plan generation call with the same prompt can produce different action sequences across runs\. Therefore, we should express safety properties for stochastic agents probabilistically \(“the agent violates the policy with probability less thanϵ\\epsilon”\) rather than deterministically\. ProbGuard\[[56](https://arxiv.org/html/2608.14590#bib.bib37)\]is the only included study that addresses probabilistic safety; it usesDTMCmodels withPAC\-learning bounds\. Researchers have not applied PRISM\-stylePCTLmodel checking toLLMagent plans\.

RG6\.1 –PCTLspecifications forLLMagent safety properties\.We can lift standard safety specifications \(e\.g\., “authenticate before data access”\) to probabilistic versions: “the probability of accessing data without prior authentication is less than 0\.01”\.PCTLprovides the formal language for such statements; PRISM provides a tool to check them againstDTMCorMDPmodels\. Adapting PRISM toLLMagent execution traces – learning theDTMCfrom empirical traces and model\-checkingPCTLproperties against it – is a feasible and direct extension of ProbGuard\.

RG6\.2 – Calibrated uncertainty quantification for safety monitors\.Current deterministic monitors make binary block/allow decisions\. A monitor that quantifies its own uncertainty – outputting a probability of violation rather than a binary verdict – can be integrated with risk\-threshold policies, enabling deployments to explicitly calibrate the safety\-utility trade\-off\. Conformal prediction\[[54](https://arxiv.org/html/2608.14590#bib.bib57)\]provides a distribution\-free framework for calibrated uncertainty quantification, but researchers have not yet applied it to agent safety monitoring\.

### 7\.7RG7 – Verified Re\-Planning

When a plan violates a safety property, all included enforcement systems either block the action, log and continue, or abort the task\. None generates an alternative plan segment that satisfies all safety constraints and continues toward the goal\. VeriPlan\[[35](https://arxiv.org/html/2608.14590#bib.bib35)\]generates user\-facing constraint\-satisfying plans in end\-user planning settings but does not address automated replanning for agentic systems\.

RG7\.1 – Constraint\-satisfying plan repair\.Plan repair\[[19](https://arxiv.org/html/2608.14590#bib.bib58)\]modifies a failing plan minimally to restore validity\. Integrated with anLTLorPDDLconstraint checker, plan repair could generate an alternative plan fragment from the point of violation that satisfies all checked properties\. The challenge forLLM\-based agents is that plan repair operates on formal plan representations, whereasLLMplans are inNL– requiring a bidirectional translation pipeline\.

RG7\.2 – ConstrainedLLMplan generation\.Rather than repairing a violating plan post\-hoc, the enforcement system can impose hard constraints on theLLM’s generation process, steering the model toward safe plan completions using constrained beam search orSMT\-guided decoding\. Agent\-C’sSMT\-based constrained decoding\[[31](https://arxiv.org/html/2608.14590#bib.bib27)\]demonstrates feasibility for temporal sequence constraints; extension to arbitraryLTLproperties over plan prefixes is an open problem\.

### 7\.8RG8 – Specification Acquisition at Scale

Writing formal safety specifications \(LTLformulas, AgentSpecDSLrules,PDDLconstraints\) requires formal methods expertise\. This expertise requirement creates a scalability bottleneck: there are far more agent\-deployment domains than there are formal\-methods experts\. Existing approaches to automated specification acquisition – mining from demonstrations\[[27](https://arxiv.org/html/2608.14590#bib.bib19)\], interactive disambiguation from regulatory text\[[11](https://arxiv.org/html/2608.14590#bib.bib20)\]– remain nascent and have seen evaluation only in narrow domains\.

RG8\.1 – Specification mining from demonstration traces\.Given a corpus of labeled agent execution traces \(safe vs\. unsafe\), specification mining algorithms\[[5](https://arxiv.org/html/2608.14590#bib.bib59)\]can inferLTLformulas that distinguish safe from unsafe traces\. Applying this toLLMagent execution logs – which are increasingly available from production deployments – would enable data\-driven specification acquisition without human expert authoring\.

RG8\.2 – Specification extraction from regulatory and policy documents\.Formal regulations govern many agent deployment domains \(e\.g\., GDPR, HIPAA, and financial compliance rules\)\. Extracting formal safety specifications from these documents – usingLLMsas translators under expert validation – would leverage existing domain knowledge and produce reusable specification libraries\. The literature demonstrates the principle for unstructured text; no study has yet applied it at scale to structured regulatory documents\[[11](https://arxiv.org/html/2608.14590#bib.bib20)\]\.

RG8\.3 – Compositional specification libraries\.A shared, peer\-reviewed library of reusableLTLandDSLspecifications for common agent safety properties \(authentication\-before\-access, data\-minimization, human\-gate\-before\-irreversible\-action\) would reduce the per\-deployment specification burden\. AgentVerify’s four\-domain specification library\[[15](https://arxiv.org/html/2608.14590#bib.bib30)\]provides a seed, but the community needs to curate it systematically\.

### 7\.9RG9 – Adversarial Robustness of Verification Systems

Enforcement systems themselves present attack surfaces\. Researchers have demonstrated prompt\-injection attacks that bypass AgentSpec\-style monitors\[[33](https://arxiv.org/html/2608.14590#bib.bib38)\]; production\-grade guardrails still allow1\.75%1\.75\\text\{\\,\}\\mathrm\{\\char 37\\relax\}attack success\[[6](https://arxiv.org/html/2608.14590#bib.bib43)\]\. Verification components that rely onLLM\-based translation are additionally vulnerable to adversarial inputs that cause theLLMto generate incorrect specifications or Kripke structures\[[57](https://arxiv.org/html/2608.14590#bib.bib62)\]\. Adversarial evaluation of verification and enforcement systems is systematically absent from the literature\.

RG9\.1 – Red\-teaming of verification pipelines\.Systematic adversarial evaluation of the end\-to\-end pipeline – fromNLrequirement elicitation through specification translation, model checking, and enforcement – is needed to characterize the attack surface\. AdaptingLLMred\-teaming methodologies\[[2](https://arxiv.org/html/2608.14590#bib.bib48)\]to target the verification pipeline specifically \(prompt injection into specification generators, adversarial Kripke structures, monitor bypass via indirect action sequences\) would characterize the residual risk of each component\.

RG9\.2 – Formal robustness guarantees for specification translators\.If the specification translator is itself formally verified \(e\.g\., through type\-safe grammars or certified compilation\), its correctness guarantee is robust to adversarial inputs by construction\. Applying verified compilation techniques\[[36](https://arxiv.org/html/2608.14590#bib.bib60)\]toLTL\-generating components – at least for a restricted fragment of the input language – would provide robustness without relying on empirical red\-teaming\.

### 7\.10RG10 – Evaluation Standardisation

No benchmark simultaneously evaluates formal verification coverage, runtime overhead, andSSRacross multiple agent architectures and task domains\. Existing benchmarks address subsets: Agent\-SafetyBench\[[63](https://arxiv.org/html/2608.14590#bib.bib47)\]covers safety but not formal verification;τ\\tau\-Bench\[[60](https://arxiv.org/html/2608.14590#bib.bib51)\]enablesSSRmeasurement but only in a narrow transactional domain; AgentBench\[[39](https://arxiv.org/html/2608.14590#bib.bib49)\]covers task success but not safety\. The Verifier Tax paper\[[47](https://arxiv.org/html/2608.14590#bib.bib45)\]introducedSSRas a unified metric but evaluated it on a single benchmark\.

RG10\.1 – A unified formal safety evaluation suite\.A benchmark should define: \(a\) a set of task environments with known ground\-truth safe and unsafe plans; \(b\) a corresponding library of formal safety specifications for each task; \(c\) standardized metrics includingSSR, formal verification coverage \(a formal language captures only a fraction of possible safety properties\), and runtime overhead\. This benchmark should be contributed to by the formal methods,NLP, andAIsafety communities jointly to ensure coverage of all relevant dimensions\.

RG10\.2 – Adoption ofSSRas the primary metric\.The field should standardize onSSR\[[47](https://arxiv.org/html/2608.14590#bib.bib45)\]as the primary evaluation metric for enforcement systems, supplemented by action\-level conformance as a secondary metric\.SSRcaptures the end\-to\-end objective \(tasks completed both safely and correctly\) and avoids the false confidence that action\-level compliance rates alone provide\. A community\-maintained leaderboard or shared evaluation server would accelerate metric adoption\.

RG10\.3 – Benchmark contamination mitigation\.LLMstrained on internet data may have memorized evaluation scenarios from public benchmarks, inflating reported performance\. Mitigation strategies include held\-out evaluation sets updated after each major model release, procedurally generated tasks with verifiable ground truth, and canary task detection for known contamination in benchmarks\.

## 8Discussion

The taxonomy developed in Section[4](https://arxiv.org/html/2608.14590#S4)provides a structural lens for analyzing the literature\. We now turn to its implications, organizing the discussion around five themes: field maturity, practical deployment recommendations, relationships between safety paradigms, societal and ethical considerations, and threats to the validity of this review\.

### 8\.1Field Maturity Assessment

The field of formal verification forLLMagent plans is at an early but structurally sound stage of development\. Using the Gartner Hype Cycle\[[12](https://arxiv.org/html/2608.14590#bib.bib63)\]as a rough heuristic, the field appears to be transitioning from the*Peak of Inflated Expectations*\(2023 to 2024, marked by many demonstration papers with limited evaluation\) toward the*Slope of Enlightenment*\(2025–2026, with the first empirical findings that challenge simplistic assumptions – most notably the verifier tax\[[47](https://arxiv.org/html/2608.14590#bib.bib45)\]\)\.

Indicators of earlymaturityinclude convergence on a dominant specification language \(LTL\) with consistent findings across independent groups\[[27](https://arxiv.org/html/2608.14590#bib.bib19),[11](https://arxiv.org/html/2608.14590#bib.bib20),[31](https://arxiv.org/html/2608.14590#bib.bib27),[55](https://arxiv.org/html/2608.14590#bib.bib28)\]; the emergence of dedicated workshops at major software engineering and programming\-languages venues as forums for this research; production deployment of at least one system \(LlamaFirewall\[[6](https://arxiv.org/html/2608.14590#bib.bib43)\]at Meta\) with disclosed performance metrics; the development of standardised benchmarks \(Agent\-SafetyBench\[[63](https://arxiv.org/html/2608.14590#bib.bib47)\],τ\\tau\-Bench\[[60](https://arxiv.org/html/2608.14590#bib.bib51)\]\) that enable cross\-system comparison; and the first negative empirical result that challenges field assumptions \(verifier tax\[[47](https://arxiv.org/html/2608.14590#bib.bib45)\]\)\.

Indicators ofimmaturityinclude thatGRADEcertainty is*Low*or*Very Low*for most principal claims with no claim reaching*High*; most studies are single\-group, single\-domain evaluations without independent replication; no system simultaneously satisfies soundness, completeness, scalability, semantic grounding, and utility preservation; the field lacks a shared formal framework – every paper introduces its own agent model, specification language fragment, and evaluation protocol; and specification acquisition and verified re\-planning \(arguably the most important problems\) are the least studied\.

The maturation trajectory of this field parallels the early development of neural network verification \(2017 to 2020\), which similarly began with demonstrations on narrow benchmarks \(MNIST classifiers, small ReLU networks\) before confronting scalability and semantic gap challenges that required fundamental theoretical advances\[[32](https://arxiv.org/html/2608.14590#bib.bib61)\]\. Neural network verification is now a mature subfield with verified industrial applications \(e\.g\., NASA airborne collision avoidance\)\. TheLLMagent verification field is approximately three to four years behind this trajectory, with the additional complication that the*output*ofLLMsisNLrather than a fixed\-dimension vector – making the semantic gap problem structurally harder\.

### 8\.2Practical Implications for Deployment

The evidence base, despite its limitations, supports several practical recommendations for teams deployingLLMagents in consequential settings today\.

REC1: Do not rely on action\-level enforcement alone\.The verifier tax finding\[[47](https://arxiv.org/html/2608.14590#bib.bib45)\]demonstrates that blocking individually unsafe actions does not produce safe task completion\. Any enforcement system deployed in production should measureSSR, not only action conformance\. Enforcement should be supplemented by integrity constraints \(Section[7\.3](https://arxiv.org/html/2608.14590#S7.SS3)\) and human\-in\-the\-loop gates for high\-stakes decisions\.

REC2: Prefer runtime monitoring over static verification for dynamic agents\.For agents that generate plans dynamically \(the majority of production deployments\), static pre\-execution verification is structurally inapplicable\. Runtime monitoring systems \(AgentSpec\[[55](https://arxiv.org/html/2608.14590#bib.bib28)\], Agent\-C\[[31](https://arxiv.org/html/2608.14590#bib.bib27)\]\) offer the best currently available combination of practical deployability and demonstrated safety improvement\. Note that sub\-millisecond per\-action overhead is confirmed only for AgentSpec; other runtime systems have not quantified their overhead \(Table[3](https://arxiv.org/html/2608.14590#S6.T3)\)\.

REC3: Use compositional specification for maintainability\.Safety specifications for agent systems should be organized compositionally by concern domain \(memory integrity, tool protocols, human gates, credential constraints\)\. This compositional organization enables incremental auditing, independent updating of sub\-specifications, and reuse across agent architectures\[[59](https://arxiv.org/html/2608.14590#bib.bib31),[15](https://arxiv.org/html/2608.14590#bib.bib30)\]\.

REC4: Apply probabilistic monitoring for early warning in high\-stakes domains\.In domains where safety violations are severe and irreversible \(autonomous driving, medical decision support, financial transactions\), probabilistic monitoring\[[56](https://arxiv.org/html/2608.14590#bib.bib37)\]provides actionable early warnings withPAC\-style accuracy bounds\. The 38\.66\-second warning demonstrated in autonomous driving corresponds to meaningful intervention time for a human supervisor\.

REC5: Invest in specification quality, not only verification power\.The most sophisticated model checker applied to a semantically incorrect specification provides false assurance\. Teams should invest in specification review and validation \(using interactive disambiguation tools such as NL2Spec\[[11](https://arxiv.org/html/2608.14590#bib.bib20)\]\) before deploying verification infrastructure\. They should treat the specification as a first\-class artifact subject to version control, testing, and peer review\.

### 8\.3Relationship Between Safety Paradigms

The included studies reflect three distinct intellectual traditions for addressingLLMagent safety – traditions that rarely engage in explicit dialogue\.

Theformal methods tradition\(AgentVerify\[[15](https://arxiv.org/html/2608.14590#bib.bib30)\], AgentProof\[[59](https://arxiv.org/html/2608.14590#bib.bib31)\], AutoRocq\[[52](https://arxiv.org/html/2608.14590#bib.bib39)\], VeriGuard\[[43](https://arxiv.org/html/2608.14590#bib.bib29)\]\) draws on 50\+ years of model checking and theorem proving research\. This tradition prioritizes soundness and completeness: if verification says a plan is safe, it*is*safe\. This limitation arises because soundness guarantees depend on the correctness of the specification and the model, andLLMswith non\-negligible semantic error rates constructs both\.

TheMachine Learning \(ML\)safety/alignment tradition\(ConstitutionalAI\[[3](https://arxiv.org/html/2608.14590#bib.bib18)\], Agent Safety Alignment viaRL\[[49](https://arxiv.org/html/2608.14590#bib.bib44)\], Self\-Refine\[[41](https://arxiv.org/html/2608.14590#bib.bib42)\]\) draws on reinforcement learning, RLHF, and iterative refinement\. This tradition prioritizes scalability and generality: trained models implicitly apply safety constraints to arbitrary inputs without per\-deployment specification engineering\. The limitation is the absence of formal guarantees: a model trained to be safe can generate unsafe outputs at inference time, and there is no formal procedure to confirm that it cannot\.

Thesecurity engineering tradition\(LlamaFirewall\[[6](https://arxiv.org/html/2608.14590#bib.bib43)\], AgentGuard\[[33](https://arxiv.org/html/2608.14590#bib.bib38)\]\) draws on systems security, threat modeling, and defensive programming\. This tradition prioritizes adversarial robustness and production deployability: the threat model is an active adversary attempting to exploit the agent, not a passive environment\. The limitation is that this tradition is primarily empirical \(a reduction in attack success rate\) rather than formal \(a provable bound on attack success rate\)\.

Theneed for integrationfollows directly\. Each tradition covers a different part of the safety landscape and has different failure modes\. The most robust deployed systems will combine elements of all three: formal runtime monitors \(providing sound action\-level guarantees\) over aligned base models \(reducing the frequency of violations that reach the monitor\) within hardened system architectures \(defending against adversarial exploitation of the monitoring infrastructure\)\. None of the included systems has yet demonstrated this integration\.

### 8\.4Societal and Ethical Considerations

The deployment of formal verification forLLMagents raises societal and ethical questions that extend beyond technical correctness\. Three concerns merit particular attention: the pressure to deploy unsafe systems, the politics of specification authorship, and the risk of over\-reliance on formal certificates\.

The deployment pressure paradox\.The pace ofLLMagent deployment in production settings far exceeds the pace of formal safety verification’s maturation\. Agents are being deployed in healthcare, legal, and financial settings, whileGRADEcertainty for most verification claims remains*Low*or*Very Low*\. The societal consequence of this gap is that the harm reduction achieved by current verification systems – while real and significant – is not yet formally guaranteed or independently replicated at scale\. Survey findings should inform deployment governance: requiringSSRmeasurement, mandatory specification review, and periodic re\-evaluation against updated benchmarks as agent capabilities evolve\.

Specification as a power structure\.Who writes the formal safety specification for anLLMagent determines which behaviors are permitted and which are blocked\. Specification acquisition at scale \(RG8\) raises governance questions: specifications derived from corporate policy documents may protect business interests at the expense of user interests\. In contrast, those derived from regulatory documents may lag behind technological capabilities\. Transparent, publicly accessible specification libraries with explicit authorship and versioning would reduce the risk of opaque specification capture\.

The completeness illusion\.A formal safety certificate declares: “This agent has been verified against specificationφ\\varphi”, and creates a social expectation of safety that may not be warranted whenφ\\varphifails to capture all relevant safety properties\. Cautionary precedents include the history of aviation \(formal certification of control software that nonetheless crashes due to mode confusion\) and medical devices \(formally verified firmware with verified insecure communication protocols\)\. Formal verification ofLLMagent plans should present a partial safety guarantee conditioned on specification completeness, not a blanket safety assurance\.

### 8\.5Threats to Validity of This Review

This review is subject to several limitations\. We organize them according to four standard validity threats: internal, external, construct, and conclusion validity\.

Internal validity\.The review was conducted by a single reviewer, introducing the risk of subjective selection and data extraction bias\. The authors did not perform an inter\-rater reliability check\. Borderline cases were resolved conservatively \(retain if in doubt\); this strategy may have inflated inclusion counts relative to a dual\-reviewer protocol with explicit disagreement resolution\.

External validity\.We limited the search to six English\-language databases and to papers accessible in full text\. The survey does not capture proprietary industry systems \(e\.g\., OpenAI’s internal safety infrastructure, Google’s production agent safety layer\)\. It also excludes relevant arXiv papers published after 29 May 2026\. The field’s publication pace \(multiple relevant papers per week on arXiv\) means this survey represents a snapshot rather than a complete, up\-to\-date map\.

Construct validity\.TheGRADEframework originated in clinical research, but we adapted it to computer science – a context for which its original designers did not intend it\. The resulting certainty ratings reflect the reviewer’s judgment of construct, internal, and external validity relative to an ideal computer science evidence standard, not a clinical one\. Readers should interpretGRADEratings in this context\.

Conclusion validity\.The narrative synthesis and gap analysis are theory\-driven: the five thematic clusters and ten gaps were identified through the reviewer’s reading of the corpus and may not capture all relevant patterns\. Alternative clustering schemes \(e\.g\., by application domain,LLMarchitecture, or mathematical formalism\) would yield different gap structures\. The research agenda in Section[7](https://arxiv.org/html/2608.14590#S7)should be read as one informed synthesis, not as a definitive enumeration of all open problems\.

## 9Conclusion

This survey has systematically mapped the emerging field of formal verification forLLMagent plans\. Following a PRISMA 2020 protocol over six databases, we identified and synthesized 38 studies spanning specification techniques, verification approaches, enforcement mechanisms, and safety evaluation benchmarks, published between 2022 and 2026\.

### 9\.1Summary of Findings

The synthesis of the reviewed literature reveals four cross\-cutting findings that inform the research agenda\.

The specification bottleneck is real and underaddressed\.Every verification approach that relies on formal properties must first acquire those properties from human\-expressible requirements\.LLM\-basedNL\-to\-formal translation achieves high syntactic correctness \(above90%90\\text\{\\,\}\\mathrm\{\\char 37\\relax\}forLTL; above96%96\\text\{\\,\}\\mathrm\{\\char 37\\relax\}forPDDL\) but low semantic correctness \(24%to35%24\\text\{\\,\}\\mathrm\{\\char 37\\relax\}35\\text\{\\,\}\\mathrm\{\\char 37\\relax\}forPDDL\[[51](https://arxiv.org/html/2608.14590#bib.bib24)\]; comparable forLTL\[[11](https://arxiv.org/html/2608.14590#bib.bib20)\]\)\. Formal verification applied to semantically incorrect specifications provides false assurance rather than genuine safety guarantees\. This gap – between syntactic and semantic correctness in specification translation – is the most fundamental unresolved challenge in the pipeline\.

Runtime monitoring is the most mature sub\-field\.AgentSpec\[[55](https://arxiv.org/html/2608.14590#bib.bib28)\], Agent\-C\[[31](https://arxiv.org/html/2608.14590#bib.bib27)\], LogicGuard\[[22](https://arxiv.org/html/2608.14590#bib.bib36)\], ProbGuard\[[56](https://arxiv.org/html/2608.14590#bib.bib37)\], and VerifyLLM\[[23](https://arxiv.org/html/2608.14590#bib.bib33)\]collectively demonstrate that temporal, probabilistic, and rule\-based runtime monitoring is practical at millisecond overhead and produces significant reductions in unsafe agent actions in closed\-domain settings\. Static verification of workflow graphs \(AgentProof\[[59](https://arxiv.org/html/2608.14590#bib.bib31)\]\) and theorem\-proving\-based policy synthesis \(VeriGuard\[[43](https://arxiv.org/html/2608.14590#bib.bib29)\], AutoRocq\[[52](https://arxiv.org/html/2608.14590#bib.bib39)\]\) provide stronger guarantees but are limited to pre\-specified finite structures\.

The verifier tax is the field’s most consequential empirical finding\.Hard enforcement intercepting up to94%94\\text\{\\,\}\\mathrm\{\\char 37\\relax\}of individually unsafe actions still produces aSSRbelow5%5\\text\{\\,\}\\mathrm\{\\char 37\\relax\}in most settings, as demonstrated in prior work\[[47](https://arxiv.org/html/2608.14590#bib.bib45)\]\. The mechanism is integrity leaks: agents hallucinate user identifiers to bypass authentication checks after direct violations are blocked, thereby finding alternative unsafe paths\. This finding decouples action\-level safety \(what most enforcement papers measure\) from task\-level safety \(what end users and auditors care about\), and remains unaddressed by any existing system\.SSRshould be adopted as the primary evaluation metric going forward\[[47](https://arxiv.org/html/2608.14590#bib.bib45)\]\.

No current approach simultaneously achieves the desiderata\.An ideal verification system forLLMagent plans would be:*soundness\-preserving*\(all violations detected\);*complete*\(no false positives\);*scalable*\(long\-horizon, open\-ended tasks\);*semantically grounded*\(correct specification acquisition\); and*task\-utility\-preserving*\(highSSR\)\. Table[1](https://arxiv.org/html/2608.14590#S4.T1)and the synthesis of Sections[5](https://arxiv.org/html/2608.14590#S5)–[6](https://arxiv.org/html/2608.14590#S6)confirm that no included study satisfies more than three of these five desiderata simultaneously\.

### 9\.2Research Agenda

The ten gaps identified in Section[5\.7](https://arxiv.org/html/2608.14590#S5.SS7)define a structured research agenda\. The three we consider highest priority are:

Semantic correctness in specification translation \(RG1\)\.The65%to76%65\\text\{\\,\}\\mathrm\{\\char 37\\relax\}76\\text\{\\,\}\\mathrm\{\\char 37\\relax\}semantic error rate inNL\-to\-formal translation is a foundational blocker\. Grammar\-constrained decoding, formal equivalence checkers integrated into the translation loop, and semantic ground\-truth benchmarks are the most promising near\-term approaches\.

Task\-level safety and safe re\-planning \(RG3, RG7\)\.The verifier tax problem requires a shift from action\-level to plan\-level safety policies, combined with verified re\-planning mechanisms that generate constraint\-satisfying alternative plan fragments upon detection of violations\. Solving the verifier tax problem is a joint problem in constraint satisfaction, formal synthesis, andLLMplan generation\.

Scalability to long\-horizon plans \(RG2\)\.Current verified systems cover plans of5to305\\text\{\\,\}30\\text\{\\,\}actions\. Long\-horizon agentic tasks require partial verification over safety\-critical sub\-sequences, abstraction\-refinement techniques borrowed from classical model checking, and compositional specification libraries that allow incremental verification as plans grow\.

### 9\.3Principal Contributions Revisited

The five contributions stated in Section[1\.3](https://arxiv.org/html/2608.14590#S1.SS3)– systematic PRISMA coverage, unified three\-level taxonomy, multidimensional comparative analysis, empirical verifier tax synthesis, and the ten\-problem research agenda – have been delivered as described\. Together, Table[1](https://arxiv.org/html/2608.14590#S4.T1), Table[6](https://arxiv.org/html/2608.14590#S6.T6), and the synthesis of Section[6](https://arxiv.org/html/2608.14590#S6)provide the shared vocabulary and gap map needed to guide the next stage of research in this field\.

### 9\.4Limitations

A single reviewer conducted this review without inter\-rater reliability checking, precluding formal risk\-of\-bias agreement statistics\. No meta\-analysis was possible due to the high heterogeneity in metrics, domains, and methods across the included studies\. We limited the search to English\-language, accessible papers; the review does not cover proprietary industry systems or preprints published after May 2026\.GRADEcertainty is predominantly Low to Very Low due to the novelty of the field and the absence of large, independent replications\.

### 9\.5Closing Remarks

The case for formal verification ofLLMagent plans is compelling: agents operating in consequential domains must provide guarantees that go beyond empirical performance on benchmarks\. The case is also technically hard: the stochastic,NL\-native nature ofLLMsresists direct application of classical formal methods\.

The field has made substantial progress in four years, moving from informal safety prompting to runtimeLTLmonitors with millisecond per\-rule overhead\[[55](https://arxiv.org/html/2608.14590#bib.bib28)\], pre\-executionDFAproduct verification over multi\-framework workflow graphs\[[59](https://arxiv.org/html/2608.14590#bib.bib31)\], and probabilistic monitors that warn of violations tens of seconds before they occur\[[56](https://arxiv.org/html/2608.14590#bib.bib37)\]\. But the translation bottleneck, the verifier tax, and the scalability gap remain open – and resolving them will require sustained collaboration among the formal methods,NLprocessing, andAIsafety research communities\.

Through the unified taxonomy, gap analysis, and evidence synthesis presented in this survey, we accelerate that collaboration by providing a shared vocabulary and a clear map of what the field has achieved and what remains to be done\.

## References

- \[1\]\(2022\)Do as i can, not as i say: grounding language in robotic affordances\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2204.01691)Cited by:[2nd item](https://arxiv.org/html/2608.14590#S4.I1.i2.p1.1),[1st item](https://arxiv.org/html/2608.14590#S4.I5.i1.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.13.1),[§5\.2](https://arxiv.org/html/2608.14590#S5.SS2.p3.1)\.
- \[2\]M\. Andriushchenko, A\. Souly, M\. Dziemian, D\. Duenas, M\. Lin, J\. Wang, D\. Hendrycks, A\. Zou, Z\. Kolter, M\. Fredrikson, E\. Winsor, J\. Wynne, Y\. Gal, and X\. Davies\(2024\)AgentHarm: a benchmark for measuring harmfulness of llm agents\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2410.09024)Cited by:[§1](https://arxiv.org/html/2608.14590#S1.p2.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.29.1),[item 3](https://arxiv.org/html/2608.14590#S5.I1.i3.p1.1),[item RG9\.1 – Red\-teaming of verification pipelines\.](https://arxiv.org/html/2608.14590#S7.I9.ix1.p1.1)\.
- \[3\]Y\. Bai, S\. Kadavath,et al\.\(2022\)Constitutional ai: harmlessness from ai feedback\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2212.08073)Cited by:[3rd item](https://arxiv.org/html/2608.14590#S4.I1.i3.p1.1),[4th item](https://arxiv.org/html/2608.14590#S4.I3.i4.p1.1),[5th item](https://arxiv.org/html/2608.14590#S4.I5.i5.p1.1),[item 3](https://arxiv.org/html/2608.14590#S4.I6.i3.p1.3),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.14.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.42.1),[§5\.3](https://arxiv.org/html/2608.14590#S5.SS3.p4.1),[§8\.3](https://arxiv.org/html/2608.14590#S8.SS3.p3.1)\.
- \[4\]D\. Banerjee, O\. Bouissou, and S\. Zetzsche\(2026\)DafnyPro: llm\-assisted automated verification for dafny programs\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2601.05385)Cited by:[2nd item](https://arxiv.org/html/2608.14590#S4.I2.i2.p1.1),[2nd item](https://arxiv.org/html/2608.14590#S4.I5.i2.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.22.1),[§5\.4](https://arxiv.org/html/2608.14590#S5.SS4.p5.5),[Table 5](https://arxiv.org/html/2608.14590#S6.T5.11.11.2.1.1)\.
- \[5\]I\. Beschastnikh, Y\. Brun, S\. Schneider, M\. Sloan, and M\. D\. Ernst\(2011\-09\)Leveraging existing instrumentation to automatically infer invariant\-constrained models\.InProceedings of the 19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineering,ESEC/FSE’11,Szeged, Hungary,pp\. 267–277\.External Links:[Document](https://dx.doi.org/10.1145/2025113.2025151)Cited by:[item RG8\.1 – Specification mining from demonstration traces\.](https://arxiv.org/html/2608.14590#S7.I8.ix1.p1.1)\.
- \[6\]S\. Chennabasappa, C\. Nikolaidis, D\. Song, D\. Molnar, S\. Ding, S\. Wan, S\. Whitman, L\. Deason, N\. Doucette, A\. Montilla, A\. Gampa, B\. de Paola, D\. Gabi, J\. Crnkovich, J\. Testud, K\. He, R\. Chaturvedi, W\. Zhou, and J\. Saxe\(2025\)LlamaFirewall: an open source guardrail system for building secure ai agents\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2505.03574)Cited by:[3rd item](https://arxiv.org/html/2608.14590#S4.I3.i3.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.40.1),[itemRG9\.](https://arxiv.org/html/2608.14590#S5.I2.i9.p1.1),[§5\.5](https://arxiv.org/html/2608.14590#S5.SS5.p3.2),[§6\.3](https://arxiv.org/html/2608.14590#S6.SS3.p6.2),[Table 3](https://arxiv.org/html/2608.14590#S6.T3.1.7.1),[Table 4](https://arxiv.org/html/2608.14590#S6.T4.7.5.2),[§7\.9](https://arxiv.org/html/2608.14590#S7.SS9.p1.1),[§8\.1](https://arxiv.org/html/2608.14590#S8.SS1.p2.1),[§8\.3](https://arxiv.org/html/2608.14590#S8.SS3.p4.1)\.
- \[7\]E\. Clarke, O\. Grumberg, S\. Jha, Y\. Lu, and H\. Veith\(2003\-09\)Counterexample\-guided abstraction refinement for symbolic model checking\.Journal of the ACM50\(5\),pp\. 752–794\.External Links:ISSN 1557\-735X,[Document](https://dx.doi.org/10.1145/876638.876643)Cited by:[item RG2\.2 – Abstraction\-refinement for agent plans\.](https://arxiv.org/html/2608.14590#S7.I2.ix2.p1.1)\.
- \[8\]E\. M\. Clarke and E\. A\. Emerson\(1981\)Design and synthesis of synchronization skeletons using branching\-time temporal logic\.InLogics of Programs, Workshop, Yorktown Heights, New York \(LNCS 131\),Berlin,pp\. 52–71\.External Links:[Document](https://dx.doi.org/10.1007/BFb0025774)Cited by:[§2\.1](https://arxiv.org/html/2608.14590#S2.SS1.p3.4)\.
- \[9\]E\. M\. Clarke, T\. A\. Henzinger, H\. Veith, and R\. Bloem \(Eds\.\)\(2018\)Handbook of model checking\.Springer International Publishing,Cham\.External Links:ISBN 9783319105758,[Document](https://dx.doi.org/10.1007/978-3-319-10575-8)Cited by:[§2\.2](https://arxiv.org/html/2608.14590#S2.SS2.p1.3)\.
- \[10\]J\. M\. Cobleigh, D\. Giannakopoulou, and C\. S\. Păsăreanu\(2003\)Learning assumptions for compositional verification\.InTools and Algorithms for the Construction and Analysis of Systems,pp\. 331–346\.External Links:ISBN 9783540365778,ISSN 0302\-9743,[Document](https://dx.doi.org/10.1007/3-540-36577-x%5F24)Cited by:[item RG2\.3 – Compositional verification with assume\-guarantee contracts\.](https://arxiv.org/html/2608.14590#S7.I2.ix3.p1.1),[item RG5\.1 – Contract\-based interfaces between agents\.](https://arxiv.org/html/2608.14590#S7.I5.ix1.p1.1)\.
- \[11\]M\. Cosler, C\. Hahn, D\. Mendoza, F\. Schmitt, and C\. Trippel\(2023\)Nl2spec: interactively translating unstructured natural language to temporal logics with large language models\.InComputer Aided Verification,pp\. 383–396\.External Links:ISBN 9783031377037,ISSN 1611\-3349,[Document](https://dx.doi.org/10.1007/978-3-031-37703-7%5F18)Cited by:[§2\.1](https://arxiv.org/html/2608.14590#S2.SS1.p2.2),[1st item](https://arxiv.org/html/2608.14590#S4.I1.i1.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.8.1),[itemRG1\.](https://arxiv.org/html/2608.14590#S5.I2.i1.p1.2),[§5\.3](https://arxiv.org/html/2608.14590#S5.SS3.p2.1),[§6\.1](https://arxiv.org/html/2608.14590#S6.SS1.p2.3),[§6\.1](https://arxiv.org/html/2608.14590#S6.SS1.p3.2),[§6\.1](https://arxiv.org/html/2608.14590#S6.SS1.p5.1),[Table 5](https://arxiv.org/html/2608.14590#S6.T5.4.4.3.1.1),[itemRG1\.2](https://arxiv.org/html/2608.14590#S7.I1.i2.p1.1),[item RG8\.2 – Specification extraction from regulatory and policy documents\.](https://arxiv.org/html/2608.14590#S7.I8.ix2.p1.1),[§7\.1](https://arxiv.org/html/2608.14590#S7.SS1.p1.3),[§7\.8](https://arxiv.org/html/2608.14590#S7.SS8.p1.1),[item REC5: Invest in specification quality, not only verification power\.](https://arxiv.org/html/2608.14590#S8.I1.ix5.p1.1),[§8\.1](https://arxiv.org/html/2608.14590#S8.SS1.p2.1),[§9\.1](https://arxiv.org/html/2608.14590#S9.SS1.p2.3)\.
- \[12\]O\. Dedehayir and M\. Steinert\(2016\-07\)The hype cycle model: a review and future directions\.Technological Forecasting and Social Change108,pp\. 28–41\.External Links:ISSN 0040\-1625,[Document](https://dx.doi.org/10.1016/j.techfore.2016.04.005)Cited by:[§8\.1](https://arxiv.org/html/2608.14590#S8.SS1.p1.1)\.
- \[13\]A\. Doshi, Y\. Hong, C\. Xu, E\. Kang, A\. Kapravelos, and C\. Kästner\(2026\)Towards verifiably safe tool use for llm agents\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2601.08012)Cited by:[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.38.1),[§5\.5](https://arxiv.org/html/2608.14590#S5.SS5.p5.1)\.
- \[14\]K\. Erol, J\. Hendler, and D\. S\. Nau\(1996\-03\)Complexity results for htn planning\.Annals of Mathematics and Artificial Intelligence18\(1\),pp\. 69–93\.External Links:ISSN 1573\-7470,[Document](https://dx.doi.org/10.1007/bf02136175)Cited by:[§2\.3](https://arxiv.org/html/2608.14590#S2.SS3.p3.1)\.
- \[15\]E\. Fang\(2026\-04\)AgentVerify: compositional formal verification of ai agent safety properties via ltl model checking\.Preprints\.org1\(1\),pp\. 1–15\.External Links:[Document](https://dx.doi.org/10.20944/preprints202604.1029.v1)Cited by:[§2\.1](https://arxiv.org/html/2608.14590#S2.SS1.p2.2),[§2\.1](https://arxiv.org/html/2608.14590#S2.SS1.p3.4),[§2\.2](https://arxiv.org/html/2608.14590#S2.SS2.p2.3),[1st item](https://arxiv.org/html/2608.14590#S4.I2.i1.p1.1),[3rd item](https://arxiv.org/html/2608.14590#S4.I5.i3.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.17.1),[§5\.4](https://arxiv.org/html/2608.14590#S5.SS4.p2.1),[§6\.5](https://arxiv.org/html/2608.14590#S6.SS5.p1.1),[Table 4](https://arxiv.org/html/2608.14590#S6.T4.9.9.1),[item RG2\.1 – Partial verification of safety\-critical sub\-sequences\.](https://arxiv.org/html/2608.14590#S7.I2.ix1.p1.1),[item RG5\.2 – Protocol verification for inter\-agent communication\.](https://arxiv.org/html/2608.14590#S7.I5.ix2.p1.1),[item RG8\.3 – Compositional specification libraries\.](https://arxiv.org/html/2608.14590#S7.I8.ix3.p1.1),[§7\.5](https://arxiv.org/html/2608.14590#S7.SS5.p1.1),[item REC3: Use compositional specification for maintainability\.](https://arxiv.org/html/2608.14590#S8.I1.ix3.p1.1),[§8\.3](https://arxiv.org/html/2608.14590#S8.SS3.p2.1)\.
- \[16\]Y\. Fang, Z\. Jin, J\. An, H\. Chen, X\. Chen, and N\. Zhan\(2025\)Enhancing transformation from natural language to signal temporal logic using llms with diverse external knowledge\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2505.20658)Cited by:[§2\.1](https://arxiv.org/html/2608.14590#S2.SS1.p4.1),[1st item](https://arxiv.org/html/2608.14590#S4.I1.i1.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.10.1),[§5\.3](https://arxiv.org/html/2608.14590#S5.SS3.p2.1)\.
- \[17\]Y\. Fang, Z\. Jin, J\. An, H\. Chen, X\. Chen, and N\. Zhan\(2026\)ClarifySTL: an interactive llm agent framework for stl transformation through requirements clarification\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2605.01209)Cited by:[§2\.1](https://arxiv.org/html/2608.14590#S2.SS1.p4.1),[1st item](https://arxiv.org/html/2608.14590#S4.I1.i1.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.11.1),[§5\.3](https://arxiv.org/html/2608.14590#S5.SS3.p2.1),[§6\.1](https://arxiv.org/html/2608.14590#S6.SS1.p5.1),[§7\.1](https://arxiv.org/html/2608.14590#S7.SS1.p1.3)\.
- \[18\]R\. E\. Fikes and N\. J\. Nilsson\(1971\)STRIPS: a new approach to the application of theorem proving to problem solving\.Artificial Intelligence2\(3–4\),pp\. 189–208\.External Links:[Document](https://dx.doi.org/10.1016/0004-3702%2871%2990010-5)Cited by:[§2\.3](https://arxiv.org/html/2608.14590#S2.SS3.p3.1)\.
- \[19\]M\. Fox, A\. Gerevini, D\. Long, and I\. Serina\(2006\)Plan stability: replanning versus plan repair\.InProceedings of the Sixteenth International Conference on Automated Planning and Scheduling,ICAPS’06,Cumbria, UK,pp\. 212–221\.External Links:ISBN 9781577352709Cited by:[item RG7\.1 – Constraint\-satisfying plan repair\.](https://arxiv.org/html/2608.14590#S7.I7.ix1.p1.1)\.
- \[20\]S\. Geng, M\. Josifoski, M\. Peyrard, and R\. West\(2023\)Grammar\-constrained decoding for structured nlp tasks without finetuning\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2305.13971)Cited by:[itemRG1\.1](https://arxiv.org/html/2608.14590#S7.I1.i1.p1.1)\.
- \[21\]A\. E\. Gerevini\(2020\-03\)An introduction to the planning domain definition language \(pddl\): book review\.Artificial Intelligence280,pp\. 103221\.External Links:ISSN 0004\-3702,[Document](https://dx.doi.org/10.1016/j.artint.2019.103221)Cited by:[§2\.3](https://arxiv.org/html/2608.14590#S2.SS3.p2.1)\.
- \[22\]A\. Gokhale, V\. Srivastava, and F\. Bullo\(2025\)LogicGuard: improving embodied llm agents through temporal logic based critics\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2507.03293)Cited by:[§2\.1](https://arxiv.org/html/2608.14590#S2.SS1.p2.2),[1st item](https://arxiv.org/html/2608.14590#S4.I3.i1.p1.1),[2nd item](https://arxiv.org/html/2608.14590#S4.I4.i2.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.35.1),[§5\.4](https://arxiv.org/html/2608.14590#S5.SS4.p4.7),[§6\.2](https://arxiv.org/html/2608.14590#S6.SS2.p3.2),[Table 3](https://arxiv.org/html/2608.14590#S6.T3.1.5.1),[§9\.1](https://arxiv.org/html/2608.14590#S9.SS1.p3.1)\.
- \[23\]D\. S\. Grigorev, A\. K\. Kovalev, and A\. I\. Panov\(2025\)VerifyLLM: llm\-based pre\-execution task plan verification for robots\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2507.05118)Cited by:[§2\.1](https://arxiv.org/html/2608.14590#S2.SS1.p2.2),[1st item](https://arxiv.org/html/2608.14590#S4.I3.i1.p1.1),[1st item](https://arxiv.org/html/2608.14590#S4.I4.i1.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.36.1),[§5\.2](https://arxiv.org/html/2608.14590#S5.SS2.p2.1),[§5\.4](https://arxiv.org/html/2608.14590#S5.SS4.p4.7),[§6\.2](https://arxiv.org/html/2608.14590#S6.SS2.p3.2),[Table 3](https://arxiv.org/html/2608.14590#S6.T3.1.6.1),[§7\.2](https://arxiv.org/html/2608.14590#S7.SS2.p1.2),[§9\.1](https://arxiv.org/html/2608.14590#S9.SS1.p3.1)\.
- \[24\]G\. H\. Guyatt, A\. D\. Oxman, G\. E\. Vist, R\. Kunz, Y\. Falck\-Ytter, P\. Alonso\-Coello, H\. J\. Schünemann, and GRADE Working Group\(2008\)GRADE: an emerging consensus on rating quality of evidence and strength of recommendations\.BMJ336\(7650\),pp\. 924–926\.External Links:[Document](https://dx.doi.org/10.1136/bmj.39489.470347.AD)Cited by:[item 3](https://arxiv.org/html/2608.14590#S1.I3.i3.p1.1)\.
- \[25\]H\. Hansson and B\. Jonsson\(1994\)A logic for reasoning about time and reliability\.Formal Aspects of Computing6\(5\),pp\. 512–535\.External Links:[Document](https://dx.doi.org/10.1007/BF01211866)Cited by:[§2\.1](https://arxiv.org/html/2608.14590#S2.SS1.p5.3)\.
- \[26\]A\. Hariharan, V\. Dongre, D\. Hakkani\-Tür, and G\. Tur\(2025\)Plan verification for llm\-based embodied task completion agents\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2509.02761)Cited by:[4th item](https://arxiv.org/html/2608.14590#S4.I2.i4.p1.1),[3rd item](https://arxiv.org/html/2608.14590#S4.I4.i3.p1.1),[5th item](https://arxiv.org/html/2608.14590#S4.I5.i5.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.27.1),[§5\.4](https://arxiv.org/html/2608.14590#S5.SS4.p5.5)\.
- \[27\]J\. He, K\. Baraka, F\. Saraoglu, R\. Alami, S\. Lemaignan, and S\. Booth\(2023\)NL2LTL — A Python package for converting natural language \(NL\) instructions to linear temporal logic \(LTL\) formulas\.InProceedings of the Thirty\-Seventh AAAI Conference on Artificial Intelligence \(AAAI 2023\),Washington, DC, USA,pp\. 16529–16530\.External Links:[Document](https://dx.doi.org/10.1609/aaai.v37i13.27068)Cited by:[§2\.1](https://arxiv.org/html/2608.14590#S2.SS1.p2.2),[1st item](https://arxiv.org/html/2608.14590#S4.I1.i1.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.7.1),[§5\.3](https://arxiv.org/html/2608.14590#S5.SS3.p2.1),[§6\.1](https://arxiv.org/html/2608.14590#S6.SS1.p2.3),[Table 5](https://arxiv.org/html/2608.14590#S6.T5.4.4.3.1.1),[§7\.8](https://arxiv.org/html/2608.14590#S7.SS8.p1.1),[§8\.1](https://arxiv.org/html/2608.14590#S8.SS1.p2.1)\.
- \[28\]K\. Honda, N\. Yoshida, and M\. Carbone\(2008\-01\)Multiparty asynchronous session types\.InProceedings of the 35th annual ACM SIGPLAN\-SIGACT symposium on Principles of programming languages,POPL08,San Francisco, CA, USA,pp\. 273–284\.External Links:[Document](https://dx.doi.org/10.1145/1328438.1328472)Cited by:[item RG5\.2 – Protocol verification for inter\-agent communication\.](https://arxiv.org/html/2608.14590#S7.I5.ix2.p1.1)\.
- \[29\]R\. Howey, D\. Long, and M\. Fox\(2004\)VAL: automatic plan validation, continuing research on the development of language independent plan validators\.InProceedings of the 16th IEEE International Conference on Tools with Artificial Intelligence \(ICTAI 2004\),Los Alamitos, CA, USA,pp\. 294–301\.External Links:[Document](https://dx.doi.org/10.1109/ICTAI.2004.110)Cited by:[§2\.3](https://arxiv.org/html/2608.14590#S2.SS3.p2.1)\.
- \[30\]X\. Huang, W\. Liu, X\. Chen, X\. Wang, H\. Wang, D\. Lian, Y\. Wang, R\. Tang, and E\. Chen\(2024\)Understanding the planning of llm agents: a survey\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2402.02716)Cited by:[§4\.6](https://arxiv.org/html/2608.14590#S4.SS6.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.5.1),[§5\.2](https://arxiv.org/html/2608.14590#S5.SS2.p4.1),[Table 2](https://arxiv.org/html/2608.14590#S5.T2.1.4.1)\.
- \[31\]A\. Kamath, S\. Zhang, C\. Xu, S\. Ugare, G\. Singh, and S\. Misailovic\(2025\)Enforcing temporal constraints for llm agents\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2512.23738)Cited by:[§1](https://arxiv.org/html/2608.14590#S1.p1.1),[§2\.1](https://arxiv.org/html/2608.14590#S2.SS1.p2.2),[1st item](https://arxiv.org/html/2608.14590#S4.I3.i1.p1.1),[2nd item](https://arxiv.org/html/2608.14590#S4.I4.i2.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.33.1),[§5\.4](https://arxiv.org/html/2608.14590#S5.SS4.p4.7),[§5\.5](https://arxiv.org/html/2608.14590#S5.SS5.p2.1),[§6\.2](https://arxiv.org/html/2608.14590#S6.SS2.p3.2),[Table 3](https://arxiv.org/html/2608.14590#S6.T3.1.3.1),[Table 4](https://arxiv.org/html/2608.14590#S6.T4.4.2.2),[Table 5](https://arxiv.org/html/2608.14590#S6.T5.6.6.2.1.1),[item RG3\.1 – Plan\-level safety policies\.](https://arxiv.org/html/2608.14590#S7.I3.ix1.p1.1),[item RG7\.2 – ConstrainedLLMplan generation\.](https://arxiv.org/html/2608.14590#S7.I7.ix2.p1.1),[§7\.2](https://arxiv.org/html/2608.14590#S7.SS2.p1.2),[§7\.3](https://arxiv.org/html/2608.14590#S7.SS3.p1.3),[item REC2: Prefer runtime monitoring over static verification for dynamic agents\.](https://arxiv.org/html/2608.14590#S8.I1.ix2.p1.1),[§8\.1](https://arxiv.org/html/2608.14590#S8.SS1.p2.1),[§9\.1](https://arxiv.org/html/2608.14590#S9.SS1.p3.1)\.
- \[32\]G\. Katz, C\. Barrett, D\. L\. Dill, K\. Julian, and M\. J\. Kochenderfer\(2017\)Reluplex: an efficient smt solver for verifying deep neural networks\.InComputer Aided Verification,pp\. 97–117\.External Links:ISBN 9783319633879,ISSN 1611\-3349,[Document](https://dx.doi.org/10.1007/978-3-319-63387-9%5F5)Cited by:[§8\.1](https://arxiv.org/html/2608.14590#S8.SS1.p4.1)\.
- \[33\]R\. Koohestani\(2025\)AgentGuard: runtime verification of ai agents\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2509.23864)Cited by:[itemRG9\.](https://arxiv.org/html/2608.14590#S5.I2.i9.p1.1),[§5\.4](https://arxiv.org/html/2608.14590#S5.SS4.p4.7),[§6\.3](https://arxiv.org/html/2608.14590#S6.SS3.p6.2),[Table 4](https://arxiv.org/html/2608.14590#S6.T4.8.6.2),[§7\.5](https://arxiv.org/html/2608.14590#S7.SS5.p1.1),[§7\.9](https://arxiv.org/html/2608.14590#S7.SS9.p1.1),[§8\.3](https://arxiv.org/html/2608.14590#S8.SS3.p4.1)\.
- \[34\]M\. Kwiatkowska, G\. Norman, and D\. Parker\(2011\)PRISM 4\.0: verification of probabilistic real\-time systems\.InProceedings of the 23rd International Conference on Computer Aided Verification \(CAV 2011\), LNCS 6806,Berlin, Heidelberg,pp\. 585–591\.External Links:[Document](https://dx.doi.org/10.1007/978-3-642-22110-1%5F47)Cited by:[§2\.2](https://arxiv.org/html/2608.14590#S2.SS2.p4.1)\.
- \[35\]C\. P\. Lee, D\. Porfirio, X\. J\. Wang, K\. C\. Zhao, and B\. Mutlu\(2025\-04\)VeriPlan: integrating formal verification and llms into end\-user planning\.InProceedings of the 2025 CHI Conference on Human Factors in Computing Systems,CHI ’25,Yokohama, Japan,pp\. 1–19\.External Links:[Document](https://dx.doi.org/10.1145/3706598.3714113)Cited by:[1st item](https://arxiv.org/html/2608.14590#S4.I2.i1.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.19.1),[§5\.4](https://arxiv.org/html/2608.14590#S5.SS4.p2.1),[item RG3\.3 – Safe replanning upon violation\.](https://arxiv.org/html/2608.14590#S7.I3.ix3.p1.1),[§7\.7](https://arxiv.org/html/2608.14590#S7.SS7.p1.1)\.
- \[36\]X\. Leroy\(2009\-07\)Formal verification of a realistic compiler\.Communications of the ACM52\(7\),pp\. 107–115\.External Links:ISSN 1557\-7317,[Document](https://dx.doi.org/10.1145/1538788.1538814)Cited by:[item RG9\.2 – Formal robustness guarantees for specification translators\.](https://arxiv.org/html/2608.14590#S7.I9.ix2.p1.1)\.
- \[37\]Y\. C\. Li, S\. Zetzsche, and S\. Somayyajula\(2025\)Dafny as verification\-aware intermediate language for code generation\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2501.06283)Cited by:[§2\.4](https://arxiv.org/html/2608.14590#S2.SS4.p2.1),[2nd item](https://arxiv.org/html/2608.14590#S4.I2.i2.p1.1),[2nd item](https://arxiv.org/html/2608.14590#S4.I5.i2.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.21.1),[§5\.4](https://arxiv.org/html/2608.14590#S5.SS4.p5.5)\.
- \[38\]J\. Lim, M\. T\. Anbarani, R\. Meira\-Góes, and I\. Kovalenko\(2026\)Logic\-based verification of task allocation for llm\-enabled multi\-agent manufacturing systems\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2604.17142)Cited by:[§2\.3](https://arxiv.org/html/2608.14590#S2.SS3.p3.1),[§2\.4](https://arxiv.org/html/2608.14590#S2.SS4.p4.1),[1st item](https://arxiv.org/html/2608.14590#S4.I2.i1.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.18.1),[itemRG5\.](https://arxiv.org/html/2608.14590#S5.I2.i5.p1.1),[§5\.4](https://arxiv.org/html/2608.14590#S5.SS4.p2.1),[§7\.5](https://arxiv.org/html/2608.14590#S7.SS5.p1.1)\.
- \[39\]X\. Liu, H\. Yu, H\. Zhang, Y\. Xu, X\. Lei, H\. Lai, Y\. Gu, H\. Ding, K\. Men, K\. Yang, S\. Zhang, X\. Deng, A\. Zeng, Z\. Du, C\. Zhang, S\. Shen, T\. Zhang, Y\. Su, H\. Sun, M\. Huang, Y\. Dong, and J\. Tang\(2023\)AgentBench: evaluating llms as agents\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2308.03688)Cited by:[§1](https://arxiv.org/html/2608.14590#S1.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.30.1),[item 1](https://arxiv.org/html/2608.14590#S5.I1.i1.p1.1),[§7\.10](https://arxiv.org/html/2608.14590#S7.SS10.p1.1)\.
- \[40\]Z\. Ma, C\. Wen, Z\. Su, X\. Liang, C\. Tian, S\. Qin, and M\. Yang\(2025\)Bridging natural language and formal specification–automated translation of software requirements to ltl via hierarchical semantics decomposition using llms\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2512.17334)Cited by:[1st item](https://arxiv.org/html/2608.14590#S4.I1.i1.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.9.1),[§5\.3](https://arxiv.org/html/2608.14590#S5.SS3.p2.1),[§6\.1](https://arxiv.org/html/2608.14590#S6.SS1.p2.3),[§6\.1](https://arxiv.org/html/2608.14590#S6.SS1.p3.2),[§6\.1](https://arxiv.org/html/2608.14590#S6.SS1.p5.1),[Table 5](https://arxiv.org/html/2608.14590#S6.T5.4.4.3.1.1),[§7\.1](https://arxiv.org/html/2608.14590#S7.SS1.p1.3)\.
- \[41\]A\. Madaan, N\. Tandon, P\. Gupta, S\. Hallinan, L\. Gao, S\. Wiegreffe, U\. Alon, N\. Dziri, S\. Prabhumoye, Y\. Yang, S\. Gupta, B\. P\. Majumder, K\. Hermann, S\. Welleck, A\. Yazdanbakhsh, and P\. Clark\(2023\)Self\-refine: iterative refinement with self\-feedback\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2303.17651)Cited by:[4th item](https://arxiv.org/html/2608.14590#S4.I2.i4.p1.1),[3rd item](https://arxiv.org/html/2608.14590#S4.I4.i3.p1.1),[5th item](https://arxiv.org/html/2608.14590#S4.I5.i5.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.26.1),[§5\.4](https://arxiv.org/html/2608.14590#S5.SS4.p5.5),[Table 5](https://arxiv.org/html/2608.14590#S6.T5.10.10.3.1.1),[§8\.3](https://arxiv.org/html/2608.14590#S8.SS3.p3.1)\.
- \[42\]O\. Maler and D\. Nickovic\(2004\)Monitoring temporal properties of continuous signals\.InFormal Techniques, Modelling and Analysis of Timed and Fault\-Tolerant Systems \(FORMATS/FTRTFT 2004\), LNCS 3253,Berlin, Heidelberg,pp\. 152–166\.External Links:[Document](https://dx.doi.org/10.1007/978-3-540-30206-3%5F12)Cited by:[§2\.1](https://arxiv.org/html/2608.14590#S2.SS1.p4.1)\.
- \[43\]L\. Miculicich, M\. Parmar, H\. Palangi, K\. D\. Dvijotham, M\. Montanari, T\. Pfister, and L\. T\. Le\(2025\)VeriGuard: enhancing llm agent safety via verified code generation\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2510.05156)Cited by:[§1](https://arxiv.org/html/2608.14590#S1.p1.1),[§2\.4](https://arxiv.org/html/2608.14590#S2.SS4.p2.1),[3rd item](https://arxiv.org/html/2608.14590#S4.I2.i3.p1.1),[1st item](https://arxiv.org/html/2608.14590#S4.I4.i1.p1.1),[2nd item](https://arxiv.org/html/2608.14590#S4.I5.i2.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.23.1),[§5\.4](https://arxiv.org/html/2608.14590#S5.SS4.p3.2),[§6\.2](https://arxiv.org/html/2608.14590#S6.SS2.p2.1),[§6\.2](https://arxiv.org/html/2608.14590#S6.SS2.p4.1),[Table 4](https://arxiv.org/html/2608.14590#S6.T4.9.7.2),[§7\.4](https://arxiv.org/html/2608.14590#S7.SS4.p1.1),[§8\.3](https://arxiv.org/html/2608.14590#S8.SS3.p2.1),[§9\.1](https://arxiv.org/html/2608.14590#S9.SS1.p3.1)\.
- \[44\]M\. J\. Page, J\. E\. McKenzie,et al\.\(2021\)The PRISMA 2020 statement: an updated guideline for reporting systematic reviews\.BMJ372,pp\. n71\.External Links:[Document](https://dx.doi.org/10.1136/bmj.n71)Cited by:[§3](https://arxiv.org/html/2608.14590#S3.p1.1)\.
- \[45\]A\. Pnueli\(1977\)The temporal logic of programs\.InProceedings of the 18th Annual Symposium on Foundations of Computer Science \(FOCS 1977\),Los Alamitos, CA, USA,pp\. 46–57\.External Links:[Document](https://dx.doi.org/10.1109/SFCS.1977.32)Cited by:[§2\.1](https://arxiv.org/html/2608.14590#S2.SS1.p1.1),[§2\.1](https://arxiv.org/html/2608.14590#S2.SS1.p2.2)\.
- \[46\]K\. Ramani, V\. Tawosi, S\. Alamir, and D\. Borrajo\(2025\)Bridging llm planning agents and formal methods: a case study in plan verification\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2510.03469)Cited by:[§1](https://arxiv.org/html/2608.14590#S1.p3.1),[§2\.2](https://arxiv.org/html/2608.14590#S2.SS2.p2.3),[1st item](https://arxiv.org/html/2608.14590#S4.I2.i1.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.16.1),[§5\.2](https://arxiv.org/html/2608.14590#S5.SS2.p2.1),[§5\.4](https://arxiv.org/html/2608.14590#S5.SS4.p2.1),[§6\.1](https://arxiv.org/html/2608.14590#S6.SS1.p2.3),[Table 5](https://arxiv.org/html/2608.14590#S6.T5.4.4.3.1.1)\.
- \[47\]T\. Sah, V\. Srivastava, D\. Sah, and K\. Jordan\(2026\)The verifier tax: horizon dependent safety success tradeoffs in tool using llm agents\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2603.19328)Cited by:[item 4](https://arxiv.org/html/2608.14590#S1.I3.i4.p1.1),[§1](https://arxiv.org/html/2608.14590#S1.p3.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.37.1),[itemRG3\.](https://arxiv.org/html/2608.14590#S5.I2.i3.p1.2),[§5\.5](https://arxiv.org/html/2608.14590#S5.SS5.p4.3),[§6\.3](https://arxiv.org/html/2608.14590#S6.SS3.p1.1),[§6\.3](https://arxiv.org/html/2608.14590#S6.SS3.p3.1),[Table 5](https://arxiv.org/html/2608.14590#S6.T5.8.8.1.1.1),[item RG10\.2 – Adoption ofSSRas the primary metric\.](https://arxiv.org/html/2608.14590#S7.I10.ix2.p1.1),[§7\.10](https://arxiv.org/html/2608.14590#S7.SS10.p1.1),[§7\.3](https://arxiv.org/html/2608.14590#S7.SS3.p1.3),[item REC1: Do not rely on action\-level enforcement alone\.](https://arxiv.org/html/2608.14590#S8.I1.ix1.p1.1),[§8\.1](https://arxiv.org/html/2608.14590#S8.SS1.p1.1),[§8\.1](https://arxiv.org/html/2608.14590#S8.SS1.p2.1),[§9\.1](https://arxiv.org/html/2608.14590#S9.SS1.p4.2),[Definition 3](https://arxiv.org/html/2608.14590#Thmdefinition3.p1.3)\.
- \[48\]T\. Schick, J\. Dwivedi\-Yu, R\. Dessì, R\. Raileanu, M\. Lomeli, L\. Zettlemoyer, N\. Cancedda, and T\. Scialom\(2023\)Toolformer: language models can teach themselves to use tools\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2302.04761)Cited by:[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.3.1),[§5\.2](https://arxiv.org/html/2608.14590#S5.SS2.p3.1)\.
- \[49\]Z\. Sha, H\. Tian, Z\. Xu, S\. Cui, C\. Meng, and W\. Wang\(2025\)Agent safety alignment via reinforcement learning\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2507.08270)Cited by:[3rd item](https://arxiv.org/html/2608.14590#S4.I1.i3.p1.1),[4th item](https://arxiv.org/html/2608.14590#S4.I3.i4.p1.1),[5th item](https://arxiv.org/html/2608.14590#S4.I5.i5.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.43.1),[§5\.5](https://arxiv.org/html/2608.14590#S5.SS5.p3.2),[§8\.3](https://arxiv.org/html/2608.14590#S8.SS3.p3.1)\.
- \[50\]A\. Solar\-Lezama, L\. Tancau, R\. Bodik, S\. Seshia, and V\. Saraswat\(2006\-10\)Combinatorial sketching for finite programs\.InProceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems,ASPLOS06,San Jose, CA, USA,pp\. 404–415\.External Links:[Document](https://dx.doi.org/10.1145/1168857.1168907)Cited by:[itemRG1\.2](https://arxiv.org/html/2608.14590#S7.I1.i2.p1.1)\.
- \[51\]M\. Tantakoun, X\. Zhu, and C\. Muise\(2025\)LLMs as planning formalizers: a survey for leveraging large language models to construct automated planning models\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2503.18971)Cited by:[§1](https://arxiv.org/html/2608.14590#S1.p3.1),[§2\.3](https://arxiv.org/html/2608.14590#S2.SS3.p2.1),[2nd item](https://arxiv.org/html/2608.14590#S4.I1.i2.p1.1),[1st item](https://arxiv.org/html/2608.14590#S4.I5.i1.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.12.1),[itemRG1\.](https://arxiv.org/html/2608.14590#S5.I2.i1.p1.2),[§5\.2](https://arxiv.org/html/2608.14590#S5.SS2.p2.1),[§5\.3](https://arxiv.org/html/2608.14590#S5.SS3.p3.2),[§6\.1](https://arxiv.org/html/2608.14590#S6.SS1.p2.3),[§6\.1](https://arxiv.org/html/2608.14590#S6.SS1.p3.2),[Table 5](https://arxiv.org/html/2608.14590#S6.T5.5.5.2.1.1),[§7\.1](https://arxiv.org/html/2608.14590#S7.SS1.p1.3),[§9\.1](https://arxiv.org/html/2608.14590#S9.SS1.p2.3)\.
- \[52\]H\. Tu, H\. Zhao, Y\. Song, M\. Zafar, R\. Meng, and A\. Roychoudhury\(2025\)Agentic verification of software systems\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2511.17330)Cited by:[3rd item](https://arxiv.org/html/2608.14590#S4.I2.i3.p1.1),[2nd item](https://arxiv.org/html/2608.14590#S4.I5.i2.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.24.1),[§5\.4](https://arxiv.org/html/2608.14590#S5.SS4.p3.2),[§8\.3](https://arxiv.org/html/2608.14590#S8.SS3.p2.1),[§9\.1](https://arxiv.org/html/2608.14590#S9.SS1.p3.1)\.
- \[53\]K\. Valmeekam, M\. Marquez, A\. Olmo, S\. Sreedharan, and S\. Kambhampati\(2022\)PlanBench: an extensible benchmark for evaluating large language models on planning and reasoning about change\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2206.10498)Cited by:[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.31.1),[item 4](https://arxiv.org/html/2608.14590#S5.I1.i4.p1.1),[§5\.3](https://arxiv.org/html/2608.14590#S5.SS3.p3.2)\.
- \[54\]V\. Vovk, A\. Gammerman, and G\. Shafer\(2005\)Algorithmic learning in a random world\.Springer\-Verlag,New York\.External Links:ISBN 0387001522,[Document](https://dx.doi.org/10.1007/b106715)Cited by:[item RG6\.2 – Calibrated uncertainty quantification for safety monitors\.](https://arxiv.org/html/2608.14590#S7.I6.ix2.p1.1)\.
- \[55\]H\. Wang, C\. M\. Poskitt, and J\. Sun\(2025\)AgentSpec: customizable runtime enforcement for safe and reliable llm agents\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2503.18666)Cited by:[1st item](https://arxiv.org/html/2608.14590#S4.I3.i1.p1.1),[2nd item](https://arxiv.org/html/2608.14590#S4.I4.i2.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.34.1),[§5\.4](https://arxiv.org/html/2608.14590#S5.SS4.p4.7),[§5\.5](https://arxiv.org/html/2608.14590#S5.SS5.p2.1),[§6\.2](https://arxiv.org/html/2608.14590#S6.SS2.p3.2),[§6\.2](https://arxiv.org/html/2608.14590#S6.SS2.p5.1),[Table 3](https://arxiv.org/html/2608.14590#S6.T3.1.2.1),[Table 4](https://arxiv.org/html/2608.14590#S6.T4.3.1.2),[Table 5](https://arxiv.org/html/2608.14590#S6.T5.6.6.2.1.1),[§7\.2](https://arxiv.org/html/2608.14590#S7.SS2.p1.2),[§7\.3](https://arxiv.org/html/2608.14590#S7.SS3.p1.3),[item REC2: Prefer runtime monitoring over static verification for dynamic agents\.](https://arxiv.org/html/2608.14590#S8.I1.ix2.p1.1),[§8\.1](https://arxiv.org/html/2608.14590#S8.SS1.p2.1),[§9\.1](https://arxiv.org/html/2608.14590#S9.SS1.p3.1),[§9\.5](https://arxiv.org/html/2608.14590#S9.SS5.p2.1)\.
- \[56\]H\. Wang, C\. M\. Poskitt, J\. Wei, and J\. Sun\(2025\)ProbGuard: probabilistic runtime monitoring for llm agent safety\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2508.00500)Cited by:[§1](https://arxiv.org/html/2608.14590#S1.p1.1),[§2\.1](https://arxiv.org/html/2608.14590#S2.SS1.p5.3),[§2\.2](https://arxiv.org/html/2608.14590#S2.SS2.p4.1),[2nd item](https://arxiv.org/html/2608.14590#S4.I3.i2.p1.1),[2nd item](https://arxiv.org/html/2608.14590#S4.I4.i2.p1.1),[4th item](https://arxiv.org/html/2608.14590#S4.I5.i4.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.39.1),[itemRG6\.](https://arxiv.org/html/2608.14590#S5.I2.i6.p1.1),[§5\.4](https://arxiv.org/html/2608.14590#S5.SS4.p4.7),[§6\.2](https://arxiv.org/html/2608.14590#S6.SS2.p3.2),[§6\.4](https://arxiv.org/html/2608.14590#S6.SS4.p1.1),[Table 3](https://arxiv.org/html/2608.14590#S6.T3.1.4.1),[Table 4](https://arxiv.org/html/2608.14590#S6.T4.9.10.1),[Table 5](https://arxiv.org/html/2608.14590#S6.T5.11.13.2.1.1),[§7\.6](https://arxiv.org/html/2608.14590#S7.SS6.p1.1),[item REC4: Apply probabilistic monitoring for early warning in high\-stakes domains\.](https://arxiv.org/html/2608.14590#S8.I1.ix4.p1.1),[§9\.1](https://arxiv.org/html/2608.14590#S9.SS1.p3.1),[§9\.5](https://arxiv.org/html/2608.14590#S9.SS5.p2.1)\.
- \[57\]K\. Wang, G\. Zhang,et al\.\(2025\)A comprehensive survey in llm\(\-agent\) full stack safety: data, training and deployment\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2504.15585)Cited by:[3rd item](https://arxiv.org/html/2608.14590#S4.I3.i3.p1.1),[5th item](https://arxiv.org/html/2608.14590#S4.I5.i5.p1.1),[§4\.6](https://arxiv.org/html/2608.14590#S4.SS6.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.41.1),[§5\.4](https://arxiv.org/html/2608.14590#S5.SS4.p5.5),[Table 2](https://arxiv.org/html/2608.14590#S5.T2.1.3.1),[§7\.9](https://arxiv.org/html/2608.14590#S7.SS9.p1.1)\.
- \[58\]J\. Wei, X\. Wang, D\. Schuurmans, M\. Bosma, B\. Ichter, F\. Xia, E\. Chi, Q\. Le, and D\. Zhou\(2022\)Chain\-of\-thought prompting elicits reasoning in large language models\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2201.11903)Cited by:[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.4.1),[§5\.2](https://arxiv.org/html/2608.14590#S5.SS2.p2.1)\.
- \[59\]M\. Xavier, V\. M\. A, M\. Jolly, and M\. Xavier\(2026\)Agentproof: static verification of agent workflow graphs\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2603.20356)Cited by:[§2\.2](https://arxiv.org/html/2608.14590#S2.SS2.p3.3),[§2\.4](https://arxiv.org/html/2608.14590#S2.SS4.p2.1),[2nd item](https://arxiv.org/html/2608.14590#S4.I2.i2.p1.1),[1st item](https://arxiv.org/html/2608.14590#S4.I4.i1.p1.1),[3rd item](https://arxiv.org/html/2608.14590#S4.I5.i3.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.20.1),[§5\.2](https://arxiv.org/html/2608.14590#S5.SS2.p4.1),[§5\.4](https://arxiv.org/html/2608.14590#S5.SS4.p3.2),[§6\.2](https://arxiv.org/html/2608.14590#S6.SS2.p2.1),[§6\.5](https://arxiv.org/html/2608.14590#S6.SS5.p1.1),[Table 4](https://arxiv.org/html/2608.14590#S6.T4.6.4.3),[Table 5](https://arxiv.org/html/2608.14590#S6.T5.7.7.2.1.1),[item RG2\.3 – Compositional verification with assume\-guarantee contracts\.](https://arxiv.org/html/2608.14590#S7.I2.ix3.p1.1),[item RG4\.1 – Online workflow graph extraction\.](https://arxiv.org/html/2608.14590#S7.I4.ix1.p1.1),[§7\.2](https://arxiv.org/html/2608.14590#S7.SS2.p1.2),[§7\.4](https://arxiv.org/html/2608.14590#S7.SS4.p1.1),[item REC3: Use compositional specification for maintainability\.](https://arxiv.org/html/2608.14590#S8.I1.ix3.p1.1),[§8\.3](https://arxiv.org/html/2608.14590#S8.SS3.p2.1),[§9\.1](https://arxiv.org/html/2608.14590#S9.SS1.p3.1),[§9\.5](https://arxiv.org/html/2608.14590#S9.SS5.p2.1)\.
- \[60\]S\. Yao, N\. Shinn, P\. Razavi, and K\. Narasimhan\(2024\)τ\\tau\-Bench: a benchmark for tool\-agent\-user interaction in real\-world domains\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2406.12045)Cited by:[item 5](https://arxiv.org/html/2608.14590#S5.I1.i5.p1.1),[§5\.5](https://arxiv.org/html/2608.14590#S5.SS5.p4.3),[§6\.3](https://arxiv.org/html/2608.14590#S6.SS3.p2.3),[§7\.10](https://arxiv.org/html/2608.14590#S7.SS10.p1.1),[§8\.1](https://arxiv.org/html/2608.14590#S8.SS1.p2.1)\.
- \[61\]S\. Yao, J\. Zhao, D\. Yu, N\. Du, I\. Shafran, K\. Narasimhan, and Y\. Cao\(2022\)ReAct: synergizing reasoning and acting in language models\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2210.03629)Cited by:[§2\.4](https://arxiv.org/html/2608.14590#S2.SS4.p2.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.25.1),[§5\.2](https://arxiv.org/html/2608.14590#S5.SS2.p2.1)\.
- \[62\]Y\. Zhang, Y\. Cai, X\. Zuo, X\. Luan, K\. Wang, Z\. Hou, Y\. Zhang, Z\. Wei, M\. Sun, J\. Sun, J\. Sun, and J\. S\. Dong\(2024\)The fusion of large language models and formal methods for trustworthy ai agents: a roadmap\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2412.06512)Cited by:[§4\.6](https://arxiv.org/html/2608.14590#S4.SS6.p1.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.6.1),[§5\.3](https://arxiv.org/html/2608.14590#S5.SS3.p5.1),[Table 2](https://arxiv.org/html/2608.14590#S5.T2.1.2.1)\.
- \[63\]Z\. Zhang, S\. Cui, Y\. Lu, J\. Zhou, J\. Yang, H\. Wang, and M\. Huang\(2024\)Agent\-safetybench: evaluating the safety of llm agents\.arXiv\.External Links:[Document](https://dx.doi.org/10.48550/ARXIV.2412.14470)Cited by:[§1](https://arxiv.org/html/2608.14590#S1.p2.1),[Table 1](https://arxiv.org/html/2608.14590#S4.T1.1.28.1),[item 2](https://arxiv.org/html/2608.14590#S5.I1.i2.p1.1),[Table 5](https://arxiv.org/html/2608.14590#S6.T5.2.2.3.1.1),[§7\.10](https://arxiv.org/html/2608.14590#S7.SS10.p1.1),[§8\.1](https://arxiv.org/html/2608.14590#S8.SS1.p2.1)\.