# Solver-Aided Verification of Policy Compliance in Tool-Augmented LLM Agents

arXiv: https://arxiv.org/abs/2603.20449 · HTML: https://mlsanity.com/paper/2603.20449/

## Key facts

- Cited by 16 papers in the map (data through 14 Oct 2026).
- Placed in Agent threats, guardrails and governance, one of 16 directions in LLM agents and tool use.
- Builds on 8 of its 13 references that are in the map.
- First posted on arXiv 20 Mar 2026.

## Placed in

- LLM agents and tool use / [Agent threats, guardrails and governance](https://mlsanity.com/agents/agent-threats-guardrails-and-governance/)

## Builds on (most cited first, 8 of 8)

- [τ-bench: A Benchmark for Tool-Agent-User Interaction in Real-World Domains](https://mlsanity.com/paper/2406.12045/) (2024)
- [API-Bank: A Comprehensive Benchmark for Tool-Augmented LLMs](https://mlsanity.com/paper/2304.08244/) (2023)
- [Chameleon: Plug-and-Play Compositional Reasoning with Large Language Models](https://mlsanity.com/paper/2304.09842/) (2023)
- [ToolkenGPT: Augmenting Frozen Language Models with Massive Tools via Tool Embeddings](https://mlsanity.com/paper/2305.11554/) (2023)
- [MetaTool Benchmark for Large Language Models: Deciding Whether to Use Tools and Which to Use](https://mlsanity.com/paper/2310.03128/) (2023)
- [TaskBench: Benchmarking Large Language Models for Task Automation](https://mlsanity.com/paper/2311.18760/) (2023)
- [A Complete Survey on LLM-based AI Chatbots](https://mlsanity.com/paper/2406.16937/) (2024)
- [Proof of Thought : Neurosymbolic Program Synthesis allows Robust and Interpretable Reasoning](https://mlsanity.com/paper/2409.17270/) (2024)

## Built on by (most cited first, 16 of 16)

- [Reason Less, Verify More: Deterministic Gates Recover a Silent Policy-Violation Failure Mode in Tool-Using LLM Agents](https://mlsanity.com/paper/2607.07405/) (2026)
- [AgentLTL: A Trace-Verification Framework for Measuring, Enforcing, and Training Procedural Compliance in Tool-Using LLM Agents](https://mlsanity.com/paper/2607.02599/) (2026)
- [PolicyGuard: A Dialogue-Grounded Sub-Agent Verifier for Policy Adherence in LLM Agents](https://mlsanity.com/paper/2606.29225/) (2026)
- [ATM: CID-Brokered Pre-Write Admission for Multi-Agent Code Co-Synthesis](https://mlsanity.com/paper/2607.00041/) (2026)
- [PolicyGuide: From Guarding One Action to Guiding the Whole Workflow for Policy-Compliant LLM Agents](https://mlsanity.com/paper/2608.19861/) (2026)
- [Owner-Harm: A Missing Threat Model for AI Agent Safety](https://mlsanity.com/paper/2604.18658/) (2026)
- [Prompts Don't Protect: Architectural Enforcement via MCP Proxy for LLM Tool Access Control](https://mlsanity.com/paper/2605.18414/) (2026)
- [When Retrieval Metrics Mislead: Measuring Policy Signal in Long-Horizon Tool-Use Agents](https://mlsanity.com/paper/2606.23937/) (2026)
- [Learning Context-Free Grammars for Grammar-Constrained Decoding via Declarative Agentic Programming with Guarantees](https://mlsanity.com/paper/2608.05493/) (2026)
- [Multi-Agent Scheduling with LLM-Assisted Contract Net Negotiation for Stream Processing in Mobile Edge Computing](https://mlsanity.com/paper/2608.12371/) (2026)
- [CAPRI: Contract-Aware Proof Repair for Isabelle](https://mlsanity.com/paper/2608.13459/) (2026)
- [STAGE: Stateful Translation to Agentic Graph Execution with Policy-Scoped Context and Deterministic Control](https://mlsanity.com/paper/2608.22538/) (2026)
- [Policy Loopholes in Agent Evaluation: When Policy Ambiguity Masquerades as Agent Error](https://mlsanity.com/paper/2609.14400/) (2026)
- [What Can Component-Replacement Evidence Establish? A Critical Scoping Review of Local Decisions in LLM Agents](https://mlsanity.com/paper/2609.39989/) (2026)
- [NOMOS: Compiling Written Policies into Statically Verified Tool-Call Gates for LLM Agents](https://mlsanity.com/paper/2610.11030/) (2026)
- [MENTOR: Procedural Shielding of Tool-Using LLM Agents](https://mlsanity.com/paper/2610.17039/) (2026)

## Abstract (arXiv)

Tool-augmented Large Language Models (TaLLMs) extend LLMs with the ability to invoke external tools, enabling them to interact with real-world environments. However, a major limitation in deploying TaLLMs in sensitive applications such as customer service and business process automation is a lack of reliable compliance with domain-specific operational policies regarding tool-use and agent behavior. Current approaches merely steer LLMs to adhere to policies by including policy descriptions in the LLM context, but these provide no guarantees that policy violations will be prevented. In this paper, we introduce an SMT solver-aided framework to enforce tool-use policy compliance in TaLLM agents. Specifically, we use an LLM-assisted, human-guided approach to translate natural-language-specified tool-use policies into formal logic (SMT-LIB-2.0) constraints over agent-observable state and tool arguments. At runtime, planned tool calls are intercepted and checked against the constraints using the Z3 solver as a pre-condition to the tool call. Tool invocations that violate the policy are blocked. We evaluated on the TauBench benchmark and demonstrate that solver-aided policy checking reduces policy violations while maintaining overall task accuracy. These results suggest that integrating formal reasoning into TaLLM execution can improve tool-call policy compliance and overall reliability.