Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

VeriGuard tackles the safety challenges of autonomous LLM agents in high-stakes domains by marrying formal verification with runtime enforcement. It introduces a two-stage pipeline: offline policy generation, validation, and formal verification to yield a correct-by-construction safety policy, and online monitoring that enforces the verified policy before every action. Empirical results across ASB, EICU-AC, and Mind2Web-SC demonstrate substantial reductions in attack success while preserving task utility, with a hybrid Collaborative Re-planning plus Tool Execution Halt strategy often delivering the best security-utility balance. The work advances practical, provable safety for LLM-driven agents and points to scalable verification and specification generation as promising directions for real-world deployment.

Abstract

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.

VeriGuard: Enhancing LLM Agent Safety via Verified Code Generation

TL;DR

VeriGuard tackles the safety challenges of autonomous LLM agents in high-stakes domains by marrying formal verification with runtime enforcement. It introduces a two-stage pipeline: offline policy generation, validation, and formal verification to yield a correct-by-construction safety policy, and online monitoring that enforces the verified policy before every action. Empirical results across ASB, EICU-AC, and Mind2Web-SC demonstrate substantial reductions in attack success while preserving task utility, with a hybrid Collaborative Re-planning plus Tool Execution Halt strategy often delivering the best security-utility balance. The work advances practical, provable safety for LLM-driven agents and points to scalable verification and specification generation as promising directions for real-world deployment.

Abstract

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.

Paper Structure

This paper contains 41 sections, 2 equations, 2 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. LLM Agents and the Emergence of Autonomous Systems
  4. LLM Safety, Alignment, and Guardrails
  5. Formal Methods and Verifiable Code Generation
  6. Methodology
  7. Task Definition
  8. Policy Generation
  9. Policy Enforcement
  10. Framework
  11. Policy Generator
  12. Refinement Process
  13. Validation
  14. Code Testing
  15. Verification
  16. ...and 26 more sections

Figures (2)

  • Figure 1: VeriGuard overview which includes Policy generation and Policy enforcement. The verified policy is integrated into the agent as a runtime safeguard, intercepting and preventing harmful actions.
  • Figure 2: (a) shows the ASR is systematically reduced to 0% across all evaluated attack types. (b) shows the TSR increases as defense layers are added.