Towards Verifiably Safe Tool Use for LLM Agents
Aarya Doshi, Yining Hong, Congying Xu, Eunsuk Kang, Alexandros Kapravelos, Christian Kästner
TL;DR
The paper tackles the challenge of verifiable safety for LLM-based agents that interact with tools, where traditional probabilistic safeguards are insufficient for enterprise contexts. It introduces a framework that fuses STPA safety engineering with information-flow control, implemented through an enhanced Model Context Protocol (MCP) to formalize data-flow and tool-sequence constraints. Key contributions include the SPEC formalism for safety requirements, a four-tier enforcement scheme (Blocklist, Mustlist, Allowlist, Confirmation), and a runtime labeling approach using key-value tags (capabilities, confidentiality, trust level) analyzed via Alloy for formal verification. The work aims to shift from ad hoc reliability fixes to formal guardrails that permit configurable autonomy, enabling safer and more controllable tool use by LLM agents in high-stakes settings.
Abstract
Large language model (LLM)-based AI agents extend LLM capabilities by enabling access to tools such as data sources, APIs, search engines, code sandboxes, and even other agents. While this empowers agents to perform complex tasks, LLMs may invoke unintended tool interactions and introduce risks, such as leaking sensitive data or overwriting critical records, which are unacceptable in enterprise contexts. Current approaches to mitigate these risks, such as model-based safeguards, enhance agents' reliability but cannot guarantee system safety. Methods like information flow control (IFC) and temporal constraints aim to provide guarantees but often require extensive human annotation. We propose a process that starts with applying System-Theoretic Process Analysis (STPA) to identify hazards in agent workflows, derive safety requirements, and formalize them as enforceable specifications on data flows and tool sequences. To enable this, we introduce a capability-enhanced Model Context Protocol (MCP) framework that requires structured labels on capabilities, confidentiality, and trust level. Together, these contributions aim to shift LLM-based agent safety from ad hoc reliability fixes to proactive guardrails with formal guarantees, while reducing dependence on user confirmation and making autonomy a deliberate design choice.