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

Security policies for tool-using agents are increasingly written in natural language and compiled by a language model into executable rules that a deterministic gate enforces at every tool call. We ask a question this pattern has not faced: is the compiled enforcement invariant to the model that compiled it? We compile seven policies from two agent benchmarks with six frontier and open-weight models through one fixed compiler and measure divergence at two levels: the rule text (intensional) and the decisions the rules make on 17,000 recorded tool calls (extensional). The two levels come apart. On three policies the compiled rule sets differ in text (pairwise Jaccard 0.65) yet decide 97–99% of recorded calls identically; on three others the same textual divergence splits 18–29% of calls. Deployed on the same benchmark with the same executing model, the choice of compiling model alone moves the attack success rate from 0% to 54% and benign task completion from 0% to 33%. Repeated compiles are deterministic for the frontier models (Jaccard 1.0), so the divergence is systematic disagreement, not sampling noise. We give a formalization that explains the split: extensional divergence is bounded by the activation mass of the bindings on which models disagree, and vanishes exactly when the compiler’s closed predicate vocabulary can express the policy on the deployed call distribution. The mechanism is testable by intervention: extending the vocabulary with two predicates collapses cross-model disagreement on the divergent policies. The practical conclusion is that invariance is a property of the vocabulary and verification layer, not of the model, and that a compiled policy should be tested for model invariance before it is trusted.