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

Pierre Dantas; Lucas Cordeiro; Ehsan Nowroozi; Norbert Tihanyi

cs.AIJun 22, 2026

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

Authors: Pierre Dantas, Lucas Cordeiro, Ehsan Nowroozi, Norbert Tihanyi

Organizations: The University of Manchester, Manchester, UK · The University of Greenwich, London, UK · Technology Innovation Institute, Abu Dhabi, UAE

Abstract

Large Language Model (LLM) agents take irreversible real-world actions, yet no system gives formally grounded, task-level safety guarantees for their plans. In a PRISMA 2020 systematic review, we searched six databases (20-29 May 2026) for work on LLM agent specification, verification, and enforcement published in 2022-2026. We narratively synthesized 38 studies, assessed risk of bias per study, and graded evidence certainty with GRADE. Three authors independently screened a repeated search to validate the single-reviewer screening (agreement: Fleiss' $κ= 0.81$ ). First, specification is the bottleneck: on one benchmark, only 24.8-34.2% of LLM translations from natural language into Planning Domain Definition Language (PDDL) are semantically correct. Second, runtime monitoring is the most mature enforcement strategy; it reduced unsafe actions by 65.37% in one household-agent study, but its guarantees cover only single steps or short horizons. Third, in one $τ$ -Bench study of transactional tool-use agents, blocking 94% of unsafe actions still left fewer than 5% of tasks completed both safely and correctly in most settings, because agents found other unsafe routes (the verifier tax). Fourth, no approach simultaneously achieves soundness, completeness, scalability, semantic grounding, and utility preservation. For seven of the nine principal claims, GRADE gives the lowest certainty rating (Very Low), meaning further studies are likely to produce substantially different figures; each rests on one or two studies in narrow domains. Two of the open problems we rank highest are translating requirements into formal specifications that keep their meaning and enforcing safety over whole plans rather than single actions. We contribute a three-level taxonomy and an agenda of ten open problems.

Figures & tables

Figure 1: The specification-verification-enforcement pipeline for LLM agent plans. Given a task

t

and history

h

, an agent

\mathcal{A}

generates a plan

\pi

. The specification stage (1) acquires a formal safety property

\varphi

from human requirements; the verification stage (2) checks whether

\pi\models\varphi

before, during, or after execution; the enforcement stage (3) intervenes when

\pi\not\models\varphi

. The dashed box in each stage names the research gaps (Section 5.7 ) that arise there. Only tasks completed with

\pi\models\varphi

count toward SSR .

Database	Access method	Date searched
arXiv (cs.AI, cs.LG, cs.SE, cs.LO)	API + WebFetch	20–29 May 2026
ACM Digital Library	site:dl.acm.org web search	20–29 May 2026
IEEE Xplore	site:ieeexplore.ieee.org web search	20–29 May 2026
Semantic Scholar	site:semanticscholar.org web search	20–29 May 2026
Google Scholar	Web search	20–29 May 2026
Preprints.org	site:preprints.org web search	20–29 May 2026

Table 1: Databases searched.

#	Search string
S1	formal verification LLM agent plans model checking 2023 2024 2025
S2	runtime verification large language model agents safety 2023 2024
S3	temporal logic LLM agents specification verification arXiv 2024 2025
S4	LLM agent safety specification formal methods survey 2024 2025 arXiv
S5	model checking AI planning PDDL formal specification agent behavior 2023 2024
S6	natural language to formal specification LTL TLA+ translation LLM 2023 2024 2025

Table 2: Primary search strings. Year terms (e.g. “2024 2025”) were searched as literal keywords against each database’s default field(s) rather than applied via a dedicated publication-date filter. A keyword match on a year is a weaker proxy for publication date than a native date-range filter.

Panel of Figure 2 — Figure 2: PRISMA 2020 flow diagram for study selection.

System / Paper	Year	Venue	Stage	Sub-cat	Moment	Grounding
Foundational and Survey Works (FS) – outside the three-stage taxonomy ∗
Toolformer [ 23 ]	2023	PR (NeurIPS)	FS	Arch.	N/A	–
Chain-of-Thought [ 24 ]	2022	PR (NeurIPS)	FS	Arch.	N/A	–
Planning Survey [ 42 ]	2024	PP	FS	Survey	N/A	–
LLM+FM Roadmap [ 43 ]	2024	PP	FS	Survey	N/A	–
ReAct [ 25 ]	2023	PR (ICLR)	FS	Arch.	N/A	–

Table 3: Classification of all 38 included studies under the proposed taxonomy, grouped by pipeline stage.

Survey	Type	Scope	Method	FM depth	Pipeline	Evidence
Zhang et al. [ 43 ]	NS	FM– LLM integration	Narrative	Mod.	S, V	None
Full-Stack Safety [ 44 ]	NS	Full LLM safety	Narrative	Low	Partial	None
Huang et al. [ 42 ]	NS	LLM planning	Narrative	None	S only	None
This survey	SLR	Spec-Verif-Enf	PRISMA 2020	Deep	S,V,E	GRADE

Table 4: Comparison with related surveys. Type: SLR = Systematic Literature Review; NS = Narrative Survey. Pipeline: S = Specification, V = Verification, E = Enforcement.

System	Overhead unit	Reported value	Domain
AgentSpec [ 19 ]	Per-rule evaluation	Milliseconds	Code, embodied, driving
Agent-C [ 3 ]	Constrained decoding	Not quantified	Retail, airline
ProbGuard [ 4 ]	Not reported	Not quantified	Autonomous driving
LogicGuard [ 40 ]	Critic evaluation	Not quantified	Minecraft
VerifyLLM [ 39 ]	Per-window check	Not quantified	Household robotics
LlamaFirewall [ 41 ]	Per-request	Production latency	Meta production

Table 5: Reported runtime overhead for enforcement systems.

System	Temporal seq.	Memory/PII	Tool safety	Credentials	Multi-agent	Adversarial
AgentSpec [ 19 ]	✓	$\circ$	✓	—	—	—
Agent-C [ 3 ]	✓	—	✓	$\circ$	—	—
AgentVerify [ 21 ]	✓	✓	✓	—	—	—
AgentProof [ 34 ]	✓	$\circ$	✓	—	$\circ$	—
LlamaFirewall [ 41 ]	—	—	$\circ$	—	—	✓
ProbGuard [ 4 ]	✓	—	—	—	—	—

Table 6: Safety domains addressed by included verification/enforcement systems. ✓: explicitly evaluated.

\circ

: partially addressed. —: not addressed.

Domain	Concrete trigger for this literature
Study limitations (L)	No released code, specification, or evaluation harness; a single model family evaluated; no variance or confidence interval reported across runs.
Inconsistency (I)	Conflicting results for the same claim across two or more independent studies or benchmarks.
Indirectness (D)	Evaluation restricted to a simulated or narrow task domain that differs materially from realistic deployment conditions.
Imprecision (P)	A single supporting study, fewer than a field-appropriate minimum number of tasks, or no confidence interval reported.
Publication bias	Standing limitation across all ratings (Section 6.6 ); not scored per claim in this review.

Table 7: GRADE downgrade domains operationalized for LLM-agent safety evidence.

Claim	Supporting evidence	L	I	D	P	GRADE
No LLM agent achieves $>$ $60\text{\,}\mathrm{\%}$ safety on comprehensive benchmarks	Agent-SafetyBench (16 agents, 2k cases) [ 5 ]				✓	Moderate
LLM -to- LTL translation achieves $>$ $90\text{\,}\mathrm{\%}$ syntactic correctness	4+ independent studies [ 18 , 26 , 27 , 8 ]		✓			Moderate
LLM -to- PDDL semantic correctness is $24.8\text{\,}\mathrm{\%}34.2\text{\,}\mathrm{\%}$	Planetarium (1 benchmark) [ 48 ] , via survey [ 7 ]	✓		✓	✓	Very Low
LTL runtime enforcement achieves $100\text{\,}\mathrm{\%}$ conformance in closed domains	Agent-C, AgentSpec (2 studies) [ 3 , 19 ]	✓		✓	✓	Very Low
Static graph verification detects structural defects in $<$ 1 s	AgentProof (1 study, 18 workflows) [ 34 ]	✓		✓	✓	Very Low
Probabilistic monitoring warns up to 15.84 s before violation without false alarms	ProbGuard (1 study, 2 domains) [ 4 ]	✓		✓	✓	Very Low

Table 8: GRADE certainty of evidence for principal claims. Downgrade reasons: L = study limitations, I = inconsistency, D = indirectness, P = imprecision (single study).

Gap	Arch	Spec	Verif	Enf	Bench
RG1 – Semantic translation		$\bullet$	$\circ$
RG2 – Long-horizon scale	$\bullet$		$\bullet$		$\circ$
RG3 – Verifier tax			$\circ$	$\bullet$	$\bullet$
RG4 – Dynamic plan generation	$\bullet$		$\bullet$
RG5 – Multi-agent	$\bullet$	$\circ$	$\bullet$
RG6 – Stochastic model check.		$\circ$	$\bullet$

Table 9: Gap coverage heatmap.

\bullet

: this cluster gives rise to or studies the gap.

\circ

: the cluster partially addresses the gap.

Gap	Binding difficulty	Research directions
RG1 – Semantic translation	Novel domains have no independent ground truth against which to check a translated specification	RG1.1 grammar- and type-constrained decoding; RG1.2 Counter-example Guided Inductive Synthesis (CEGIS) -style equivalence checking of candidate translations; RG1.3 benchmarks pairing requirements with verified specifications and traces
RG2 – Long-horizon scale	Kripke state space grows exponentially with plan length; verified systems handle $5\text{\,}30\text{\,}$ actions	RG2.1 partial verification of safety-critical sub-sequences; RG2.2 abstraction refinement focused on high-risk transitions; RG2.3 assume-guarantee contracts between plan segments
RG3 – Verifier tax	Agents route around action-level blocks, for example by fabricating identifiers	RG3.1 plan-level, goal-contextual policies; RG3.2 identifier-integrity monitor against a ground-truth index; RG3.3 safe replanning upon violation
RG4 – Dynamic plans	Static methods need a finite, pre-specified workflow graph	RG4.1 online, incremental workflow-graph extraction; RG4.2 pre-verified plan templates whose instantiations inherit the proof
RG5 – Multi-agent	Composing agents raises the complexity class (Section 7.1 )	RG5.1 assume-guarantee contracts between agents; RG5.2 protocol verification with session types or communicating automata
RG6 – Probabilistic specification	Stochastic agents meet deterministic specifications; one corpus study (ProbGuard) addresses this	RG6.1 PCTL properties checked on DTMCs learned from traces; RG6.2 calibrated monitors via conformal prediction

Table 10: Research directions for the ten open problems of Section 5.7 . Appendix C develops each gap and each direction with pointers to prior work.

Mechanism	Cost in $n$	Cost in $k$ (agents)	Reported limit
Runtime automaton monitor (AgentSpec)	$O(1)$ per action	Not evaluated for $k>1$	Millisecond/rule [ 19 ]
LTL product check (single agent)	$\|M\|\cdot 2^{O(\|\varphi\|)}$	N/A	$5\text{\,}30\text{\,}$ actions [ 8 ]
CTL / CTL ∗ , $k$ agents composed	Polynomial in $\|M\|$	pspace -complete (program compl.) [ 53 ]	Not evaluated in corpus
atl , perfect information	Polynomial in $\|M\|$ , $\|\varphi\|$	Polynomial [ 54 ]	Not evaluated in corpus
atl , imperfect information	Undecidable [ 55 ]	Undecidable	Not applicable
DFA product (AgentProof)	$O(\|G\|\cdot\|D\|)$	Single-agent workflows only	5,000 nodes, sub-second [ 34 ]

Table 11: Verification cost as a function of plan length

n

and agent count

k

, by mechanism. Notation follows each source;

|M|

= model size,

|\varphi|

= formula length,

|G|

|D|

= workflow graph and DFA sizes.

LLM Agent Safety

Large language model agent safety studies how to keep tool-using, persistent, and multi-agent systems aligned with user intent and authorized limits.

See all 322 papers

Position: A Three-Layer Probabilistic Assume-Guarantee Architecture Is Structurally Required for Safe LLM Agent Deployment
May 18, 2026S. Bensalem, Y. Dong, M. Franzle +6AI Agent Reliability LLM Guardrails
1CSX-AI, France · University of Liverpool, UK · 3Carl von Ossietzky Universität Oldenburg, Germany +2
Tool Specifications Matter: Uncovering and Mitigating Safety Risks in AI Agents
Jul 31, 2026Minghui Pan, Jiayuxuan Yang, Yuanyuan Yuan +2LLM Guardrails Prompt Injection Attacks on AI Agents
Beijing University of Posts and Telecommunications · Beihang University · Tsinghua University
AgentBoundary: Counterfactual Evaluation of Safety in Tool-Using LLM Agents
Sep 27, 2026Tianzhuo Yang, Zirui Mi, Yantao Huang +4LLM Agent Evaluation LLM Agents
Peking University · Beijing Academy of Artificial Intelligence

May 18, 2026J/K move · Enter open · S save

Position: A Three-Layer Probabilistic Assume-Guarantee Architecture Is Structurally Required for Safe LLM Agent Deployment

S. Bensalem, Y. Dong, M. Franzle, X. Huang+5

1CSX-AI, France · University of Liverpool, UK · 3Carl von Ossietzky Universität Oldenburg, Germany+2

AI Agent Reliability LLM Guardrails Runtime Enforcement for AI Agents LLM Agent Safety

Open paper AskPDF arXiv

This position paper argues that enforcing LLM agent safety within a single abstraction layer is not merely suboptimal but categorically insufficient for deployed LLM agents -- a structural consequence of how agent execution works, not a contingent limitation of current systems. The three dimensions that jointly constitute safe operation -- semantic intent and policy compliance, environmental validity, and dynamical feasibility -- each depend on a strictly distinct set of information that becomes available at different stages of execution. No single guardrail can certify all three. We argue that the community must respond with a contract-based architecture in which each safety dimension is enforced by an independently certified layer whose probabilistic guarantee satisfies the next layer's assumption. We sketch such an architecture and derive the compositional system-level safety bounds it admits via the chain rule of probability. Three open problems stand between this and a deployable standard: bound estimation from non-i.i.d.\ traces, graceful degradation of contracts under deployment drift, and extension to multi-agent settings -- the most important unfinished business in LLM agent runtime assurance.

Abstract

LLM Agent Safety

Explore similar work

Position: A Three-Layer Probabilistic Assume-Guarantee Architecture Is Structurally Required for Safe LLM Agent Deployment

Tool Specifications Matter: Uncovering and Mitigating Safety Risks in AI Agents

AgentBoundary: Counterfactual Evaluation of Safety in Tool-Using LLM Agents