PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Pierre Dantas, Lucas Cordeiro, Ehsan Nowroozi, Tihanyi Norbert

arXiv:2608.14590v1cs.AI

TL;DR

LLM-agent safety research lacks formally grounded, task-level guarantees for plans with irreversible effects. This PRISMA 2020 review synthesizes 38 studies and finds that no current approach simultaneously achieves soundness, scalability, semantic correctness, and task-level safety preservation.

  • Problem

    LLM agents can execute plans with irreversible real-world effects, yet existing verification approaches lack complete, scalable guarantees for dynamically generated open-ended plans.

  • Method

    The paper conducts a PRISMA 2020 systematic review synthesizing 38 studies from six academic databases across specification, verification, enforcement, and safety evaluation.

  • Results

    No included study simultaneously satisfies soundness, completeness, scalability, semantic grounding, and task-utility preservation; semantic correctness in PDDL translation is only 24% to 35%.

  • Takeaways & Limitations

    Semantically incorrect specifications can produce false assurance, while action-level enforcement may leave task-level safety below 5%, supporting SSR as a primary evaluation metric.

  • Takeaways & Limitations

    The review has predominantly Low to Very Low certainty because of field novelty, heterogeneous evidence, and limited independent replication.

Abstract

from arXiv · show

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 only 24% to 35% semantic correctness, undermining downstream verification. Second, runtime monitoring is the most mature enforcement strategy, reducing unsafe actions by 40% to 65% in controlled settings, but it does not provide complete safety guarantees. Third, the verifier tax shows that blocking 94% of unsafe actions can still result in less than 5% 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 agentic AI.

1 Introduction

LLM agents increasingly execute consequential, potentially irreversible plans, yet their fluent outputs can violate formal safety requirements because they are generated through statistical pattern matching rather than sound logical inference. This survey frames safety as a specification–verification–enforcement pipeline and systematically synthesizes 38 studies from 2022–2026.

  • Motivation: LLM agents now operate in consequential domains, where multi-step plans can commit irreversible real-world actions.Examples include software engineering, healthcare, customer service, and autonomous driving.
  • Safety gap: LLM-generated plans may violate safety invariants, disregard temporal ordering constraints, or cause cascading harmful effects despite appearing coherent.Classical planning and formal verification tools provide rigorous guarantees, but applying them to agent outputs requires bridging natural language and formal mathematical structures.
  • Safety gap: 16 popular LLM agents scored above 60 % on a structured safety benchmark spanning 2,000 test cases.Frontier models also show limited robustness to basic jailbreak attacks in multi-step agentic settings.
  • Survey contributions: 38 studies from 2022 to 2026 were identified across six databases using a PRISMA 2020 systematic review protocol.The survey contributes a three-level taxonomy, a multidimensional comparison, an empirical synthesis of the verifier tax, and ten open problems.
  • Pipeline framing: The formal validation problem comprises specification, verification, and enforcement: acquiring φ, determining whether π |= φ, and responding when π̸ |= φ.Each sub-problem is independently difficult, and their composition introduces additional challenges.

2 Background and Preliminaries

The survey’s verification foundations combine temporal logics, model checking, classical planning formalisms, and LLM-agent representations. These foundations define how agent plans, safety properties, stochastic behavior, and translation assumptions are represented and checked.

  • Temporal logic: Temporal logic is the dominant specification language, spanning linear traces, branching futures, continuous-time robustness, and probabilistic safety guarantees.LTL evaluates infinite traces; CTL quantifies over paths, STL measures quantitative robustness for real-valued signals, and PCTL expresses probabilistic properties such as P≥p[φ].
  • Model checking: Model checking decides whether a formal model M satisfies a specification φ, typically using Kripke structures and automata-based or probabilistic algorithms.Automata-based LTL checking searches for accepting cycles in M ⊗ A¬φ, while probabilistic model checking handles Markov chains and MDPs to quantify unsafe-state reachability.
  • Classical planning: PDDL provides the main structured planning formalism, representing domains, problems, action effects, initial states, and goals so external planners can validate generated plans.STRIPS and HTN planning also map to LLM-agent plan structures, with HTN verification studied for multi-agent task allocation.
  • LLM-agent characterization: Agent verification depends on plan representation, execution horizon, and agency mode, ranging from trace, graph, or code plans to short or long horizons and single- or multi-agent systems.Short-horizon plans contain 5 to 30 actions and are tractable for current verifiers, whereas long-horizon plans contain 50 to 500+ actions and exceed existing approaches; multi-agent interactions also increase complexity.
  • Formal definitions and assumptions: The NL-to-formal translation problem is a core assumption risk: translators can achieve high syntactic validity while semantic correctness remains low.The translation is represented as τ : N → F, with semantic failure expressed as τ(x)̸ ≡x and identified as a root cause of false assurance.

3 Methodology

The review used a prereview-fixed PRISMA 2020 protocol to systematically assess LLM-agent safety research published from 2022 to 2026. Its quantitative findings and synthesis are based on 38 included studies identified through searches of six academic databases.

  • Review protocol: The review followed PRISMA 2020 guidelines and fixed its eligibility criteria, search strings, and synthesis approach before database searching.It was conducted independently as a rapid systematic review from 20 to 29 May 2026 and was not preregistered.
  • Eligibility criteria: Eligibility covered English-language studies from 2022 to 2026 involving LLM agents that produce multi-step plans, action sequences, or tool-call chains.Included topics were plan specification, verification, enforcement, and safety monitoring; pure chatbot safety without planning was excluded.
  • Search strategy: Six databases were searched using eight primary strings targeting formal verification, runtime verification, temporal logic, model checking, NL-to-formal translation, enforcement systems, and roadmaps.Supplementary searches covered 22 named systems, including VerifyLLM, AgentVerify, ProbGuard, LogicGuard, AgentProof, and NL2LTL.
  • Evidence corpus: The 38 included studies formed the formal PRISMA corpus underlying all quantitative claims, the taxonomy, and the GRADE assessments.The larger reference list contained 64 entries, including sources outside the PRISMA inclusion criteria, so quantitative observations apply to the 38 included studies.

4 Taxonomy and Classification System

The paper proposes an orthogonal three-level taxonomy classifying 38 studies by pipeline stage, verification moment, and formal grounding. It organizes specification, verification, and enforcement techniques while exposing trade-offs among plan availability, executability, and safety assurance.

  • Taxonomy dimensions: The taxonomy classifies all 38 studies across three largely independent dimensions: pipeline stage, verification moment, and formal grounding.The dimensions capture when verification occurs, what representation is used, and how verification is performed.
  • Specification techniques: Specification techniques comprise SPEC-NL translation, SPEC-PL planning-language descriptions, and SPEC-AL alignment-based soft constraints.Examples include NL2LTL, PDDL or HTN descriptions, and Constitutional AI or reinforcement-learning objectives.
  • Verification techniques: Verification techniques comprise model checking, static analysis, theorem proving, and LLM-assisted verification.These range from Kripke-structure or FSM checks and workflow-graph analysis to deductive contracts and LLM critics.
  • Verification moments: Pre-execution verification can reject or revise complete plans, runtime verification checks generated actions, and post-hoc verification supports auditing but cannot prevent execution-time harm.Post-hoc verification analyzes the complete execution trace after task completion, whereas runtime verification cannot assess actions not yet generated.
  • Relationship to prior frameworks: The taxonomy complements prior frameworks by classifying pipeline stage, verification moment, and formal grounding rather than integration direction, planning strategy, or deployment phase.Used with prior taxonomies, it provides a more thorough characterization of individual approaches.

5 Related Work

Related work spans formal specification, static and runtime verification, LLM-assisted critique, enforcement, and safety benchmarking, but no approach provides end-to-end task-level guarantees. The literature shows persistent semantic, representational, scalability, and action-to-task safety gaps.

  • No prior survey systematically covers the complete specification-verification-enforcement pipeline, applies GRADE certainty grading, and synthesizes the verifier tax as a field-level empirical finding.
  • Representation: Trace-based representations dominate runtime verification, while graph-based representations suit static analysis, but neither supports complete pre-execution verification with arbitrary open-ended planning.The field lacks a canonical intermediate representation preserving both an LLM-generated plan’s semantics and the architectural properties needed for formal verification.
  • Specification: 24.8 % to 35.1 % semantic correctness remains for leading LLMs translating language into PDDL, despite above 96 % syntactic correctness.This semantic gap undermines verification because formally checking models with incorrect preconditions and effects cannot establish the intended plan’s safety.
  • Verification: Runtime monitoring is the most mature cluster, whereas static verification offers pre-deployment soundness only for finite workflows and model checking faces state-space explosion at realistic scales.LLM-assisted verification improves accessibility but lacks formal soundness guarantees; runtime methods generally provide only one-step or short-horizon guarantees.
  • Benchmarks: None of 16 LLM agents scored above 60 % safety on Agent-SafetyBench, which covers 349 environments, 2,000 test cases, 8 risk categories, and 10 failure modes.AgentHarm likewise evaluates 110 malicious tasks across 11 harm categories and finds limited frontier-model robustness to basic multi-step jailbreaks.

6 Cross-Cutting Synthesis

The synthesis identifies semantic specification correctness as the binding constraint on sound end-to-end verification, while static and runtime enforcement each trade completeness against scalability. It also shows that action-level blocking can fail to preserve task-level safety, motivating plan-level policies, integrity constraints, safe replanning, and probabilistic warning-based monitoring.

  • Specification correctness: 24.8% to 35.1% semantic correctness in PDDL generation contrasts with above 96% syntactic validity, making specification acquisition the binding constraint on verification soundness.Interactive disambiguation and hierarchical decomposition reduce semantic errors but do not eliminate them; verified specification acquisition remains open.
  • Verification and enforcement trade-offs: Static verification provides pre-deployment soundness for finite prespecified workflow graphs, whereas runtime monitoring handles dynamic plans at millisecond-per-action overhead but cannot assess future actions.AgentProof verifies graphs up to 5000 nodes in sub-second time; runtime methods remain incomplete for as-yet-ungenerated actions.
  • Verification and enforcement trade-offs: No included study is both complete over full plan traces and scalable to dynamically generated open-ended plans.VeriGuard combines offline policy verification with runtime filtering, but its policy must remain finite and prespecified; scalable partial verification has not been demonstrated.
  • Verifier tax: 94% of non-compliant individual actions intercepted on τ-Bench still yielded below 5% SSR, revealing a verifier tax between action-level blocking and safe task completion.Agents may enter failure loops by fabricating alternative identifiers after legitimate paths are blocked, so blocking unsafe actions does not ensure task completion.
  • Verifier tax: Plan-level safety policies, integrity constraints, and safe replanning are proposed to address the verifier tax, but no included system meets all three requirements.The verifier tax has low GRADE certainty because it comes from a single study, although related bypass patterns appear in AgentGuard and LlamaFirewall.
  • Probabilistic monitoring: 65.37% reduction in unsafe behavior with 80.4% task completion rate illustrates ProbGuard’s safety-utility trade-off, while its 38.66-second warnings support intervention before irreversible harm.ProbGuard provides probabilistic rather than deterministic guarantees, requires domain-specific execution traces, and has very low generalisability evidence.

7 Research Agenda · 7.1 RG1 – Semantic Correctness in NL-to-Formal Translation · 7.2 RG2 – Scalability to Long-Horizon Plans

The research agenda identifies ten open problems, emphasizing semantic correctness in NL-to-formal translation and scalability to long-horizon plans. It prioritizes stronger semantic validation, benchmark creation, and verification strategies that focus effort on critical or composable plan segments.

  • 7 Research Agenda: The agenda organizes ten open problems, each covering the state of the art, technical difficulty, and concrete research directions.The problems are identified through systematic gap analysis in Sections 5.7 and 6.
  • 7.1 RG1 – Semantic Correctness in NL-to-Formal Translation: 24% to 35% semantic correctness for PDDL contrasts with above 90% syntactic correctness for LTL and above 96% for PDDL.Interactive disambiguation and hierarchical decomposition reduce semantic errors but do not eliminate them.
  • 7.1 RG1 – Semantic Correctness in NL-to-Formal Translation: Semantic validation is circular in novel domains because verifying a specification requires a formal oracle that correctly formalizes the domain.Such domains lack independent ground truth apart from the specification being evaluated.
  • 7.1 RG1 – Semantic Correctness in NL-to-Formal Translation: Grammar-constrained decoding can ensure syntactic validity, while semantic type constraints could eliminate some generation-time errors in LTL and PDDL.Integrating semantic type systems into decoding remains an open engineering challenge.
  • 7.1 RG1 – Semantic Correctness in NL-to-Formal Translation: Counterexample-guided equivalence checking could compare candidate translations and feed discrepancies back to the LLM for refinement.A model checker searches for a Kripke structure satisfying one candidate but not the other, adapting CEGIS to specification translation.
  • 7.1 RG1 – Semantic Correctness in NL-to-Formal Translation: Semantic-ground-truth benchmarks should pair NL requirements with formally verified LTL/PDDL specifications and execution traces, but such datasets do not yet exist at scale.Crowdsourcing requirements from deployment logs and having domain experts verify them is proposed as a near-term path.
  • 7.2 RG2 – Scalability to Long-Horizon Plans: 5 to 30 actions is the range handled by current verified systems, while SWE-bench tasks exceed 100 actions and autonomous research assistants exceed 500 actions.AgentProof scales to graphs of 5,000 nodes only for finite workflow graphs, not open-ended dynamic plans; exhaustive model checking is beyond long-horizon tasks.
  • 7.2 RG2 – Scalability to Long-Horizon Plans: Partial verification can target safety-critical sub-sequences, abstracting away low-risk actions with CEGAR and composing segments through assume-guarantee contracts.These approaches aim to reduce verification cost, but composition across dynamically generated segments remains open.

7.3 RG3 – The Verifier Tax

The verifier tax arises because blocking individually unsafe actions does not preserve task-level safety: intercepting 94% can still leave safe task completion below 5%. Proposed remedies shift enforcement toward goal-contextual plan monitoring, credential-integrity checks, and constrained replanning.

  • RG3 – The Verifier Tax: 94% of individually unsafe actions can be intercepted while safe task completion remains below 5%, driven by agents hallucinating credentials to bypass blocked paths.No existing system resolves this gap; the verifier tax reflects goal optimization when direct paths are blocked.
  • RG3.1 – Plan-level safety policies: Plan-level monitors should evaluate proposed subsequences or full plan fragments against safety properties that reference the agent’s goal context.This requires access to the task description, current intent, and action sequence; extending Agent-C’s temporal DSL toward goal-contextual properties remains open.
  • RG3.2 – Credential and identity integrity constraints: Agents can fabricate plausible identifiers absent from the ground-truth user database, motivating monitors that reject actions referencing identifiers outside a trusted index.The proposed mechanism parallels parameterized-query defenses that reject inputs deviating from a trusted schema.
  • RG3.3 – Safe replanning upon violation: Violation handling should trigger constrained replanning that generates a safe, goal-progressing alternative sequence rather than merely blocking the action.This integrates enforcement monitoring with a constrained planner such as a PDDL solver or hard-constrained LLM; VeriPlan demonstrates model-checker-guided user-facing replanning.

7.4 RG4 – Dynamic Plan Generation · 7.5 RG5 – Multi-Agent Verification · 7.6 RG6 – Probabilistic Specification and Stochastic Model Checking

The paper identifies missing verification foundations for dynamically generated plans, arbitrary multi-agent topologies, and stochastic agent behavior. It proposes online, compositional, protocol-level, and probabilistic methods to extend safety verification beyond current deterministic single-agent workflows.

  • 7.4 RG4 – Dynamic Plan Generation: Static verification assumes pre-specified finite workflow graphs, but no included study provides pre-execution soundness guarantees for dynamically assembled plans.Real deployments repeatedly observe state, generate actions, execute them, and incorporate outcomes.
  • 7.4 RG4 – Dynamic Plan Generation: Online extraction of workflow graphs with incremental static checks could verify dynamically growing plans without requiring the full graph beforehand.The sequence of calls to sub-agents and tools implicitly defines the graph as execution proceeds.
  • 7.4 RG4 – Dynamic Plan Generation: Pre-verifying parameterized plan templates and checking each generated instantiation’s conformity could provide soundness guarantees for plan families.The approach parallels type-checked generics: verified templates transfer proofs to conforming instantiations.
  • 7.5 RG5 – Multi-Agent Verification: Most verification work targets single-agent plans, and no study provides a general compositional framework for arbitrary multi-agent system topologies.Existing work includes LTL verification for multi-robot task allocation, MCP/skill protocols, and tacit treatment of collusion.
  • 7.5 RG5 – Multi-Agent Verification: Assume-guarantee contracts could compose component-level agent proofs into system-level properties without exhaustive joint state-space exploration.Adapting contracts to LLM agents with non-deterministic outputs remains an open challenge.
  • 7.5 RG5 – Multi-Agent Verification: Formal session types or communicating automata could verify inter-agent protocols for safety properties such as no deadlock or privilege escalation.AgentVerify’s MCP/skill invocation protocols provide a starting point for this tractable sub-problem.
  • 7.6 RG6 – Probabilistic Specification and Stochastic Model Checking: Probabilistic safety specifications are appropriate because identical stochastic generation calls can produce different action sequences; ProbGuard is the only included study addressing probabilistic safety.ProbGuard uses DTMC models with PAC-learning bounds, while PRISM-style PCTL model checking has not yet been applied.
  • 7.6 RG6 – Probabilistic Specification and Stochastic Model Checking: PCTL specifications checked with PRISM against learned DTMC or MDP models could extend ProbGuard to empirical LLM-agent execution traces.Calibrated monitors could also output violation probabilities and support risk-threshold policies, but conformal prediction has not yet been applied to agent safety monitoring.

7.7 RG7 – Verified Re-Planning

Existing enforcement systems block, log, or abort when plans violate safety properties, but none automatically generates a safe alternative that continues toward the goal. Verified re-planning therefore centers on constraint-satisfying repair or constrained generation, both requiring capabilities not yet fully developed for LLM agents.

  • RG7 – Verified Re-Planning: No enforcement system generates an alternative plan segment satisfying all safety constraints while continuing toward the goal.VeriPlan produces user-facing constraint-satisfying plans but does not address automated replanning for agentic systems.
  • RG7.1 – Constraint-satisfying plan repair: Plan repair minimally modifies a failing plan to restore validity and could generate a constraint-satisfying alternative fragment from the violation point.Integration with LTL or PDDL checkers is proposed, but LLM plans require bidirectional translation between natural-language and formal representations.
  • RG7.2 – Constrained LLM plan generation: Constrained generation steers LLMs toward safe plan completions using constrained beam search or SMT-guided decoding.Agent-C demonstrates feasibility for temporal sequence constraints, while extension to arbitrary LTL properties over plan prefixes remains open.

7.8 RG8 – Specification Acquisition at Scale · 7.9 RG9 – Adversarial Robustness of Verification Systems

Scaling formal safety specifications requires automated acquisition from demonstrations, regulatory documents, and reusable libraries, while verification and enforcement systems remain exposed to adversarial attacks. The agenda therefore emphasizes both scalable specification generation and end-to-end robustness guarantees.

  • 7.8 RG8 – Specification Acquisition at Scale: Formal-methods expertise creates a scalability bottleneck because agent-deployment domains vastly outnumber available experts.Existing automated acquisition approaches remain nascent and have been evaluated only in narrow domains.
  • 7.8 RG8 – Specification Acquisition at Scale: Specification mining can infer LTL formulas that distinguish safe from unsafe agent execution traces.Applying mining algorithms to production LLM-agent logs could enable data-driven acquisition without human expert authoring.
  • 7.8 RG8 – Specification Acquisition at Scale: Regulatory-document extraction could produce reusable formal safety specifications by translating existing domain rules under expert validation.No study has yet applied this principle at scale to structured regulatory documents.
  • 7.8 RG8 – Specification Acquisition at Scale: Compositional libraries of peer-reviewed LTL and DSL specifications could reduce per-deployment burdens for recurring safety properties.AgentVerify’s four-domain library provides a seed, but systematic community curation remains necessary.
  • 7.9 RG9 – Adversarial Robustness of Verification Systems: Enforcement systems have demonstrated attack surfaces, including prompt-injection monitor bypasses and 1.75 % attack success in production-grade guardrails.LLM-based translation components can also generate incorrect specifications or Kripke structures under adversarial inputs.
  • 7.9 RG9 – Adversarial Robustness of Verification Systems: Systematic red-teaming should evaluate the end-to-end verification pipeline from natural-language elicitation through specification translation, model checking, and enforcement.Targets include specification-generator prompt injection, adversarial Kripke structures, and monitor bypass through indirect action sequences.
  • 7.9 RG9 – Adversarial Robustness of Verification Systems: End-to-end adversarial evaluation would characterize the residual risk of each verification and enforcement component.The proposed approach adapts LLM red-teaming methodologies specifically to verification pipelines.
  • 7.9 RG9 – Adversarial Robustness of Verification Systems: Formally verified specification translators could provide robustness to adversarial inputs by construction through type-safe grammars or certified compilation.Applying verified compilation to LTL-generating components, at least for restricted input fragments, would reduce reliance on empirical red-teaming.

7.10 RG10 – Evaluation Standardisation

Evaluation standardisation requires a unified benchmark spanning formal verification coverage, runtime overhead, and safe task success across architectures and domains. The section recommends SSR as the primary enforcement metric and contamination-resistant evaluation practices.

  • Evaluation gap: No benchmark jointly evaluates formal verification coverage, runtime overhead, and SSR across multiple agent architectures and task domains.Existing benchmarks cover only subsets: Agent-SafetyBench addresses safety, τ-Bench measures SSR narrowly, and AgentBench measures task success without safety.
  • Unified benchmark: A unified safety suite should provide environments with ground-truth safe and unsafe plans, formal specifications, SSR, verification coverage, and runtime-overhead metrics.The suite should be developed jointly by formal methods, NLP, and AI safety communities.
  • Metric adoption: SSR should be the primary enforcement metric, supplemented by action-level conformance, because it captures tasks completed safely and correctly.A community-maintained leaderboard or shared evaluation server could accelerate adoption.
  • Contamination mitigation: LLM memorization of public benchmark scenarios may inflate performance, requiring held-out, procedurally generated, and canary-detected evaluation tasks.Held-out sets should be updated after major model releases and use verifiable ground truth.

8 Discussion

The field is early but structurally sound, with emerging standards and deployments alongside low-certainty evidence, weak replication, and unresolved specification challenges. Current recommendations favor layered runtime safeguards and specification quality, while societal risks and review-validity threats limit confidence in formal safety claims.

  • Field maturity: The field is transitioning from 2023–2024 demonstration-driven hype toward 2025–2026 empirical scrutiny, exemplified by findings challenging simplistic assumptions such as the verifier tax.This trajectory is described using the Gartner Hype Cycle as a rough heuristic.
  • Field maturity: Early maturity is signaled by convergence on LTL, dedicated workshops, production deployment of LlamaFirewall, and standardized benchmarks including Agent-SafetyBench and τ-Bench.These indicators support cross-study comparison and demonstrate movement beyond isolated demonstrations.
  • Field maturity: Most principal claims have Low or Very Low GRADE certainty, while studies commonly lack independent replication and no system simultaneously satisfies all major safety objectives.The field also lacks a shared formal framework, and specification acquisition and verified re-planning remain among the least studied problems.
  • Practical deployment recommendations: For dynamic agents, runtime monitoring is preferred over static verification because static pre-execution checking is structurally inapplicable; AgentSpec and Agent-C provide the strongest demonstrated practical options.Sub-millisecond per-action overhead is confirmed only for AgentSpec; other runtime systems have not quantified overhead.
  • Practical deployment recommendations: In high-stakes domains, probabilistic monitoring provides PAC-style early warnings, including 38.66 seconds of intervention time demonstrated in autonomous driving.The recommendation targets severe and irreversible safety violations in autonomous driving, medical decision support, and financial transactions.
  • Societal and ethical considerations: Deployment in healthcare, legal, and financial settings is outpacing formal verification’s maturation, while specification choices shape permitted behavior and certificates may create unwarranted safety expectations.These concerns include low or very low evidence certainty, conflicts between corporate and user interests, and specifications that omit relevant safety properties.

9 Conclusion

This PRISMA 2020 survey synthesizes 38 studies on specification, verification, enforcement, and safety evaluation for LLM agent plans. It finds persistent specification, verifier-tax, and scalability gaps despite progress in runtime monitoring and formal verification, and defines a focused research agenda.

  • Review scope: 38 studies published between 2022 and 2026 were synthesized using a PRISMA 2020 protocol across six databases.The review covered specification techniques, verification approaches, enforcement mechanisms, and safety evaluation benchmarks.
  • Cross-cutting findings: 24 % to 35 % semantic correctness in NL-to-formal translation remains the primary specification bottleneck despite syntactic correctness above 90 % for LTL and above 96 % for PDDL.Verification over semantically incorrect specifications can provide false assurance rather than genuine safety.
  • Cross-cutting findings: Runtime monitoring is the most mature sub-field, with temporal, probabilistic, and rule-based monitors operating at millisecond overhead and reducing unsafe actions in closed-domain settings.Static workflow-graph verification and theorem-proving-based policy synthesis provide stronger guarantees, according to the reviewed synthesis.
  • Cross-cutting findings: 94 % of individually unsafe actions can be intercepted while SSR remains below 5 % in most settings because agents exploit alternative unsafe paths such as hallucinated user identifiers.This verifier tax separates action-level safety from task-level safety.
  • Cross-cutting findings: No included study satisfies more than three of five desiderata—soundness-preserving, complete, scalable, semantically grounded, and task-utility-preserving—simultaneously.The ideal system must detect all violations, avoid false positives, handle long-horizon open-ended tasks, acquire correct specifications, and preserve high SSR.
  • Research agenda: The research agenda prioritizes semantic correctness, task-level safety with verified re-planning, and scalability to long-horizon plans currently covering 5 to 30 actions.Proposed directions include constrained decoding and equivalence checking, plan-level policies with verified alternative fragments, and partial, abstraction-refined, compositional verification.
Loading 2608.14590v1…