[2603.20449] Solver-Aided Verification of Policy Compliance in Tool-Augmented LLM Agents

Computer Science > Software Engineering arXiv:2603.20449 (cs) [Submitted on 20 Mar 2026] Title:Solver-Aided Verification of Policy Compliance in Tool-Augmented LLM Agents Authors:Cailin Winston, Claris Winston, René Just View a PDF of the paper titled Solver-Aided Verification of Policy Compliance in Tool-Augmented LLM Agents, by Cailin Winston and 2 other authors View PDF HTML (experimental) Abstract: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 ...