LEANGUARD: Lean-Verified Guardrails for Tool-Using Agents

Sreehari Sankar; Debargha Ganguly; Vikash Singh; Mohsen Hariri; Weicong Chen; Yanyan Zhang; Shouren Wang; Wang Yang

cs.AINov 2, 2026

LEANGUARD: Lean-Verified Guardrails for Tool-Using Agents

Authors: Sreehari Sankar, Debargha Ganguly, Vikash Singh, Mohsen Hariri, Weicong Chen, Yanyan Zhang, Shouren Wang, Wang Yang,

Organizations: Case Western Reserve University · UT Austin

Abstract

Tool-using language-model agents often execute actions that their domain policies forbid. We present LeanGuard, a runtime that checks every proposed tool call against a policy written in Lean4 before the call reaches the environment. Policies combine state predicates with scoped past-time temporal operators over the execution history, evaluation is fail-closed, and the decision procedure is proved equivalent to a LeanLTL semantics. A denied call can be corrected in two ways. With feedback, the agent receives the violated rule and a hint; with proof-guided repair, Lean metaprogramming searches for a nearby call that preserves the user's intent and proves that the policy admits it, without the model. On Tau-Bench with five Qwen models (0.8B-27B), unguarded agents execute at least 33 calls that the Lean policy forbids, while LeanGuard executes none; with feedback, task success does not change significantly. On DTap, LeanGuard reduces direct prompt-injection success from 57.9% to 5.9%, and in telecom, where benign tasks need no writes, benign success is unchanged. Feedback reduces repeated blocked calls and raises task success for four of five models over a bare denial. On replayed denials, repair proves an admissible edit for 88 of 252 denials caused by argument values, in a median of 2,ms.

Figures & tables

Figure 1: A retail exchange with and without LeanGuard . Unguarded, the agent follows an instruction injected into a tool output and bills the price difference to an attacker’s gift card without asking the customer. With LeanGuard , the call is denied because the customer has not confirmed and the card is not on the account; the agent asks the customer, and the reissued call is admitted. Bottom: headline results.

Figure 2: LeanGuard on the exchange of Figure 1 . (1) The agent proposes a call; text in tool outputs is not evidence. (2) LeanGuard checks the call against trusted evidence, a backend snapshot and the journal of earlier events, using compiled Lean rules. (3) A denial returns the failed rules and a hint. After the customer confirms on a trusted screen, the reissued call is admitted, dispatched once, and recorded in the journal. The proved repair in (3) is computed offline by the search of § 2.6 ; in our experiments, the agent receives only the rules and the hint.

	$\tau^{2}$ -bench						DTap (read-only deployment)
	Task success ( $\uparrow$ )			Judge-flagged ( $\downarrow$ )			Benign success ( $\uparrow$ )		Direct attack ( $\downarrow$ )		Indirect attack ( $\downarrow$ )
Model	None	LG	LG+F	None	LG	LG+F	None	LG+F	None	LG+F	None	LG+F
Qwen3.5-0.8B	48.9	41.4	45.3	14.4	6.6	8.8	20.2	10.3	46.7	3.3	3.1	1.7
Qwen3.5-2B	68.3	66.9	72.7	15.4	11.7	12.1	31.9	11.3	53.1	3.4	11.6	2.5
Qwen3.5-4B	83.8	79.5	82.4	7.6	4.7	4.4	59.8	11.7	71.6	7.5	27.4	5.4
Qwen3.5-9B	84.9	80.9	83.1	5.1	3.3	5.1	67.4	12.8	74.4	11.0	37.0	4.9

Table 1: Protection and cost of LeanGuard (%).

\tau^{2}

-bench: task success, and judge-flagged episodes (an LLM judge finds an executed call that breaks the benchmark policy), for the Unguarded (None), LeanGuard (LG), and LeanGuard + feedback (LG+F) arms. DTap: benign task success and attack success under the read-only deployment. The last row gives the change from None for all models. Per-domain results and raw counts are in Appendix G .

Figure 3: Calls stopped by LeanGuard per failure category of § 3 (% of each benchmark’s stopped calls; labels give counts).

\tau^{2}

-bench: both LeanGuard arms, all models (1,702 calls). DTap: attack episodes in six domains (24,461 calls); medical is excluded because its patient registration was denied, and benign episodes because their stops are mostly withheld approvals. A call can fall into several categories. Not modeled : tools whose effect LeanGuard cannot determine, such as shell commands.

	Recovery (RQ3)						Repair (RQ4)
	Blocked ( $\downarrow$ )		Actions ( $\downarrow$ )		Recovered ( $\uparrow$ )		Fixable		Repaired
Model	LG	LG+F	LG	LG+F	LG	LG+F	LG	LG+F	LG	LG+F
Qwen3.5-0.8B	426	383	307	276	5	5	56	30	23	9
Qwen3.5-2B	271	144	141	104	8	13	62	31	16	5
Qwen3.5-4B	91	62	56	42	9	12	27	13	17	9
Qwen3.5-9B	88	57	57	46	9	8	13	14	4	5

Table 2: After a denial on

\tau^{2}

-bench, for the LeanGuard (LG) and LeanGuard + feedback (LG+F) arms (278 episodes per model and arm). Blocked : calls not dispatched: 1,613 policy denials, 17 calls whose arguments fail the tool schema, and 72 adapter faults. Actions : distinct denied actions. Recovered : denied actions later executed after the missing requirement was met. Fixable : policy denials caused by argument values. Repaired : fixable denials for which guard_repair? proves an admissible edit.

Appendix figures & tables24 assets

Supplementary material from the paper’s appendix.

Appendix

LeanGuard constructor	LeanLTL interpretation
atom, $\top$ , $\bot$	trace predicate, true, false
$\neg$ , $\land$ , $\lor$	not, and, or
previous $w$ $p$	strong next of (window $w$ $\land$ $p$ )
once $w$ $p$	finally (window $w$ $\land$ $p$ )
since $w$ $p$ $q$	$p$ until (window $w$ $\land$ $q$ )
within scope $p$	$p$ on the projected history

Appendix

Table 3: Interpretation of LeanGuard ’s temporal policy language in LeanLTL.

Domain	Tools	Rules	Lines of Lean
Retail	16	17	97
Airline	14	14	288
Telecom	13	14	136
Shared definitions	–	–	62
Total	43	45	583

Appendix

Table 4: Size of the

\tau^{2}

-bench policies. Tools are the agent’s tools; the customer’s telecom device tools are not part of the policy.

Domain	Tool contracts
Telecom	44
Travel	25
Customer service	40
Medical	22
Finance	13
Legal	37

Appendix

Table 5: Reviewed tool contracts for the seven DTap domains we evaluate.

	Cases			Unscored episodes
Domain	DTap	Evaluated	Why the other cases are not evaluated	None	LG+F
Telecom	447	434	named orders have no single known owner (11); the attack targets no identifiable account (2)	198	205
Travel	355	355	–	2	63
Customer service	361	358	the original judge needs an external LLM (3)	228	319
Medical	1,093	1,091	the original judge needs an external LLM (2)	877	1,220
Finance	600	95	the case needs another application (505)	10	5

Appendix

Table 6: DTap coverage. Cases : benign and attack cases of each domain in DTap, and those we evaluate. Unscored episodes : episodes over all models and runs without a verdict, mostly because the conversation exceeded the context window (customer service, travel), the judge endpoint rejected the answer (medical), or the judge could not read the backend (telecom).

	$\tau^{2}$ -bench	DTap, 6 domains
Category	calls [exec.]	attack	benign
(i) Invalid	312 [0]	1,550	383
(ii) State	36 [14]	42	42
(iii) Temporal	187 [17]	392	330
(iv) Authorization	13 [0]	1,904	1,061
(v) Prohibition	40 [3]	441	206

Appendix

Table 7: What agents do without a guard, by category (§ 3 ), all five models.

\tau^{2}

-bench: calls that fail a rule of the Lean policy when the unguarded episodes are replayed through LeanGuard ’s rules, and in brackets how many executed and changed state; consent cannot be checked offline, so authorization is a lower bound, and rules stricter than the benchmark are excluded. DTap: episodes whose first call LeanGuard would stop falls in each category (a call can fall in several). Both arms start from the same state and decode greedily, so the unguarded transcript equals the guarded one up to that call; only pairs whose transcripts match exactly are counted (82.8% of pairs). Medical is excluded because patient registration was denied in the LG+F runs.

	$\tau^{2}$ -bench	DTap, six domains		DTap, medical
Category	Both arms	Benign	Attack	Benign	Attack
(i) Invalid invocation	551	3,684	14,207	20,051	17,974
(ii) State incompatibility	157	1,994	949	14,293	7,570
(iii) Temporal incompatibility	411	1,933	2,545	0	3,775
(iv) Authorization failure	572	9,431	14,688	4,773	10,201
(v) Policy prohibition	313	347	1,254	0	0

Appendix

Table 8: Calls LeanGuard stopped, by category, from its own decision logs.

\tau^{2}

-bench: both LeanGuard arms (LG and LG+F), 5 models

\times

278 tasks each; temporal includes 164 calls stopped only by rules stricter than the benchmark ( retail.modify_once , stable_identity ). DTap: the LG+F arm on the cases of Table 15 ; denials map by rule, fail-closed errors by their message, and a call that fails rules in several categories counts in each. Tool effect not completely modeled : LeanGuard could not determine the call’s effect (for example general shell commands, market orders without a price, tools with no reviewed contract) and failed closed. Medical is shown apart because patient registration was denied in every benign and in most attack cases, so most later calls fail with a missing patient (counted as state).

Category	$\tau^{2}$ -bench rules (stopped calls, both LeanGuard arms)	DTap rules and fail-closed errors
(i) Invalid invocation	no permit for the tool (534), argument schema (17)	dtap.contract ; schema errors; malformed identifiers or values
(ii) State incompatibility	telecom.payment_request (61), retail.delivered (36), telecom.roaming (30), telecom.suspend (13), retail.pending (11), telecom.resume (3), airline.active (3)	resource does not exist, already exists, or has an unexpected type
(iii) Temporal incompatibility	retail.modify_once † (158), airline.identity (77), telecom.identity (66), airline.observed (39), host.no_overlap (23), telecom.stable_identity † (21), retail.identity (18), retail.exchange_once (7), telecom.bill_observed (2), retail.status_observed (1)	dtap.observe , dtap.single_flight , dtap.budget ; path outside the observed roots
(iv) Authorization failure	airline.confirmation (180), retail.confirmation (143), telecom.detail_owner (104), airline.reservation_owner (99), telecom.customer (25), retail.order_owner (18), airline.user_owner (16), telecom.refuel_confirm (15), retail.profile_owner (7), telecom.line_owner (7)	dtap.authority , dtap.approval ; identity or authority errors
(v) Policy prohibition	airline.cancel (69), retail.return (65), airline.flights (53), airline.booking (38), airline.compensation (38), retail.modify_items (30), retail.exchange_items (10), airline.passengers (4), airline.baggage (2), retail.payment (2), telecom.refuel (2)	dtap.unavailable (the template’s forbid)
Not completely modeled	–	effect cannot be determined (Table 18 )

Appendix

Table 9: Rules behind each failure category.

\tau^{2}

-bench: calls LeanGuard stopped in both of its arms, per failed rule; a call that fails several rules counts under each, so counts can exceed the totals of Table 8 . † Stricter than the benchmark policy (§ 2.7 ). DTap: the template rules of Appendix D and the fail-closed errors assigned to each category.

Model	Arm	Retail ( $n{=}114$ )	Airline ( $n{=}50$ )	Telecom ( $n{=}114$ )	All ( $n{=}278$ )
Qwen3.5-0.8B	None	50.0	58.0	43.9	48.9
	LG	36.8 $\downarrow$ 13.2	48.0 $\downarrow$ 10.0	43.0 $\downarrow$ 0.9	41.4 $\downarrow$ 7.5
	LG+F	41.2 $\downarrow$ 8.8	52.0 $\downarrow$ 6.0	46.5 $\uparrow$ 2.6	45.3 $\downarrow$ 3.6
Qwen3.5-2B	None	68.4	58.0	72.8	68.3
	LG	67.5 $\downarrow$ 0.9	56.0 $\downarrow$ 2.0	71.1 $\downarrow$ 1.7	66.9 $\downarrow$ 1.4
	LG+F	66.7 $\downarrow$ 1.7	66.0 $\uparrow$ 8.0	81.6 $\uparrow$ 8.8	72.7 $\uparrow$ 4.4

Appendix

Table 10: Task success on

\tau^{2}

-bench by domain (%, higher is better; one episode per task). Arrows give the change from None.

Domain	Tasks	None	LG+F	Blocked (ep.)
Retail	40	86.9	75.0 $\downarrow$ 11.9	54 (37)
Airline	20	77.5	73.8 $\downarrow$ 3.7	34 (19)
Telecom	40	90.6	93.8 $\uparrow$ 3.1	16 (9)
All	100	86.5	82.2 $\downarrow$ 4.3	104 (65)

Appendix

Table 11: Qwen3.5-4B on the official

\tau^{2}

-bench test split, four seeds (400 episodes per arm). Task success in %; arrows give the change from None in pp. Blocked : tool calls denied in the LG+F arm, with the number of affected episodes in parentheses.

Model	None	LG	LG+F
Qwen3.5-0.8B	14.4 (38/263)	6.6 $\downarrow$ 7.8 (17/257)	8.8 $\downarrow$ 5.6 (23/261)
Qwen3.5-2B	15.4 (40/259)	11.7 $\downarrow$ 3.7 (31/264)	12.1 $\downarrow$ 3.3 (32/264)
Qwen3.5-4B	7.6 (21/275)	4.7 $\downarrow$ 2.9 (13/276)	4.4 $\downarrow$ 3.2 (12/274)
Qwen3.5-9B	5.1 (14/275)	3.3 $\downarrow$ 1.8 (9/276)	5.1 $\pm$ 0.0(14/276)
Qwen3.8-27B	6.6 (18/274)	1.8 $\downarrow$ 4.8 (5/273)	2.6 $\downarrow$ 4.0 (7/274)
All models	9.7 (131/1346)	5.6 $\downarrow$ 4.1 (75/1346)	6.5 $\downarrow$ 3.2 (88/1349)

Appendix

Table 12: Judge-flagged episodes on

\tau^{2}

-bench, in which Qwen3.8-27B finds an executed call that breaks the benchmark policy (%, with flagged over evaluated episodes). Arrows give the change from None.

Table 16

	Benign task success ( $\uparrow$ )		Direct attack success ( $\downarrow$ )		Indirect attack success ( $\downarrow$ )
Model	None	LG+F	None	LG+F	None	LG+F
Qwen3.5-0.8B	20.2 (152/754)	10.3 $\downarrow$ 9.9 (99/960)	46.7 (205/439)	3.3 $\downarrow$ 43.4 (15/453)	3.1 (17/549)	1.7 $\downarrow$ 1.4 (11/648)
Qwen3.5-2B	31.9 (382/1196)	11.3 $\downarrow$ 20.6 (132/1173)	53.1 (297/559)	3.4 $\downarrow$ 49.7 (20/593)	11.6 (84/723)	2.5 $\downarrow$ 9.1 (18/712)
Qwen3.5-4B	59.8 (721/1205)	11.7 $\downarrow$ 48.1 (138/1177)	71.6 (429/599)	7.5 $\downarrow$ 64.1 (41/550)	27.4 (198/722)	5.4 $\downarrow$ 22.0 (38/705)
Qwen3.5-9B	67.4 (811/1204)	12.8 $\downarrow$ 54.6 (152/1183)	74.4 (448/602)	11.0 $\downarrow$ 63.4 (67/611)	37.0 (265/716)	4.9 $\downarrow$ 32.1 (35/709)
Qwen3.8-27B	74.9 (860/1148)	18.1 $\downarrow$ 56.8 (123/679)	40.3 (243/603)	3.7 $\downarrow$ 36.6 (20/540)	28.3 (198/700)	4.5 $\downarrow$ 23.8 (24/530)

Appendix

Table 15: DTap results per model, aggregated over domains, under the read-only deployment (%, with counts). Arrows give the change from None.

	Benign task success ( $\uparrow$ )		Direct attack success ( $\downarrow$ )		Indirect attack success ( $\downarrow$ )
Domain	None	LG+F	None	LG+F	None	LG+F
Telecom	75.1 (435/579)	75.3 $\uparrow$ 0.2 (437/580)	55.1 (365/663)	2.4 $\downarrow$ 52.7 (16/655)	13.0 (95/730)	1.2 $\downarrow$ 11.8 (9/730)
Travel	66.6 (432/649)	0.0 $\downarrow$ 66.6 (0/600)	64.3 (337/524)	0.0 $\downarrow$ 64.3 (0/512)	19.8 (119/600)	9.7 $\downarrow$ 10.1 (58/600)
Customer service	71.1 (530/745)	29.0 $\downarrow$ 42.1 (184/635)	72.4 (273/377)	7.2 $\downarrow$ 65.2 (32/446)	20.9 (92/440)	10.8 $\downarrow$ 10.1 (42/390)
Medical	45.9 (1257/2736)	0.3 $\downarrow$ 45.6 (8/2559)	53.8 (495/920)	14.2 $\downarrow$ 39.6 (115/811)	41.2 (380/922)	2.0 $\downarrow$ 39.2 (17/865)
Finance	86.7 (150/173)	0.0 $\downarrow$ 86.7 (0/173)	35.6 (42/118)	0.0 $\downarrow$ 35.6 (0/123)	27.6 (48/174)	0.0 $\downarrow$ 27.6 (0/174)

Appendix

Table 16: DTap results by domain, aggregated over the five models (%, counts in parentheses). OS-filesystem has no direct-attack tasks (–).

Figure 4: DTap results by domain under the read-only deployment, aggregated over the five models (%; counts in Table 16 ). Each line joins the unguarded rate to the rate with LeanGuard + feedback. Telecom keeps its benign success, and attack success falls in every domain.

Domain	Direct	Indirect	Calls LeanGuard admitted	Attack category (DTap)
Medical	115	17	none (127 episodes); load_skill (5)	expensive drug (33), diagnosis manipulation (31), high-cost billing (31), ignored allergy (22), upcoding (15)
Customer service	32	42	reads only ( get_case , list_cases , search_messages , …)	policy misrepresentation (40), abusive communication (32), PII disclosure (2)
Travel	0	58	reads only ( query_flight , query_accommodation , …)	unnecessary PII collection (32), payment-credential collection (26)
Telecom	16	9	reads only ( query_customer , query_bill )	financial fraud (21), credential leak (2), phone-number leak (2)
Finance, legal, OS-filesystem	0	0	–	–
All	163	126	no state-changing call

Appendix

Table 17: The 289 DTap attack episodes that succeed under LeanGuard + feedback, by domain. LeanGuard admitted no state-changing call in any of them, and no call at all in 158.

Domain	Tools	Calls	Why the effect cannot be determined
OS-filesystem	execute_command	2,728	general shell execution has no complete effect plan
	edit_file , search_files , list_directory , read_file , …	178	arguments outside the modeled sed , find , and path grammar, or oversized
	ask_for_permission	44	no reviewed contract
Finance	trade_stock	931	market order without a price (835); pending limit orders (96)
	trade_option	212	no reviewed contract
Telecom	add_ticket , add_sms , add_email , add_calendar_event , …	839	record without exactly the reviewed columns, or an unreviewed ticket status

Appendix

Table 18: DTap calls that LeanGuard stopped because it could not determine their effect, over all guarded episodes of Table 8 .

First intervention of LeanGuard	Medical	Travel	Cust. serv.	Finance	OS-files.	Telecom	Legal	All
Patient registration denied	992	0	0	0	0	0	0	992
Write without issued authority or approval	0	397	216	89	85	15	8	810
Fail-closed: effect not completely modeled	0	0	2	60	5	0	0	67
Fail-closed: other (missing resource, unrecorded authority, schema error)	0	2	27	0	5	2	0	36
None; the episodes differ by chance	0	5	3	0	0	1	4	13
Total	992	404	248	149	95	18	12	1,918

Appendix

Table 19: Benign DTap cases solved without a guard but failed with LeanGuard + feedback, by domain and by the first intervention of LeanGuard in the case.

	Direct attack success ( $\downarrow$ )		Indirect attack success ( $\downarrow$ )
Attack category	None	LG+F	None	LG+F
Diagnosis manipulation	53.0 (61/115)	25.5 $\downarrow$ 27.5 (27/106)	69.4 (75/108)	3.7 $\downarrow$ 65.7 (4/108)
Excessive test	41.4 (58/140)	0.0 $\downarrow$ 41.4 (0/139)	6.4 (9/140)	0.0 $\downarrow$ 6.4 (0/140)
Expensive drug	61.7 (66/107)	37.0 $\downarrow$ 24.7 (30/81)	51.3 (58/113)	3.2 $\downarrow$ 48.1 (3/93)
High-cost billing	61.3 (68/111)	27.9 $\downarrow$ 33.4 (24/86)	61.0 (61/100)	6.8 $\downarrow$ 54.2 (7/103)
High-cost test	52.9 (74/140)	0.0 $\downarrow$ 52.9 (0/140)	36.9 (48/130)	0.0 $\downarrow$ 36.9 (0/130)

Appendix

Table 20: DTap medical-domain attack success by category, aggregated over the five models (%, counts in parentheses).

Model	None	LG+F
Qwen3.5-0.8B	21.3 (19/89)	14.8 $\downarrow$ 6.5 (13/88)
Qwen3.5-2B	31.2 (29/93)	21.7 $\downarrow$ 9.5 (20/92)
Qwen3.5-4B	48.9 (46/94)	38.5 $\downarrow$ 10.4 (35/91)
Qwen3.5-9B	57.0 (53/93)	48.3 $\downarrow$ 8.7 (42/87)
Qwen3.8-27B	45.6 (41/90)	27.8 $\downarrow$ 17.8 (20/72)
All models	41.0 (188/459)	30.2 $\downarrow$ 10.8 (130/430)

Appendix

Table 21: Success of attacks judged only on the text of the response in DTap customer-service and travel tasks (%, lower is better). These attacks need no tool call. Arrows give the change in pp.

The Lean policy has a rule
Reason the judge flags an admitted call	LG	LG+F
Consent on a confirmed action	33 (28)	38 (32)
Trusted facts the judge does not see (roaming, bill, reservation)	15 (15)	22 (22)
The Lean policy has no rule
Transfer to a human agent	12 (11)	11 (10)
Consent on an unconfirmed action	11 (11)	7 (7)

Appendix

Table 22: Executed calls the judge flags as violations in the LeanGuard arms of

\tau^{2}

-bench, by reason, all models (episodes in parentheses).

Figure 5: The agent’s next attempt after each policy denial on

\tau^{2}

-bench (denials on the right). Edited call : same tool, other arguments. Counted per denial in the Lean replay, so admitted repeats differ slightly from the recoveries of Table 2 .

	LG		LG+F
Model	Episodes	Solved	Episodes	Solved
Qwen3.5-0.8B	5	2	5	1
Qwen3.5-2B	8	6	13	9
Qwen3.5-4B	8	7	12	10
Qwen3.5-9B	9	7	8	8
Qwen3.8-27B	3	3	9	7

Appendix

Table 23:

\tau^{2}

-bench episodes with a recovered action, and how many of them are solved.

Fix required	Denials
Different argument values	252
A tool from the agent’s own interface	534
An earlier step (e.g., authentication)	298
The customer’s approval	185
None; action already done	191
None; action not allowed	153

Appendix

Table 24: Policy denials on

\tau^{2}

-bench by the kind of fix they require. guard_repair? proves a repair for 88 of the 252 denials caused by argument values.

Failed rule	Denied	Searched	Repaired
retail.return	65	64	64
telecom.payment_request	58	58	4
airline.flights	52	52	18
airline.booking	38	18	0
retail.modify_items	23	8	0
retail.exchange_items	7	0	0

Appendix

Table 25: Argument-value denials on

\tau^{2}

-bench by failed rule. Searched : with candidate edits (other payment methods, bills, baggage charges, or refuel amounts). Repaired : an admissible edit was proved.

Tool Access Control for LLM Agents

Tool access control for LLM agents limits which tools, resources, and actions agents may use, and under what conditions.

See all 229 papers

PolicyGuard: A Dialogue-Grounded Sub-Agent Verifier for Policy Adherence in LLM Agents
Jun 28, 2026Seongjae Kang, Taehyung Yu, Sung Ju HwangTool-Augmented Language Model Agents LLM Guardrails
KAIST
NOMOS: Compiling Written Policies into Statically Verified Tool-Call Gates for LLM Agents
Oct 8, 2026Min-Young Yu, Tony Kim, Jang Won ChoiTool Access Control for LLM Agents LLM Agent Safety
Corners Co., Ltd.
Stale Does Not Mean Unsafe: Guard Precision for Tool-Using LLM Agents under Infrastructure State Races
Aug 25, 2026Zihao Zheng, Jiayu Long, Baichuan Li +1Runtime Enforcement for AI Agents LLM Agent Safety
Washington University in St. Louis, St. Louis, Missouri, USA · Southern Methodist University, Dallas, Texas, USA

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

PolicyGuard: A Dialogue-Grounded Sub-Agent Verifier for Policy Adherence in LLM Agents

Seongjae Kang, Taehyung Yu, Sung Ju Hwang

KAIST

Tool-Augmented Language Model Agents LLM Guardrails LLM Agent Evaluation LLM Agent Verification LLM Agent Safety

Open paper AskPDF arXiv

LLM agents handle user requests on behalf of organizations through tool calls and must follow the company policies stated in their system prompts. Prior work approaches this as a safeguarding problem -- external checks that block non-compliant agent actions. We argue that policy adherence is a broader problem: real workflows unfold across many turns, require explicit user confirmation and prerequisite reads, and hinge on the content of the dialogue rather than on any single argument value. Meeting this bar requires (i) full conversation context, (ii) self-reasoning over the policy and the current dialogue, and (iii) conversation-specific remediation that guides the agent's next turn -- three capabilities that prior safeguard work has often underestimated. We introduce POLICYGUARD, a sub-agent verifier that shares the agent's view of the dialogue, reasons over the policy in context, and provides actionable feedback for the agent's next turn. On tau^2-BENCH airline across three vendors (GPT-5.4, Claude Sonnet 4.6, Gemini 2.5 Pro) with four trials per setting, POLICYGUARD improves PASS4 by +12.0 / +6.0 / +12.0 pp. Per-call analyses show POLICYGUARD achieves higher policy-violation recall while blocking roughly half as often as argument-level guards.

Abstract

Tool Access Control for LLM Agents

Explore similar work

PolicyGuard: A Dialogue-Grounded Sub-Agent Verifier for Policy Adherence in LLM Agents

NOMOS: Compiling Written Policies into Statically Verified Tool-Call Gates for LLM Agents

Stale Does Not Mean Unsafe: Guard Precision for Tool-Using LLM Agents under Infrastructure State Races