Source-linked AI summary
VeriGuard: Enhancing LLM Agent Safety via Verified Code Generation
Lesly Miculicich, Mihir Parmar, Hamid Palangi, Krishnamurthy Dj Dvijotham, Mirko Montanari, Tomas Pfister, Long T. Le
TL;DR
LLM agents lack formal guarantees that their actions satisfy safety constraints, while existing safeguards are largely reactive. VeriGuard generates and refines verified policies offline, then enforces them during execution; experiments report perfect EICU-AC accuracy, superior Mind2Web-SC recall, and near-zero attack success rates. Its guarantees depend on user validation of LLM-generated constraints and the capabilities of the Nagini verifier.
Problem
Existing LLM-agent safeguards are largely empirical and reactive, lacking formal specifications and provable compliance guarantees against novel attacks.
Method
VeriGuard generates executable policies and formal constraints, refines them through validation, testing, and formal verification, and integrates verified policies as runtime enforcement mechanisms.
Results
VeriGuard achieves perfect accuracy on EICU-AC, outperforms all baselines on Mind2Web-SC recall, and reduces attack success rates to near-zero across reported benchmarks.
Takeaways & Limitations
The results support using interactive verification and runtime policy enforcement to prevent unsafe agent operations while maintaining task success.
Takeaways & Limitations
Constraint soundness depends on manual user validation, and Nagini may have limited grammar for complex properties.
Abstract
from arXiv · showhide
The deployment of autonomous AI agents in sensitive domains, such as healthcare, introduces critical risks to safety, security, and privacy. These agents may deviate from user objectives, violate data handling policies, or be compromised by adversarial attacks. Mitigating these dangers necessitates a mechanism to formally guarantee that an agent's actions adhere to predefined safety constraints, a challenge that existing systems do not fully address. We introduce VeriGuard, a novel framework that provides formal safety guarantees for LLM-based agents through a dual-stage architecture designed for robust and verifiable correctness. The initial offline stage involves a comprehensive validation process. It begins by clarifying user intent to establish precise safety specifications. VeriGuard then synthesizes a behavioral policy and subjects it to both testing and formal verification to prove its compliance with these specifications. This iterative process refines the policy until it is deemed correct. Subsequently, the second stage provides online action monitoring, where VeriGuard operates as a runtime monitor to validate each proposed agent action against the pre-verified policy before execution. This separation of the exhaustive offline validation from the lightweight online monitoring allows formal guarantees to be practically applied, providing a robust safeguard that substantially improves the trustworthiness of LLM agents.
1. Introduction
LLM agents can perform complex autonomous tasks, but their flexible outputs lack reliable safety assurances and remain vulnerable to errors, adversarial inputs, and unforeseen behaviors. VeriGuard addresses this gap by generating, testing, and formally verifying policies for correct-by-construction agent actions.
- VeriGuard targets the reliability gap caused by LLM agents producing solutions without assurances against subtle errors, security flaws, and emergent behaviors.
- Existing sandboxing, filtering, and rule-based guardrails react to patterns and struggle with dynamic action spaces, novel adversarial inputs, and unforeseen edge cases.
- VeriGuard generates functional action code together with formal safety specifications, then subjects both artifacts to automated verification.
- Failed verification produces counterexamples or logical critiques that guide iterative correction toward verifiably safe code.
- The framework contributes LLM-driven generation and refinement of verifiable code plus empirical validation across challenging safety domains.
2. Related Work
Related work established increasingly autonomous LLM agents and a broad ecosystem of empirical safety mechanisms. However, existing safeguards remain largely reactive and lack formal, provable guarantees of safe behavior.
- 2.1. LLM Agents and the Emergence of Autonomous Systems: LLM agents evolved from reasoning-and-acting systems into autonomous agents that decompose goals, manage memory, and execute realistic multi-step web tasks.
- 2.2. LLM Safety, Alignment, and Guardrails: Safety research includes input/output filtering, prompt restrictions, red teaming, and safety-tuned models for tool use.
- 2.2. LLM Safety, Alignment, and Guardrails: GuardAgent and ShieldAgent add LLM-based protective layers intended to detect or prevent unsafe autonomous-agent behaviors.
- 2.2. LLM Safety, Alignment, and Guardrails: Existing guardrails are largely empirical and reactive, so novel attacks can circumvent them because formal safe-behavior specifications and compliance verification are missing.
- 2.3. Formal Methods and LLMs: Formal-methods research explores using LLMs to generate code, specifications, and verification artifacts for high-assurance software development.
3. Methodology
VeriGuard converts natural-language safety requests and agent specifications into executable policies with formal constraints, refines them through validation, testing, and verification, and enforces verified policies during agent execution. Its runtime layer maps agent data to policy arguments and supports multiple violation-response strategies.
- VeriGuard has two stages: policy generation with iterative refinement, followed by runtime policy enforcement at agent action points.
- 3.2.1. Policy Generator: The policy generator translates user intent and agent specifications into executable policy code and formal preconditions and postconditions.
- 3.2.2. Refinement Process: Validation resolves ambiguities and semantic inconsistencies through analysis queries, user feedback, or autonomous default assumptions.
- 3.2.2. Refinement Process: Code testing generates PyTest cases for typical and edge-case scenarios, iteratively refining the policy until tests pass or the iteration limit is reached.
- 3.2.2. Refinement Process: Formal verification proves that policy code satisfies specified preconditions and postconditions, returning counterexamples or error traces when the contract is violated.
- 3.3. Policy Enforcement: At runtime, an LLM-based mapping function converts system data into policy arguments, while enforcement can terminate tasks, block actions, or halt individual tool calls.
4. Experiments
The experiments evaluate VeriGuard across security and access-control benchmarks using attack prevention, task utility, and classification metrics. VeriGuard achieves near-zero attack success with strong task success on ASB, perfect accuracy on EICU-AC, and higher recall than baselines on Mind2Web-SC.
- Benchmarks: The evaluation spans ASB attacks, ICU database access control, and safety-constrained web tasks, with comparisons against specialized and general-purpose defenses.ASB covers prompt injection, memory poisoning, and plan-of-thought backdoors; the other benchmarks test restricted data access and prohibited web activities.
- Evaluation metrics: ASB measures defense quality with Attack Success Rate and operational interference with Task Success Rate.ASR is the ratio of successful attacks to attack attempts, while TSR is the ratio of successfully completed original tasks to attempted tasks.
- Evaluation metrics: EICU-AC and Mind2Web-SC treat access control as binary Allow-versus-Deny classification and report Accuracy, Precision, and Recall.Correctly stopping a forbidden action is the desired outcome in these benchmarks.
- ASB: Near-zero ASR with the highest TSR demonstrates VeriGuard’s strongest ASB security–utility trade-off across three backbone models.The evaluation compares attack success and task success against No Defense, No Attack, and several defenses.
- EICU-AC and Mind2Web-SC: Perfect accuracy on EICU-AC and the best recall on Mind2Web-SC show strong access-control violation detection against the evaluated baselines.VeriGuard achieves high recall on both datasets, while AGrail performs better on accuracy and precision in the reported comparison.
5. Analysis
The analysis finds that layered VeriGuard components reduce attack success while preserving task success, with CRP + TEH offering the strongest security–utility balance. It also identifies limitations involving generated constraints, verification tooling, language portability, and sophisticated adaptive attacks.
- 5.1. Ablation Study of VeriGuard Components: 53.5% average ASR falls to 9.97% after Policy Generation and ultimately reaches 0% across all attack vectors after the full defense pipeline.Validation reduces Memory Poisoning ASR from 31.75% to 15% before later stages neutralize remaining threats.
- 5.1. Ablation Study of VeriGuard Components: Average TSR rises from 51.87% to 63.25% as defense layers are added, indicating that the security gains do not incur the reported performance trade-off.The result is reported for the ASB ablation using Gemini-2.5-Flash with default parameters.
- 5.2. Evaluating Integration Methods: Security vs. Utility: 0.1% average ASR and 63.6% average TSR make CRP + TEH the strongest security–utility combination among the evaluated integration strategies.The combination uses CRP’s high task success with TEH’s fine-grained blocking.
- 5.2. Evaluating Integration Methods: Security vs. Utility: Collaborative Re-planning alone reaches 11.9% average ASR, whereas CRP + TEH combines safer intervention with high task success.CRP is less invasive but does not guarantee security because the agent may still perform unsafe actions.
- 5.3. Limitations: VeriGuard’s soundness depends on user validation of LLM-generated constraints and on Nagini’s expressiveness, while sophisticated attacks may exceed the hybrid architecture’s reasoning capacity.Extending the framework to other programming languages is also described as a non-trivial implementation challenge.
6. Conclusion
The conclusion presents VeriGuard as a proactive framework for formally checking LLM-agent policies and actions against safety specifications. It reports near-zero attack success with high task success and identifies verification scalability and autonomous specification generation as future directions.
- 6. Conclusion: VeriGuard formally checks agent-generated policies and actions against predefined safety specifications, moving beyond reactive pattern matching.The framework is presented as a proactive, provably-sound approach to agent safety.
- 6. Conclusion: Experiments on ASB, EICU-AC, and Mind2Web-SC report near-zero attack success while maintaining a high degree of task success.The framework also supports flexible policy enforcement strategies for different operational needs.
- 6. Conclusion: Future work should address the scalability and efficiency of formal verification and the autonomous generation of safety specifications.These are identified as promising research avenues building on VeriGuard.
A. Experiment Details
This section introduces the implementation of VeriGuard with the agent systems discussed earlier.
- A. Experiment Details: The implementation section details VeriGuard with the agent systems mentioned in Section 4.
Prompt: Policy Code Generation
The prompt directs an expert AI security agent to generate a Python security-policy function from a high-level user request.
- Prompt: Policy Code Generation: The policy-generation prompt asks an expert AI security agent to produce a Python security policy function from a high-level user request.
## CONTEXT
Given a security request and target agent specification, the system generates both extraction parameters and Python policy code.
- The generation step outputs a list of parameters to extract from runtime data.
- It also produces Python code implementing the policy function.
- These outputs connect the agent’s security request and specification to an executable policy representation.
## OUTPUT REQUIREMENTS
The output requirements define structured interfaces for extracting arguments, implementing policy functions, generating logical statements and tests, and embedding Nagini contracts.
- The policy output must provide extracted arguments and a policy function with a prescribed Python interface.
- The policy function must be named policy, accept arguments: dict, return (bool, str), document its policy, and avoid external libraries.
- Logical-statement generation translates security policies, agent descriptions, and variables into discrete, testable IF-THEN-style conditions.
- The verification workflow checks specifications and statements for ambiguity, assumptions, counterexamples, and logical errors, then requests clarifications or corrections.
- Ambiguity resolution uses user specifications as the primary intent source and agent specifications as technical context before compiling finalized requirements and assumptions.
- Generated tests should cover happy paths, edge cases, and error handling, while corrected functions receive Nagini Requires and Ensures contracts derived from logical statements.