Formal Policy Enforcement for Agentic Systems

Nils Palumbo; Sarthak Choudhary; Jihye Choi; Guy Amir; Prasad Chalasani; Isil Dillig; Somesh Jha

cs.CRFeb 18, 2026

Formal Policy Enforcement for Agentic Systems

Authors: Nils Palumbo, Sarthak Choudhary, Jihye Choi, Guy Amir, Prasad Chalasani, Isil Dillig, Somesh Jha

Organizations: University of Wisconsin–Madison · Cornell University · Langroid

Abstract

As agentic computing systems grow increasingly popular, they raise serious security concerns due to their susceptibility to various attacks. While prior research efforts aim to mitigate these concerns, they are often too coarse-grained and offer no formal correctness guarantees. In this work, we present a novel approach to agentic security based on runtime monitoring. Our method allows the user to specify their intended policy in Datalog and enforces the specified policy at runtime by constructing event graphs. When an agent is about to execute an action such as a tool call, our approach determines whether the action would violate the policy in light of the current system state and the history of past events. The action is then blocked or permitted accordingly. We implemented our approach and evaluated it across multiple benchmarks, demonstrating its merits in real-world settings. We view this work as a step towards agentic systems that are provably safe and secure.

Figures & tables

Panel of Figure 1 — Figure 1: FORGE architecture. Instrumentation records agent events and forwards them to the observability service, which maintains an event graph of their dependencies. Before a candidate action executes, the reference monitor constructs a query from the action, authenticated identity, and relevant graph facts. The policy engine evaluates the query against the Datalog policy and returns a verdict that causes the action to be released or blocked.

Panel of Figure 2 — Figure 2: Event graph for the running prompt-injection example. Edges point from an event to a later event that depends on it, with only immediate dependencies drawn. Badges are the labels derived by the policy of Listing 4 : filled at the base facts UntrustedInput(v3) and SensitiveInput(v5) , outlined where the recursive rules propagate them. The candidate action $v_{6}$ is an external email send carrying both labels, so the policy denies it.

Instrumented	Policy	ASR	Util.	Time	Cost
Yes	MLS (TOP_SECRET)	0/5	5/5	7.9	0.35
	MLS (SECRET)	0/5	5/5	7.6	0.38
	Toxic Flow	0/5	5/5	11.1	0.47
No	Anti-Exfiltration Prompt	5/5	5/5	5.3	0.30

Table 1: Information flow policy evaluation (5 trials each). ASR = Attack Success Rate. Utility (benign task completion) is 100% for all rows. Time (s) and cost (USD cents) are means per scenario.

Table 2:

\tau^{2}

-Bench results: (a) task success, (b) time and agent + user API cost, and (c) denial cohorts by domain. Time and cost are means per trial. NI = noninstrumented, I = instrumented. passˆk is the task-average probability that all

k

sampled trials succeed. 4 4 4 Costs exclude the external judge and retried-attempt cost (see Appendix E.5 ).

Figure 4:

\tau^{2}

-Bench passˆk by domain. passˆk is the task-average probability that all

k

sampled trials succeed. Dashed: noninstrumented (NI); solid: instrumented (I). Claude = Claude Opus 4.5, GPT = GPT-5.2, Gemini = Gemini 3.1 Pro Preview.

Figure 5: Authorization measurements on

\tau^{2}

-Bench airline. (a) Server-side, client-side, and replay round-trip latency: median (solid) and p99 (dashed), with 95% whole-session bootstrap intervals for live medians. (b) Authorization throughput on a warmed, fixed graph: mean

\pm

sample SD over five replay trials.

Table 3: MALADE evaluation (5 trials per question). NI = noninstrumented, I = instrumented. Compliance: no FDA-label data returned before approved registration.

	Without AgentDojo Built-in Defense				With AgentDojo Built-in Defense
	Task	Utility	ASR	ASR	Task	Utility	ASR	ASR
Configuration	Utility	Under Atk		(Effect)	Utility	Under Atk		(Effect)
No runtime defense	$79.0\pm 2.02$	$56.9\pm 1.43$	$25.2\pm 1.12$	$25.2\pm 1.12$	$83.7\pm 0.41$	$72.5\pm 0.81$	$14.1\pm 0.46$	$14.1\pm 0.46$
Tool-call filter	$72.4\pm 2.39$	$63.5\pm 0.83$	$4.2\pm 0.18$	$4.2\pm 0.18$	$73.4\pm 3.35$	$69.5\pm 0.74$	$3.1\pm 0.48$	$3.1\pm 0.48$
FORGE (FIDES IFC policy)	$32.2\pm 2.39$	$31.0\pm 0.55$	$1.5\pm 0.40$	$1.0\pm 0.41$	$33.2\pm 1.89$	$34.4\pm 0.51$	$0.6\pm 0.12$	$0.3\pm 0.20$
FORGE (provenance policy)	$57.3\pm 3.49$	$49.4\pm 0.59$	$1.7\pm 0.31$	$0.8\pm 0.15$	$62.5\pm 1.40$	$63.8\pm 0.91$	$0.9\pm 0.30$	$0.2\pm 0.12$

Table 4: AgentDojo security and task utility. Cells report mean percentages

\pm

population SD across five sweeps. ASR (Effect) reclassifies attacks scored as successful solely from fully denied attacker-goal tool calls as failed attacks, retaining all attacked runs in the denominator. Higher utility and lower ASR are better.

Approach	Expressive Policy Language	Recursive Queries	Causal Dependencies	Multi Agent Support	Deterministic Enforcement
Progent [ 56 ]	✓	✗	✗	✗	✓
NeMo Guardrails [ 44 ]	✓	✗	✗	✗	✓
Invariant Guardrails [ 37 ]	✓	✗	✗	✗	✓
AgentSpec [ 61 ]	✓	✗	✗	✗	✓
ShieldAgent [ 14 ]	✓	✗	✗	✗	✓
GuardAgent [ 63 ]	✓	✗	✗	✗	✗

Table 5: Comparison of runtime policy enforcement approaches for LLM-based agentic systems.

Appendix figures & tables4 assets

Supplementary material from the paper’s appendix.

Appendix

Agent	$\begin{array}[]{c}\textbf{Trust}\\ \textbf{Relationship}\end{array}$	Channel	$\begin{array}[]{c}\textbf{CanQuery}\\ \textbf{Targets}\end{array}$
personal	Self (private)	iMessage	projects
manager	Direct manager	Slack DM	personal
projects	Project team	Slack channel	personal
client	External client	Email	projects

Appendix

Table 6: Agent deployment. Four of twelve possible directed query edges are authorized.

Table 7:

\tau^{2}

-Bench blocked-action cohorts by domain. NI = noninstrumented, I = instrumented.

\Delta

is percentage points (I

-

NI). Rows labeled All are weighted averages across models, using cohort pair counts.

Rule	Exec.	Trials	Full reward
Product access before authentication	32	17	13
Address update after item mod (later turn)	3	3	3
Address update after item mod (same batch) *	8	8	6

Appendix

Table 8: Noninstrumented retail global-rule executions not explicitly scored.

	Successful trials
Policy	Task 8	Task 43	Task 47	Reward
Variant 1	5/5	5/5	4/5	0.933
Variant 2	5/5	5/5	5/5	1.000
Variant 3	5/5	5/5	5/5	1.000
Variant 4	5/5	3/5	5/5	0.867
Variant 5	5/5	0/5	5/5	0.667

Appendix

Table 9: Enforcement performance of five independently translated airline policies on three held-out tasks. Entries report successful trials out of five. Reward is the mean over all fifteen simulations. The final row reports the mean and standard deviation across the five translated policies. The reference policy is the policy presented in Section E.2.1 .

Runtime Enforcement for AI Agents

Runtime enforcement for AI agents checks and constrains actions as they execute, helping prevent unsafe or unauthorized effects.

See all 273 papers

Autoformalization of Agent Instructions into Policy-as-Code
Jun 25, 2026Adam Mondl, Matthew Maisel, John H. BrockFormal Verification LLM Agent Safety
Sondera
Deontic Policies for Runtime Governance of Agentic AI Systems
Jun 17, 2026Anupam Joshi, Tim Finin, Karuna Pande Joshi +1Ontology-Based Reasoning AI Agent Security
CSEE Department UMBC Baltimore, MD, USA · Center for AI UMBC Baltimore, MD, USA · Information Systems Department UMBC Baltimore, MD, USA +1
Governance by Construction for Generalist Agents
May 20, 2026Segev Shlomov, Iftach Shoham, Alon Oved +7LLM Guardrails AI Agent Governance
IBM Haifa, Israel

Jun 25, 2026J/K move · Enter open · S save

Autoformalization of Agent Instructions into Policy-as-Code

Adam Mondl, Matthew Maisel, John H. Brock

Sondera

Formal Verification LLM Agent Safety

Open paper AskPDF arXiv

Agent safety in high-stakes domains requires formal policy enforcement, but most existing approaches either rely on probabilistic guardrails (fine-tuned classifiers, prompt-based steering) that offer no formal guarantees, or on hand-coded symbolic enforcement that does not scale to the breadth of real policy specifications. We present an autoformalization pipeline that translates agent prompts, MCP tool descriptions, and natural language policy documents into formally verified policies using an LLM-based generator-critic loop. The resulting policies are written in the Cedar Policy Language. On the MedAgentBench benchmark, our autoformalized policies cover substantially more of the source natural-language specification than the hand-coded symbolic enforcement in prior work.

Abstract

Runtime Enforcement for AI Agents

Explore similar work

Autoformalization of Agent Instructions into Policy-as-Code

Deontic Policies for Runtime Governance of Agentic AI Systems

Governance by Construction for Generalist Agents