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

arXiv:2610.11030 · cs.CR, cs.AI, cs.LG · Submitted 2026-10-08 · Read on arXiv

Listen

Radio episode about this paper

Transcript

Introduction to the show: ident: Security Radio. Generated commentary on the latest security and cryptography papers.

Nadia: I'm Nadia, and with me are Elias and Priya, guest researcher.

Elias: Today's paper: "NOMOS: Compiling Written Policies into Statically Verified Tool-Call Gates for LLM Agents".

Nadia: Detailed Summary of NOMOS: Compiling Written Policies into Statically Verified Tool-Call Gates for LLM Agents The research presented in the paper "NOMOS:

Elias: First, who's behind it and why it matters.

Paper summary: Elias: So wrapping up this discussion on NOMOS, the authors are essentially pushing for this idea of coupling LLM-driven policy generation with deterministic enforcement through heavyweight formal machinery >

Nadia: They’re arguing that the safety benefit from that verification mechanism is strong enough to hold up even when tested against a second agent model >

Priya: It suggests a general principle: whenever an LLM writes artifacts that a deterministic system will execute, the missing component is this static verifier standing between them >

Elias: So, if you think about how this works in the real world, it’s not just about making the AI behave better on a benchmark; it’s about ensuring that critical tool executions stay within defined boundaries >

Nadia: They are showing that this isn't some abstract theory; they've shown concrete reductions in violations, from sixty-six point three percent down to two point six percent >

Priya: The paper lays out the title NOMOS: Compiling Written Policies into Statically Verified Tool-Call Gates for LLM Agents as a way to formalize this necessity >

Elias: It’s about turning natural language policies into gates that are mechanically checked, so you don't rely solely on the LLM's ability to write something correct >

Conclusion: Nadia: So we’ve gone through how NOMOS actually builds these gates, but now we need to talk about what this whole project really means for our work here on agent safety and control >

Elias: Yeah, looking at the title itself, "NOMOS," it sounds pretty serious, like a system of laws or rules being applied mechanically >

Priya: It’s about taking policies that an LLM writes in plain English and turning them into something that a computer can check rigorously before it ever runs anything >

Nadia: Exactly. The authors are showing how you don't just trust the LLM to write something safe; you need a formal way to verify those rules >

Elias: They’re proposing this four-pass compiler where the static verification step is the core idea, not just a nice add-on >

Priya: The big implication for us is that we don't have to rely on just scaling up the LLM's ability to write good rules anymore >

Nadia: It’s about making sure that even if the LLM hallucinates something dangerous, the verification layer catches it before it becomes an execution problem >

Elias: I think what’s really interesting is how they frame this as a necessary component for safety, not just a convenience >

Priya: They did show that this static check actually makes the system much more robust against those kinds of errors we see in testing >

Nadia: It moves the problem from being purely about LLM instruction following to being about ensuring deterministic execution at the gate level >

Elias: And if you look at their results, it shows that this structural verification really helps cut down on violations when dealing with state-changing calls >

Priya: I mean, they saw a big drop in errors on those airline policies and retail ones when they used this method compared to just letting the LLM do it >

Nadia: It’s not just about getting better scores on benchmarks; it's about building a system where the cost of being wrong is much lower than what we see now >

Elias: So, while this is a specific technique for policy compilation, the underlying idea seems to be that any LLM artifact going into a deterministic execution engine needs this formal check >

Priya: It suggests that for critical agent tasks, the verification layer isn't optional; it’s a structural requirement for reliability >

Min-Young Yu, Tony Kim, Jang Won Choi

Corners Co., Ltd.

cs.CR, cs.AI, cs.LG

Submitted: 2026-10-08

Updated: 2026-10-08

Key concepts

Four-Pass Compiler
NOMOS uses four sequential stages: PARSE, EXTRACT (LLM), RESOLVE (static verification), and MATERIALIZE. This structured approach ensures that the natural language policy is systematically converted into a final, executable rule set, moving from unstructured text to verified code.
Static Verification Pass
This crucial intermediate step mechanically checks every candidate rule generated by the LLM extraction against strict criteria like self-blocking reachability and argument consistency. It acts as a safety filter to catch errors that pure LLM generation might miss, ensuring operational correctness before execution.
Tool-Call Gate
The final output is a deterministic gate that dictates exactly when an agent can call a specific tool based on verified conditions. This ensures the enforcement mechanism is predictable and operates at high speed without needing further LLM calls during runtime.
Domain-Dependent Cost
The cost associated with NOMOS operation varies by task complexity and domain. While simple tasks have low costs, complex ones like slack management incur higher costs. This suggests that the operational benefit of the system is tied to the specific nature of the work being performed.

Terminology

Summary

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

The research presented in the paper NOMOS: Compiling Written Policies into Statically Verified Tool-Call Gates for LLM Agents introduces NOMOS, a novel four-pass compiler designed to transform natural-language policies into deterministic, statically verified tool-call gates suitable for use with Large Language Model (LLM) agents. The core innovation of NOMOS lies in the critical insertion of a rigorous static verification layer between the initial policy extraction and final enforcement, demonstrating that relying solely on LLM extraction is insufficient for safety and operational correctness.

System Architecture: The Four-Pass Compiler

NOMOS operates as a comprehensive compiler with four distinct passes:

  1. PARSE: The initial stage where the natural-language policy is parsed into a structured format.

  2. EXTRACT (The LLM Pass): This is the sole pass involving an LLM, responsible for extracting operational schemas from the natural language policy.

  3. RESOLVE (Static Verification Pass): This crucial intermediate step mechanically checks every candidate rule generated during extraction against a suite of rigorous static verification criteria. These checks include:

  • Self-blocking reachability analysis.

  • Argument–signature consistency verification.

  • Domain satisfiability testing.

  • State contradiction detection.

  • Write-scope correctness checking.

  1. MATERIALIZE: The final pass where the verified rules are materialized into the operational tool-call gate, ready for execution by the agent system at microsecond speeds without requiring further LLM calls during runtime enforcement.

Core Contributions and Safety Mechanisms

The primary contribution of NOMOS is proving that static verification is not merely a substitute for extraction scale; it is a necessary component for safety. The paper demonstrates that coupling LLM-compiled rules directly with deterministic enforcement without this static verification layer introduces significant risk.

Key findings related to its efficacy and safety include:

  • Error Reduction: Static verification significantly improves policy compliance. On the tau squared-bench (a benchmark involving state-changing calls), the compiled gate achieved a dramatic reduction in violations, cutting them from 66.3% down to 2.6% for airline policies and from 30.8% to 6.9% for retail policies—representing a 26-fold and 4.5-fold reduction, respectively.

  • Robustness Against Attacks: The system exhibits exceptional security properties, achieving a zero attack success rate (ASR) on banking by collapsing potential injection attacks onto just three structural rules within the gate.

  • Determinism and Provenance: The gate is inherently deterministic because it reads facts strictly from tool results and user turns (explicitly excluding the agent's own claims). This structural provenance rule makes the system robust against injected instructions that assert false context (e.g., the user has approved this transfer), as assertions are not treated as established facts.

  • Performance: The gate operates at microsecond latency without incurring an LLM call cost, resulting in a domain-dependent benign-utility cost. This cost is quantified: it is relatively low (5.0 points on travel and 8.3 on banking) for simpler tasks but becomes significant (76 points on slack/complex tasks).

Conclusion and Theoretical Implications

The final conclusion drawn by the authors is profound: the safety effect of the gate's verification mechanism reproduces even when tested against a second agent model. Furthermore, they characterize the nature of this cost as being domain-dependent, suggesting that legitimate operational work often targets information discovered by the agent through reading (interpreting facts) rather than solely relying on explicit user naming.

The authors extend these findings beyond simple policies, positing a broader principle: whenever an LLM writes artifacts that a deterministic system will execute, the missing component is a static verifier standing between them. In essence, NOMOS establishes the necessity of this verification layer to ensure that the flexibility of LLM-driven policy generation does not compromise the determinism and safety required for critical tool execution.

Improvements for AI systems

  1. Improved policy compilation through NOMOS: "NOMOS, a fourpass 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. This allows for mechanical repair of structural defects by checking self-blocking reachability, argument–signature consistency, domain satisfiability," ensuring that rules are not only syntactically valid but also functionally operable.

  2. Implementation of a zero-LLM behavioral preflight: NOMOS therefore adds a pre-deployment behavioral preflight: replaying compiled rules over the recorded transcripts of the undefended agent, with no synthesized test suite. This mechanism catches rules that are structurally sound but behaviorally wrong, specifically identifying self-defeating bindings which would otherwise be shipped and causing issues in real-world deployment.

  3. Deterministic runtime gate for decision making: The system replaces LLM verification with a deterministic check: The gate is deterministic and reads facts from tool results and user turns (the agent’s own claims are excluded); a blocked call returns a tool-level error naming the rule and its clause, so the agent can re-plan. This ensures decisions are made at microseconds without an LLM call, maintaining high speed while enforcing policy constraints.

  4. Characterization of defect classes: The system provides measured insights into failure modes: we identify and characterize the defect classes that make naively coupling LLM-compiled rules to deterministic enforcement unsafe, with measured frequencies from real compilations. This allows developers to understand which defects the machinery is protecting against, how often they occur, enabling targeted policy hardening.

  5. Domain-dependent cost analysis: The system quantifies overhead precisely: The benign-utility cost is domain-dependent, from point estimates of 5.0 points on travel (where the compiled calendar binding is weaker than its clause) and 8.3 on banking. This provides a nuanced understanding of the trade-off, showing that enforcement cost is cheap where user intent names the write target and expensive where the assistant’s job is to act on what it reads.

Sources

Related papers