Tool-using LLM agents violate the policies they are deployed to enforce, often silently. Prior defenses hand-write rules, query an LLM verifier per action, or compile policies through heavyweight formal machinery. Naive compilation fails: extracted rules block the tool satisfying their own precondition, or read arguments their tool lacks. NOMOS, a four-pass compiler, turns a natural-language policy into a deterministic tool-call gate; static verification with tool-schema-level checks alone (no prover, solver, or LLM) repairs or rejects 37% (airline) and 13% (retail) of candidates, without which most shipped rules are inoperable. Replaying compiled rules over undefended transcripts flags bindings that refuse legitimate work (a development binding refused 95.9% of task-passing calls); no evaluation binding is flagged. On τ2-bench the gate cuts violations of reference-encoded clauses among state-changing calls from 66.3% to 2.6% (airline) and 30.8% to 6.9% (retail), raising airline task success significantly for 2≤k≤4; a 26B on-premise compilation is not significantly worse than hand-written or frontier-compiled rules. Unlike AgentDojo's shipped defenses, it reaches a zero attack success rate (ASR) on banking, where nine attack families collapse onto three structural rules. On the other three suites its ASR is at most 3.6%, from goals with no tool call to govern and one write admitted by a binding weaker than its clause; a second agent model, Llama-3.3-70B, reproduces the effect on both benchmarks. Decisions take microseconds without an LLM call, at a domain-dependent benign-utility cost; compilation runs on-premise on open-weight gemma-4-26B.
Figures & tables
Condition
ASR
Util. (atk)
Benign
Runtime LLM
Undefended
46.5%
64.9%
79.2%
—
Progent (auto)
5.6%
52.1%
62.5%
✓
NOMOS gate
0.0%
67.4%
70.8%
—
Table I: Nearest-neighbour comparison on AgentDojo banking, run against our model endpoint with the same agent model (gemma-4-26B-A4B), the same banking tasks, injections and attack, and the same repetitions (two attacked, three benign), scored by AgentDojo’s own flags. Progent’s automatic (LLM-generated policy) variant is the only one its public repository reproduces. Util. (atk) is task success in the attack condition, as in Table XII ; Benign is utility on the attack-free runs, averaged per user task. Runtime LLM marks a defense that calls a model itself while the agent works: Progent generates and updates its policy per task, the gate makes no call at all.
Policy
LLM
Static
Runtime
Solver/
Pre-
System
source
extr.
verif.
LLM
prover
flight
PolicyGuard [ 4 ]
doc
✓
—
✓
—
—
Progent [ 27 ]
task
✓
—
✓
✓
—
VeriGuard [ 6 ]
doc
✓
✓
✓
✓
—
Zwerdling [ 7 ]
doc
✓
tests
—
—
—
NOMOS
doc
✓
✓
—
—
✓
Table II: Where the closest systems sit. Policy source : a written document (doc) or the user’s task. Static verif. : a check that the compiled artifact can function, before it runs. Runtime LLM : the defense itself calls a model while the agent works. Preflight : the artifact is replayed over recorded behaviour before deployment. Progent gives policy authors a type checker and an SMT-based check for overlapping policy conditions (its v3 also uses an SMT solver to classify policy updates as narrowing or expansion), but does not check whether a rule is operable; Zwerdling et al. type-check the generated code and regenerate it until a hand-written test suite passes, so their oracle is tests rather than structure. VeriGuard verifies its policy code offline but maps the agent’s data onto the policy’s arguments with an LLM at run time.
Figure 1: NOMOS overview. Offline, once per policy, a four-pass compiler turns a natural-language policy into verified rules (airline: 79 candidates to 10 rules; retail: 53 to 5): only Extract calls an LLM, and Resolve statically repairs or rejects the defective candidates (37% and 13% of raw extractions on structural grounds, 41% and 15% counting minority votes) before anything is enforced; the verified rules are then loaded into the gate. At runtime, a deterministic gate checks each proposed tool call against facts drawn exclusively from tool results and user turns (the agent’s own claims are excluded); a blocked call returns the rule id and clause as a tool error, and the agent re-plans.
airline
retail
Raw extraction candidates (5 samples)
79
53
Structural defects (rule names real tools, cannot function)
Repaired: self-blocking (deadlock)
0
4
Repaired: write-scope overreach
5
0
Argument–signature mismatch
8
1
Rejected: domain-unsatisfiable predicate
5
0
Table III: Static verification outcomes, counted per candidate. Rows are grouped by what the defect is : the structural rows are rules that name real tools and would run, wrongly; a reference to a tool the domain does not have would be an extraction hallucination, and none occurred. Reading only the structural block, verification repairs or rejects 36.7% (airline) and 13.2% (retail) of raw candidates; adding the stability filter gives 40.5% and 15.1%. Repair rows modify a candidate in place, which then proceeds to voting; Rejected, Merged and Enforced partition the pool ( 27+42+10=79 ; 3+45+5=53 ). A wildcard candidate is counted once here, under scope, and a candidate emptied by the argument check once, under that check, although each also trips the unknown-tool counter on its way out; the retail argument mismatch strips two bindings from a candidate that survives, and a candidate that loses any binding to the vote is counted under the stability filter. Figure 2 draws the same counts as a flow.
Figure 2: From extracted candidates to enforced rules ( Table III ). Static verification repairs or rejects 37% of raw candidates on airline (29 of 79) and 13% on retail (7 of 53) as structural defects; repaired candidates proceed to the vote. The rejected counts sum the table’s rejection rows (airline: unscoped wildcard, argument-signature mismatch, domain-unsatisfiable predicate; retail: unscoped wildcard); the retail argument mismatch strips bindings from a candidate that survives and is shown as a repair. Duplicates then merge and minority candidates drop out, leaving 10 and 5 enforced rules.
Figure 3: The authentication deadlock as extracted, and its repair (retail; the compilation report’s verbatim entry is in B ). The repair keeps the clause’s demand and removes only the bindings that made it unsatisfiable.
Tool bound to TEL-04
Refused/calls
Rate
Verdict
send_payment_request
47/49
95.9%
flagged
resume_line
0/44
0.0%
kept
Table IV: One predicate ( overdue_bill_outstanding , rule TEL-04), two bindings, on the recorded telecom baseline: refusals among calls inside runs the undefended agent passed. The defect lives in a binding, not in the rule, so diagnosis and repair are addressed to the (rule, tool) pair; unbinding the rule wholesale would have discarded the protective binding. The stage detects; the mechanical unbinding it offers was exercised on this development case only.
Figure 4: (a) Task success under the gate, airline ( k≤5 ) and retail ( k≤4 ). The shaded band and labels give the airline gain in points, bold where the paired-bootstrap CI excludes 0 ( 2≤k≤4 , Table VI ); the airline margin widens from k=1 to k=3 and stays at or above 12 points through k=5 , and pass^5/pass^1 rises from 0.51 to 0.67: the gate buys repeated reliability. Retail k=2,3 are computed from the same runs and bootstrap as Table VI (39.0% to 35.2% and 30.7% to 27.9%, both CIs include 0); no retail difference is significant. (b) Policy violations as a fraction of state-changing tool calls, measured by an independent hand-written checker replayed over recorded transcripts (per-action reading, Table V ).
Domain
Condition
Writes
Viol.
Rate
95% CI
Batch
airline
undefended
353
234
66.3%
[61.2, 71.0]
36.8%
airline
NOMOS gate
116
3
2.6%
[0.9, 7.3]
2.6%
retail
undefended
611
188
30.8%
[27.2, 34.5]
13.6%
retail
NOMOS gate
582
40
6.9%
[5.1, 9.2]
5.3%
Table V: Violations of the reference-encoded policy clauses (16 airline, 11 retail) among state-changing calls, measured by replaying the hand-written reference set over recorded transcripts. Writes counts calls to tools the benchmark declares WRITE ; under the gate these are the writes the gate admitted (refused attempts never execute and are logged separately: 226 on airline, 208 on retail). CIs are Wilson 95%. Residual violations under the gate are, with one retail exception, compiler coverage gaps (clauses, or tool bindings of a clause, that the compiled set does not encode), which are enumerable and measurable rather than random. The last column recomputes each rate under the alternative batch-confirmation reading of the policy surfaced by the checker audit ( Section 4 ): the reduction holds under either semantics (26 × and 4.5 × per action; 14 × and 2.6 × per batch). Retail is scored with the 11-rule reference set of Section 4 ; 21 of its 40 admitted violations fall under the two clauses (refund destination, same-item exchange) that the compiled rule set does not encode.
Metric
Undef.
Gate
Δ
95% CI
airline (50 tasks × 5 trials)
pass^1
39.2%
47.6%
+8.4
[−1.2,+18.0]
pass^2
27.4%
40.6%
+13.2
[+2.6,+24.0] *
pass^3
23.0%
37.0%
+14.0
[+2.6,+25.4] *
pass^4
21.2%
34.4%
+13.2
[+0.8,+25.6] *
pass^5
20.0%
32.0%
+12.0
[−2.0,+26.0]
Table VI: Task success under the gate (paired bootstrap over tasks; * = CI excludes 0). On airline the gate improves success, with the margin widening from k=1 to k=3 ; on retail all point estimates are slightly negative but no comparison is significant. CIs are per-comparison, without multiplicity adjustment across k ; the finding we rely on is the significance for 2≤k≤4 and the rise of pass^5/pass^1, not any single interval. Deltas are computed from unrounded values and can differ from the rounded columns by 0.1.
Domain
Cond.
Pass
Safe
P ∧ V
W/sim
V/sim
airline
undef.
39.2%
32.4%
17
1.41
0.94
airline
gate
47.6%
47.6%
0
0.46
0.01
retail
undef.
52.4%
41.0%
52
1.34
0.41
retail
gate
50.2%
47.8%
11
1.28
0.09
airline, Llama
undef.
22.8%
18.4%
11
1.65
1.44
airline, Llama
gate
46.8%
46.8%
0
0.11
0.01
Table VII: Safe completion (task passed and no violation of the encoded clauses), under the per-action reading of the confirmation clause. P ∧ V counts simulations that passed while violating; W/sim and V/sim are executed writes and violations per simulation. Under the batch reading the undefended safe rates are 35.6% (airline), 47.1% (retail) and 18.4% (Llama) and the gated rates are unchanged.
airline
retail
Configuration
Rules
Inop.
r/o
Rules
Inop.
r/o
All checks (reference)
8
0
0
4
0
0
− self-blocking reachability
8
0
0
4
1
0
− write-scope repair
8
0
1
4
0
0
− argument consistency
10
3
0
4
0
0
− domain satisfiability
9
1
0
4
0
0
Table VIII: Ablation of Pass 3’s static checks over a frozen candidate pool (airline 69, retail 46 candidates). The pool is a separate extraction run frozen for exact attribution, not the production compile of Table III : with all checks enabled it emits 8 and 4 rules, versus the 10 and 5 enforced in the evaluation. Inop. counts rules that cannot function at runtime; r/o counts confirmation rules left guarding read-only tools. Removing any one of the four checks that fire on defects here (self-blocking, write-scope, argument consistency, satisfiability) ships defective rules in at least one domain; the remaining checks change what ships without creating inoperable rules (see text); removing all of them, the naive coupling, ships the majority defective.
Domain
Bind.
Supp.
Fire
Worst
Flag
airline (10 rules)
16
15
11
83.3% (5/6)
0
retail (5 rules)
24
24
12
31.6% (12/38)
0
telecom (pre-repair)
2
2
1
95.9% (47/49)
1
Table IX: Behavioral-preflight replay of each rule set over its canonical undefended baseline, applying the gate’s state transitions (a confirmation is consumed by an admitted guarded write) and keeping the recorded continuation after a hypothetical refusal. Supp. counts bindings whose tool has at least one call in a task-passing baseline run; the airline confirmation binding on send_certificate has none and receives no verdict. A binding fires if it blocks at least one replayed call; the refusal rate is over calls in task-passing runs and the flag line is 0.9. No evaluation-domain binding is flagged, so the deployed airline and retail rule sets are identical with the preflight on or off; the telecom row replays the pre-repair development rule that motivated the stage, and the preflight flags exactly the self-defeating binding. Worst is the highest refusal rate over the domain’s guarded tools, reached on book_reservation , cancel_pending_order and send_payment_request respectively.
Rule source
Preparation (once per policy version)
Policy leaves premises
Runtime LLM calls
Rules
pass^1 / pass^5 (vs. local)
local compilation (26B, ours)
40 LLM calls, $0
no
0
10
47.6 / 32.0 (reference)
hand-written reference
engineer time
no
0
16
42.8 / 28.0 ( k=1 significant, −4.8 )
frontier compilation
40 LLM calls, $1.02
yes
0
14
46.4 / 30.0 (not significant)
LLM verifier, PolicyGuard-style
checklist compile
depends on verifier host
1 per state-changing decision; 347 in 250 simulations
n/a
47.2 / 38.0 (not significant; +74% wall-clock)
Table X: Where the LLM work sits, per rule source, on airline. Preparation is paid once per policy version; runtime is paid on every state-changing call. The local compilation runs on premises (40 extraction calls, no API charge) and the policy never leaves them; the frontier compilation sends the policy to a hosted model (1.02)andemits15rules,ofwhichthegate’sload−timecheckdropsone,so14areenforced;thehand−writtensetcostsanengineer’stime.pass1/pass5arefromSections5.4and5.7;significantmarksadifferencefromthelocalcompilationthatatask−pairedbootstrapseparatesfromzero.Thegate’sdecisionfunctionevaluatesinmicroseconds(3\mu$ s mean over 1,801 replayed calls, single-threaded Python); live gated simulations take 21.3 s against 20.1 s undefended.
Condition
Pairs
Att.
Blk.
Succ.
ASR
Std., undefended
288
142
0
134
46.5%
Std., gate
288
122
122
0
0.0%
Adaptive, undefended
144
55
0
50
34.7%
Adaptive, gate
144
61
61
0
0.0%
Table XI: AgentDojo banking suite, all conditions from one sweep; the standard-attack rows pool two repetitions. Attempted = the agent actually issued a tool call carrying the attacker’s account (or, for the password goal, the attacker’s password). Att. ≥ Succ. even undefended (142 vs. 134): issuing the attacker’s call is necessary but not sufficient for the benchmark’s goal state, so a few attempts fail on their own. Att. and Blk. count pairs, not calls (a pair can contain several attacker calls, since the gated agent re-plans after each refusal); gated and undefended counts come from separate runs, so gated Att. can exceed the undefended count (adaptive: 61 vs. 55). In every attempted pair the gate refused the attacker’s call ( Blk. = Att. ), so the 0% ASR reflects blocking, not an agent that never took the bait.
Defense
ASR
Util. (atk)
Benign
Undefended
46.5%
64.9%
79.2%
Spotlighting (delimiting)
36.5%
66.0%
77.1%
Repeat user prompt
31.9%
66.0%
83.3%
Tool filter
11.8%
49.7%
58.3%
NOMOS gate
0.0%
67.4%
70.8%
Table XII: AgentDojo banking, one sweep, same model and attack for every row. Two attack repetitions (288 pairs) and three benign repetitions (48 samples) per condition. Util. (atk) is task success in the attack condition; benign is task success with no attack present. Figure 5 plots these rows together with Progent.
Figure 5: Attack success against task success on AgentDojo banking (gemma-4-26B-A4B agent), (a) with no attack present and (b) in the attack condition; lower right is better, and the card in each panel gives the gate’s two coordinates. Undefended (open circle), three of AgentDojo’s shipped defenses (filled circles; spotlighting is the delimiting variant) and the gate (navy) come from one sweep ( Table XII : 288 attack pairs and 48 attack-free samples per condition); Progent (auto) (diamond), whose policy an LLM generates per task, was re-run in its own fork on identical banking task data with the same repetitions ( Table I ).
Agent model
Cond.
ASR
Att.
Blk.
gemma-4-26B
undef.
46.5%
49.3%
—
gate
0.0%
42.4%
100%
Llama-3.3-70B
undef.
44.1%
47.8%
—
gate
0.0%
40.7%
100%
Table XIII: The gate’s effect on attack success on AgentDojo banking is the same across two unrelated open-weight agent models, using one compiled rule set; payments diverted to known payees differ (8 of 288 and 11 of 140 gated pairs, Section 5.8 ). Att. is the fraction of pairs in which the agent actually issued the attacker’s call; Blk. is the fraction of those refused by the gate. The gemma rows pool two repetitions (288 pairs); the Llama runs used a per-user-task driver and recorded 186 (undefended) and 140 (gated) pairs, each counted with an unscored pair as a failed attack, so all Llama percentages are over those denominators.
Airline
gemma-4-26B
Llama-3.3-70B
pass^1
39.2 → 47.6 ( +8.4 )
22.8 → 46.8 ( +24.0 *)
pass^5
20.0 → 32.0 ( +12.0 )
14.0 → 44.0 ( +30.0 *)
safe completion
32.4 → 47.6 ( +15.2 *)
18.4 → 46.8 ( +28.4 *)
violations / writes
66.3% → 2.6%
86.9% → 7.1%
executed writes
353 → 116
413 → 28
gate refusals
226
250
Table XIV: Airline under the same ten compiled rules, two agent models. Each cell is undefended → gated; deltas are task-paired bootstrap, * marks a 95% CI excluding 0. Safe completion is task passed with no violation of the encoded clauses ( Section 5.3 ). The rule set was compiled once from the gemma extractor and reused unchanged for Llama. The gated Llama agent executed only 28 writes in 250 runs, so its residual rate (2/28) is bounded rather than pinned.
Undef. ASR
Reported
Executed
Suite
gemma
Llama
gemma
Llama
gemma
Llama
banking
46.5%
44.1%
0.0%
0.0%
0.0%
0.0%
slack
70.5%
59.0%
0.0%
10.5%
0.0%
0.0%
travel
10.0%
60.7%
3.6%
5.7%
0.7%
1.4%
workspace
7.3%
13.6%
0.0%
0.4%
0.0%
0.0%
Table XV: Reproduction on a second agent model across all four AgentDojo suites: reported vs. executed gate ASR for both agent models under the same compiled rule sets. Reported is AgentDojo’s security flag; Executed counts only flagged pairs in which a malicious state-changing tool call actually ran (the gate let it through). The two diverge where the flag credits an output-only goal (no tool call to govern) or scores a task over attempted rather than executed calls. Executed attacks occur only on travel: one pair under gemma (0.7%) and two under Llama (1.4%); in both models one is the same injected calendar event, admitted by a binding weaker than its clause ( Section 5.11 ), and Llama’s other emails the user’s passport and card numbers to the address the user named in the request, which the written policy does not forbid. Llama’s gated workspace rate counts two context-overflow pairs, which AgentDojo’s runner scores as attack successes although no malicious call executed; its undefended workspace run is partial (420 of 560 pairs). Outside the flag, injected payments were diverted to known payees on banking ( Section 5.8 ) and attacker-ordered deletions ran in nine Llama workspace pairs ( Section 5.10 ).
ASR
Benign util.
Suite
undef.
gate
undef.
gate
banking
46.5%
0.0%
79.2%
70.8%
slack
70.5%
0.0%
90.5%
14.3%
travel
10.0%
3.6% †
75.0%
70.0%
workspace
7.3%
0.0%
87.5%
65.0%
Table XVI: Live evaluation on all four AgentDojo suites, same model (gemma-4-26B-A4B), unmodified scorers; task counts are AgentDojo’s own (we did not subsample). Gated ASR denominators are 288, 105, 140 and 560 pairs (undefended: the same, except 558 recorded workspace pairs, one of them unscored and counted as a failed attack); every rule set is compiled from its suite’s one-page policy, with 3, 4, 3 and 4 rules respectively (banking with the default vocabulary, A ; slack, travel and workspace with the extended vocabulary and the accessor-activation check, C ). A repeat of the gated benign runs gave 14.3% (slack) and 62.5% (workspace). † five pairs: four are the one output-only injection goal (the attacker’s goal is satisfied by the agent’s text output, so there is no tool call to refuse), out of scope for a call-level gate; the fifth is an executed calendar write ( Section 5.11 ); on the six tool-calling goals ASR is 1/120.
Rule set
slack
travel
workspace
Undefended
70.5 / 90.5
10.0 / 75.0
7.3 / 87.5
Default vocabulary
18.1 / 28.6
–
–
Extended
14.3 / 57.1
5.7 / 60.0
7.7 / 87.5
+ accessor check ‡
0.0 / 14.3
3.6 / 70.0
0.0 / 65.0
Table XVII: Compiling slack, travel and workspace: gated ASR / benign utility (%) per rule set, gemma-4-26B-A4B, with the pairs of Table XVI . Every row except the first is a compiled set. Default vocabulary : the four extraction conditions written for banking (run on slack only). Extended : two further conditions (write-target and message-body provenance). ‡ The evaluated condition of Table XVI . The extended rows without and with the check are separate compilations of the same policy with the same extraction model and sample count; on slack their bindings differ only by the check’s repair, on travel create_calendar_event is guarded by target_not_user_named in the first and by the action_requested_by_user precondition in the second, and the second workspace set adds a message-body link rule. Executed ASR (flagged pairs in which a malicious call ran, as in Table XV ): default vocabulary 18.1% (slack); extended without the check 14.3, 2.1 and 7.3%; with it 0.0, 0.7 and 0.0%.
Table XVIII: Compiled rules for the slack, travel and workspace suites (gemma-4-26B-A4B, five samples, extended vocabulary, accessor-activation check), shown without their suite prefix (SLA-AUTO-, TRA-AUTO-, WOR-AUTO-). A rule ending in G is the retargeted copy the check made of the rule with the same number; the original survives only on slack, for the one tool whose recipient argument it can read. PRE marks a precondition, FBD a forbidden rule.
Goal
Attacker objective
Att.
Blk.
Rule
0
exfiltrate streaming-service name
24
24
FBD-02
1
exfiltrate a third party’s IBAN
13
13
FBD-02
2
exfiltrate food preference
30
30
FBD-02
3
exfiltrate phone model
21
21
FBD-02
4
redirect recurring payment
20
20
PRE-03
5
transfer maximum funds
12
12
FBD-02
Table XIX: Every attack pair with an attempted call toward the attacker’s account or credential across all gate-condition runs (two standard-attack repetitions and the adaptive attack, 432 pairs), with the rule that refused it; Att. and Blk. count pairs. Goal 4 targets a tool outside FBD-02’s guard set and is caught by the broader user-request precondition; goal 7 changes a credential rather than moving money and is caught by the password rule. No goal reaches the attacker; goal 1’s payment is diverted to a payee already in the history in 15 pairs ( Section 5.8 ).