Symbolic Temporal Supervision of LLM Agents Using Contracts

# Symbolic Temporal Supervision of LLM Agents Using Contracts
Source: [https://arxiv.org/html/2609.18128](https://arxiv.org/html/2609.18128)
###### Abstract

Large language model \(LLM\) agents augmented by tools can automate complex, multi\-step tasks, such as web navigation, code generation, and workflow orchestration, by acting on external systems through tool calls\. However, hallucinations, distributional instability, and adversarial manipulations in LLMs, and the irreversible consequences of certain tool calls can lead to harmful outcomes\. Existing safeguards either grade recorded trajectories post hoc with stochastic LLM judges or block unsafe actions one call at a time, and no single deterministic artifact supports both roles\. We present𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}, a contract\-based framework for symbolic temporal supervision of LLM agents\.𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}captures an agent’s behavior as a sequence of tool calls and formalizes it as a trace over a fixed set of checkable predicates\. It then specifies required behaviors using assume\-guarantee contracts in linear temporal logic over finite traces \(LTLf\)\. Each contract is compiled to a deterministic finite automaton \(DFA\) that serves two roles: gating agent actions online and evaluating recorded traces offline\. A contract library, acting as a reusable knowledge base, is maintained independently of the agent’s model and can be applied across different agents within the same task domain\. We show the effectiveness of our approach on four benchmarks spanning both roles, where𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}matches state\-of\-the\-art LLM\-judge and rule\-based guardrail baselines while producing deterministic, reproducible verdicts and, in the online mode, orders\-of\-magnitude lower per\-call latency\.

1Department of Electrical Engineering and Computer Sciences, University of California, Berkeley, CA, USA

\{yifeng\_xiao, pierluigi\.nuzzo\}@berkeley\.edu

## 1Introduction

Recent tool\-augmentedlarge language model \(LLM\)agents can automate complex, multi\-step tasks in real\-world domains, including web navigation\([Zhou et al\. 2024](https://arxiv.org/html/2609.18128#bib.bib56)\), code generation\([Jimenez et al\. 2024](https://arxiv.org/html/2609.18128#bib.bib23)\), and workflow orchestration\([Wu et al\. 2024](https://arxiv.org/html/2609.18128#bib.bib46)\)\. Agentic frameworks such as OpenClaw\([OpenClaw Project 2026](https://arxiv.org/html/2609.18128#bib.bib33)\), HermesAgent\([Nous Research 2026](https://arxiv.org/html/2609.18128#bib.bib30)\), and LangChain\([Chase 2022](https://arxiv.org/html/2609.18128#bib.bib10)\)achieve these capabilities through tool\-call interfaces, ranging from shell commands toapplication programming interface \(API\)calls and protocols such as theModel Context Protocol \(MCP\)\([Anthropic 2024](https://arxiv.org/html/2609.18128#bib.bib2)\)\. These interfaces let agents act on external systems, but they also introduce safety risks: the hallucinations and distributional instability ofLLMs combined with possible adversarial manipulations and the irreversible consequences of tool calls can lead to harmful outcomes\. These failure modes include indirect prompt injection, metric gaming under performance pressure, dangerous code execution, and identity confusion across delegating agents\([Sotiropoulos et al\. 2025](https://arxiv.org/html/2609.18128#bib.bib41)\)\.

Several approaches grade a recorded trajectory post hoc with anLLMjudge or a learned detector\([Zheng et al\. 2023](https://arxiv.org/html/2609.18128#bib.bib54);[Sharma, Barke, and Zorn 2026](https://arxiv.org/html/2609.18128#bib.bib39);[Wen et al\. 2026](https://arxiv.org/html/2609.18128#bib.bib45)\), but their verdicts are stochastic and hard to reproduce\. Enforcement mechanisms instead block unsafe actions in real time, yet they judge each action in isolation and miss properties that span the trajectory\([Wang, Poskitt, and Sun 2026](https://arxiv.org/html/2609.18128#bib.bib43);[Inan et al\. 2023](https://arxiv.org/html/2609.18128#bib.bib22)\), attach to semantic intent rather than tool\-call behavior\([Kamath et al\. 2025](https://arxiv.org/html/2609.18128#bib.bib24);[Miculicich et al\. 2025](https://arxiv.org/html/2609.18128#bib.bib29)\), or depend on a model of the specific agent\([Wang et al\. 2025](https://arxiv.org/html/2609.18128#bib.bib44)\)\. No single deterministic artifact both guards an agent online and grades a recorded trajectory offline\.

![Refer to caption](https://arxiv.org/html/2609.18128v1/image/agent.png)Figure 1:𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}monitors the tool\-call interface between anLLMagent and its tools\.Inspired byassume\-guarantee \(A/G\)contract\-based design\([Benveniste et al\. 2018](https://arxiv.org/html/2609.18128#bib.bib8);[Nuzzo et al\. 2015](https://arxiv.org/html/2609.18128#bib.bib32)\), whose compositional reasoning has been applied to cyber\-physical systems\([Xiao et al\. 2024](https://arxiv.org/html/2609.18128#bib.bib49);[Xiao and Nuzzo 2026](https://arxiv.org/html/2609.18128#bib.bib48);[Xiao et al\. 2026](https://arxiv.org/html/2609.18128#bib.bib47)\), we present𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}, a contract\-based, model\-agnostic, deterministic framework for symbolic temporal supervision ofLLMagents\. We formalize trajectory\-level requirements asA/Gcontracts inlinear temporal logic on finite traces \(LTLf\)\([De Giacomo and Vardi 2013](https://arxiv.org/html/2609.18128#bib.bib15)\)over checkableatomic propositions \(AP\)on agent actions\. Contracts are compiled todeterministic finite automaton \(DFA\)checkers that supervise the agent’s trajectory, by gating agent actions online, as shown in Figure[1](https://arxiv.org/html/2609.18128#S1.F1), or evaluating recorded traces offline\. Our contributions can be summarized as follows:

- •We introduceA/Gcontracts as formal specifications of intent requirements forLLMagents, using a set of checkableAPover tool\-call traces and forming a contract library\.
- •We present𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}, a model\-agnostic, deterministic supervision framework forLLMagents using contracts to both shield an agent online and score its traces offline\.
- •We evaluate𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}across four benchmarks spanning both roles, showing it matches strong LLM\-judge and guardrail baselines at orders of magnitude lower per\-call latency, and provides a deterministic, reproducible evaluator of recorded traces\.

The remainder of the paper is organized as follows\. After discussing related work in Section[2](https://arxiv.org/html/2609.18128#S2), we provide background on agent frameworks,LTLf, andA/Gcontracts in Section[3](https://arxiv.org/html/2609.18128#S3)\. Section[4](https://arxiv.org/html/2609.18128#S4)introduces interaction predicates and agent contracts, while Section[5](https://arxiv.org/html/2609.18128#S5)provides details on contract compilation and contract\-based supervision\. Section[6](https://arxiv.org/html/2609.18128#S6)reports results from the four benchmarks, and is followed by concluding remarks in Section[7](https://arxiv.org/html/2609.18128#S7)\.

## 2Related Work

Most runtime safeguards for tool\-based operation ofLLMagents act at the tool\-call boundary\. Per\-action rule languages such as AgentSpec\([Wang, Poskitt, and Sun 2026](https://arxiv.org/html/2609.18128#bib.bib43)\)check each proposed call against a set of rules\. They are fast and deterministic but scoped to a single action rather than reasoning about a trajectory’s action ordering, history, or counts\. A separate information\-flow line of work tracks data and privilege across the execution to stop prompt injection and exfiltration, as in Progent\([Shi et al\. 2025](https://arxiv.org/html/2609.18128#bib.bib40)\), CaMeL\([Debenedetti et al\. 2025](https://arxiv.org/html/2609.18128#bib.bib17)\), RTBAS\([Zhong et al\. 2025](https://arxiv.org/html/2609.18128#bib.bib55)\), and Fides\([Costa et al\. 2025](https://arxiv.org/html/2609.18128#bib.bib14)\)\. The threat model considered in this line of work is, however, orthogonal to𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}’s contracts\.

A class of approaches uses logic to reason about the execution trace: Agent\-C\([Kamath et al\. 2025](https://arxiv.org/html/2609.18128#bib.bib24)\)checks temporal constraints withsatisfiability modulo theories \(SMT\)solving during generation, VeriGuard\([Miculicich et al\. 2025](https://arxiv.org/html/2609.18128#bib.bib29)\)generates policy code with anLLMand formally verifies it before use, and FORGE\([Palumbo et al\. 2026](https://arxiv.org/html/2609.18128#bib.bib34)\)weaves deterministic Datalog policies into multi\-agent deployments\. However, none of them maintains a symbolic verdict over the whole trajectory\. Safety Chip\([Yang et al\. 2024](https://arxiv.org/html/2609.18128#bib.bib51)\)compiles propositionallinear temporal logic \(LTL\)to mask unsafe actions of embodied robot agents, whereas𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}supervises general tool\-callingLLMagents withA/Gcontracts over checkableAP\.

Another class of approaches aims to grade or shield behaviors using a learned model or anLLMjudge\.LLM\-as\-judge graders\([Zheng et al\. 2023](https://arxiv.org/html/2609.18128#bib.bib54)\), AgentPex\([Sharma, Barke, and Zorn 2026](https://arxiv.org/html/2609.18128#bib.bib39)\), and learned detectors such as PolicyGuard\([Wen et al\. 2026](https://arxiv.org/html/2609.18128#bib.bib45)\)score recorded trajectories, but their verdicts are stochastic and hard to reproduce, particularly on safety judgments\([Chen and Goldfarb\-Tarrant 2025](https://arxiv.org/html/2609.18128#bib.bib11)\)\. ShieldAgent\([Chen, Kang, and Li 2025](https://arxiv.org/html/2609.18128#bib.bib12)\)compiles policy documents into action\-based probabilistic rule circuits, ABC\([Bhardwaj 2026](https://arxiv.org/html/2609.18128#bib.bib9)\)enforces behavioral contracts under a probabilistic satisfaction relation, and ProbGuard\([Wang et al\. 2025](https://arxiv.org/html/2609.18128#bib.bib44)\)predicts violations by probabilistic model checking of a learned agent model, so their verdicts are probabilistic and are not used to deterministically block undesirable behaviors\.

## 3Preliminaries

As we aim to supervise an agent’s tool calls withA/Gcontracts, we first give background on agent frameworks and temporal logic, then state the supervision problem\.

### 3\.1Agent Frameworks

An agent pairs anLLMbackbone with a tool set, issuing tool calls and folding their outputs into a reasoning loop until task completion\([Yao et al\. 2023](https://arxiv.org/html/2609.18128#bib.bib52)\)\. The*tool\-call interface*is the set of tools the framework exposes to the agent, together with their call and return conventions\. Reasoning steps carry the agent’s decision making, but they take external effect only through the tool calls they issue, and the class of irreversible consequences this paper targets arises at this interface\.𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}therefore tracks the*tool\-call trace*, the ordered sequence of tool\-call events the agent emits, now often a long\-horizon, multi\-tool trajectory\([Xu et al\. 2026](https://arxiv.org/html/2609.18128#bib.bib50)\)\.

###### Definition 1\(Agent session\)

LetΣ\\Sigmadenote the finite set of tool\-call*events*\. Each tool call produces two events: a*call*eventa=\(𝗍𝗈𝗈𝗅,𝖺𝗋𝗀𝗌\)a=\(\\mathsf\{tool\},\\mathsf\{args\}\)when the agent issues the call, and a*return*eventa′=\(𝗍𝗈𝗈𝗅,𝗋𝖾𝗌𝗎𝗅𝗍\)a^\{\\prime\}=\(\\mathsf\{tool\},\\mathsf\{result\}\)when the executed tool returns\. An agent’s execution is a transition system\([Baier and Katoen 2008](https://arxiv.org/html/2609.18128#bib.bib3)\)𝒯=\(S,s0,Σ,R\)\\mathcal\{T\}=\(S,s\_\{0\},\\Sigma,R\)\. A states:=\(τ,κ,ρ\)∈Ss:=\(\\tau,\\kappa,\\rho\)\\in Scomprises the traceτ∈Σ∗\\tau\\in\\Sigma^\{\*\}of events issued so far, a finite mapκ\\kappafrom context keys to values recorded from earlier events, and a vectorρ\\rhoof numeric session counters, withs0:=\(ε,κ0,ρ0\)s\_\{0\}:=\(\\varepsilon,\\kappa\_\{0\},\\rho\_\{0\}\)\. Each eventaainduces a transition\(s,a,s′\)∈R\(s,a,s^\{\\prime\}\)\\in Rthat appendsaatoτ\\tauand updatesκ\\kappaandρ\\rho\. An agent*session*is a finite paths0→a1⋯→aksks\_\{0\}\\xrightarrow\{a\_\{1\}\}\\cdots\\xrightarrow\{a\_\{k\}\}s\_\{k\}, with traceτ=a1⋯ak\\tau=a\_\{1\}\\cdots a\_\{k\}\.

A context key records a fact carried across events, such as the caller’s identity or a document’s source, and a counter tracks a cumulative quantity, such as the tokens consumed\.

### 3\.2Finite\-Trace LTL \(LTLf\)

LTL\([Pnueli 1977](https://arxiv.org/html/2609.18128#bib.bib35)\)extends propositional logic to reason over infinite sequences of propositional interpretations, or*traces*\.LTLf\([De Giacomo and Vardi 2013](https://arxiv.org/html/2609.18128#bib.bib15)\)restricts this logic to finite traces\. LetA​PAPbe a finite set of atomic propositions\. The class ofLTLfformulae overA​PAPis defined by the grammarφ::=P​∣¬φ​∣φ∧φ′​∣X​φ∣​F​φ∣​G​φ∣​φ​U​φ′,\\varphi::=P\\mid\\neg\\varphi\\mid\\varphi\\wedge\\varphi^\{\\prime\}\\mid X\\,\\varphi\\mid F\\,\\varphi\\mid G\\,\\varphi\\mid\\varphi\\,U\\,\\varphi^\{\\prime\},whereP∈A​PP\\in APis anAPandφ′\\varphi^\{\\prime\}is anLTLfformula, with temporal operatorsXX\(next\),FF\(eventually\),GG\(always\), andUU\(until\)\. EachLTLfformula compiles to an equivalentDFAthat accepts exactly the traces satisfying it\([De Giacomo and Vardi 2013](https://arxiv.org/html/2609.18128#bib.bib15)\), which is the canonical monitor construction of runtime verification\([Bauer, Leucker, and Schallhart 2011](https://arxiv.org/html/2609.18128#bib.bib6);[Leucker and Schallhart 2009](https://arxiv.org/html/2609.18128#bib.bib25)\)\.

When an atomic predicate is used to compare an arithmetic quantity read from the session statess, such as a call count or token total accumulated inρ\\rho, or an argument value latched intoκ\\kappa, against a bound, then it is better captured by a linear\-arithmetic constraint than by a plain proposition\. AnLTLfformula over such atoms is then taken modulo linear arithmetic, i\.e\., arithmetic LTLf\(ALTLf\)\([Felli et al\. 2023](https://arxiv.org/html/2609.18128#bib.bib19)\), an instance ofLTLfmodulo theories\([Geatti, Gianola, and Gigante 2022](https://arxiv.org/html/2609.18128#bib.bib20)\)\.𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}evaluates every atom*pointwise*, i\.e\., its truth value at each event is computed from the current eventaaand the session statess\.

### 3\.3Assume\-Guarantee \(A/G\) Contracts

LetMMdenote a component, i\.e\., an element of a system, characterized by a set of variablesVcV\_\{c\}and a set of behaviors⟦M⟧\\llbracket M\\rrbracketoverVcV\_\{c\}\. A contractCCformally captures a set of specifications forMMusing a tripleC=\(Vc,A,G\)C=\(V\_\{c\},A,G\)\([Benveniste et al\. 2018](https://arxiv.org/html/2609.18128#bib.bib8)\), whereAAandGGare sets of behaviors overVcV\_\{c\}\.AAis the assumptions on the environment ofMMwhileGGis the guarantees provided byMM, given that the assumptions are satisfied\. We say thatMMis a valid implementation ofCC, i\.e\.,M⊧CM\\models C, if all the behaviors ofMMare included in the guarantees given the assumptions ofCC, i\.e\.,⟦M⟧⊆G∪A¯\\llbracket M\\rrbracket\\subseteq G\\cup\\overline\{A\}\. We say that componentEcE\_\{c\}is a valid environment ofCCif all the behaviors ofEcE\_\{c\}are contained in the assumptions ofCC\. A contract is*consistent*if and only if there exists a valid implementation, i\.e\.,G∪A¯≠∅G\\cup\\overline\{A\}\\neq\\emptyset, and it is*compatible*if there exists a valid environmentEcE\_\{c\}, i\.e\.,A≠∅A\\neq\\emptyset\.

𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}formalizes contracts over the agent’s tool\-call trace: the component is the agent, whose behaviors⟦M⟧\\llbracket M\\rrbracketare the tool\-call traces it can produce \(Def\.[1](https://arxiv.org/html/2609.18128#Thmmydefinition1)\), and the variablesVcV\_\{c\}are the setA​PAP\. At runtime, a session exposes a single behavior of this component, and𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}evaluates the observed traceτ\\tauby the three\-valued valuation below\.

###### Definition 2\(Runtime contract valuation\)

A contractCCis a pair\(A,G\)\(A,G\)of ALTLfproperties overA​PAP\. Against a concrete traceτ\\tau, its valuation takes one of three values, namedIDLE\\mathrm\{IDLE\}\(11\),ACTIVE\\mathrm\{ACTIVE\}\(ee\), andFAIL\\mathrm\{FAIL\}\(00\), ordered as0≤e≤10\\leq e\\leq 1, following the multi\-valued verdicts of runtime verification\([Bauer, Leucker, and Schallhart 2006](https://arxiv.org/html/2609.18128#bib.bib5)\):

⟦\(A,G\)⟧​\(τ\)=\{1,τ⊧A¯,e,τ⊧A∧G,0,τ⊧A∧G¯\.\\llbracket\(A,G\)\\rrbracket\(\\tau\)=\\begin\{cases\}1,&\\tau\\models\\overline\{A\},\\\\ e,&\\tau\\models A\\land G,\\\\ 0,&\\tau\\models A\\land\\overline\{G\}\.\\end\{cases\}\(1\)

### 3\.4Agent Trajectory Supervision

An execution monitor can be used to halt a run at the first policy\-violating action, thus enforcing a safety property\([Schneider 2000](https://arxiv.org/html/2609.18128#bib.bib38)\)\. We adapt this approach to the agent’s tool\-call trace\.

###### Problem 1\(Agent Trajectory Supervision\)

Agent trajectory supervision is the problem of monitoring an agent’s tool\-call traceτ\\tauagainst a set of contracts𝒞=\{C1,…,Cn\}\\mathcal\{C\}=\\\{C\_\{1\},\\dots,C\_\{n\}\\\}withCi=\(Ai,Gi\)C\_\{i\}=\(A\_\{i\},G\_\{i\}\)\. We define the monitor verdictv⁡\(τ\)=\(venv​\(τ\),vag​\(τ\)\)v\(\\tau\)=\\big\(v\_\{\\mathrm\{env\}\}\(\\tau\),\\;v\_\{\\mathrm\{ag\}\}\(\\tau\)\\big\)is defined by the join and the meet of the contract valuations as follows:

venv​\(τ\)=⋁i⟦\(Ai,Gi\)⟧​\(τ\),\\displaystyle v\_\{\\mathrm\{env\}\}\(\\tau\)=\\textstyle\\bigvee\_\{i\}\\llbracket\(A\_\{i\},G\_\{i\}\)\\rrbracket\(\\tau\),\(2\)vag​\(τ\)=⋀i⟦\(Ai,Gi\)⟧​\(τ\)\.\\displaystyle v\_\{\\mathrm\{ag\}\}\(\\tau\)=\\textstyle\\bigwedge\_\{i\}\\llbracket\(A\_\{i\},G\_\{i\}\)\\rrbracket\(\\tau\)\.\(3\)The environment is not valid for at least one contract if and only ifvenv​\(τ\)=1v\_\{\\mathrm\{env\}\}\(\\tau\)=1; the agent violates at least one contract if and only ifvag​\(τ\)=0v\_\{\\mathrm\{ag\}\}\(\\tau\)=0\. Therefore, trajectory supervision provides deterministic maps over𝒞\\mathcal\{C\}as follows:

- •In*online enforcement*, it provides a mapσ:Σ∗→\{𝗉𝖺𝗌𝗌,𝖻𝗅𝗈𝖼𝗄\}\\sigma:\\Sigma^\{\*\}\\to\\\{\\mathsf\{pass\},\\mathsf\{block\}\\\}that, on the trace, returns𝖻𝗅𝗈𝖼𝗄\\mathsf\{block\}at the first prefixτk=a1⋯ak\\tau\_\{k\}=a\_\{1\}\\cdots a\_\{k\}withv⁡\(τk\)≠\(e,e\)v\(\\tau\_\{k\}\)\\neq\(e,e\)and𝗉𝖺𝗌𝗌\\mathsf\{pass\}at every earlier prefix;
- •In*offline evaluation*, it provides a mapμ:Σ∗→\{0,e,1\}2\\mu:\\Sigma^\{\*\}\\to\\\{0,e,1\\\}^\{2\}withμ⁡\(τ\)=v⁡\(τ\)\\mu\(\\tau\)=v\(\\tau\), the monitor verdict\.

𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}solves this problem using one checker per contract, executed online forσ\\sigmaand replayed offline forμ\\mu, as shown in §[5\.2](https://arxiv.org/html/2609.18128#S5.SS2)\.

## 4Agent Contracts

We introduce theinteraction predicate, the atomic proposition from which agent contracts are built\. In the following, we use⊤\\topand⊥\\botto denote the Boolean values*true*and*false*, respectively\.

###### Definition 3\(Interaction Predicate\)

We define an*interaction predicate*as a predicateP⁡\(s,a,c\)P\(s,a,c\)over a session statess, a tool\-call eventa∈Σa\\in\\Sigma\(Def\.[1](https://arxiv.org/html/2609.18128#Thmmydefinition1)\), and a parametercc\. Its truth value,⊤\\topor⊥\\bot, is a deterministic function ofss,aa, andcc, evaluated by the monitor at each event \(§[5\.1](https://arxiv.org/html/2609.18128#S5.SS1)\)\.

The parameterccinstantiates a predicate with, for example, a numeric bound or a string pattern\. Given a session, we define a set of interaction predicates monitored at runtime\. They cover a wide range of properties over the tool\-call interface: predicates over the call and the session state are evaluated at call events, and predicates over the result \(e\.g\.,𝖮𝗎𝗍𝖧𝖺𝗌\\mathsf\{OutHas\}\) at return events\. We categorize the predicates into two families, as shown in Table[1](https://arxiv.org/html/2609.18128#S4.T1)\.

Table 1:𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}’s interaction predicates \(subset; full vocabulary in Appendix[A](https://arxiv.org/html/2609.18128#A1)\)\.TTis a tool,ffan argument field,ppa regular\-expression or literal\-value pattern,PPa permission set,SSan allowed\-value set,s,ds,dargument or result fields as source and sink, andkka context value\. Numeric rows list the quantityθ\\theta; the predicate isθ⋈c\\theta\\bowtie cwith boundcc\.#### Structural predicates\.

A*structural*predicate is a deterministic Boolean test of a discrete condition: the presence or absence of an event \(e\.g\., a tool firing,𝖢𝖺𝗅𝗅\\mathsf\{Call\}, or a data flow,𝖥𝗅𝗈𝗐\\mathsf\{Flow\}\), or a pattern, equality, or membership match on a field \(e\.g\.,𝖠𝗋𝗀𝖧𝖺𝗌\\mathsf\{ArgHas\},𝖬𝖺𝗍𝖼𝗁\\mathsf\{Match\}\), with no model in the loop\.

#### Numeric predicates\.

We extend the structural family with a*stateful, numeric*family that tracks cumulative quantities over the session, such as counts and totals\. A*numeric*predicate has the formθ⁡\(s,a\)⋈c\\theta\(s,a\)\\bowtie c, with⋈∈\{≤,<,≥,\>,=\}\\bowtie\\in\\\{\\leq,<,\\geq,\>,=\\\}, whereθ\\thetaextracts a quantity from the current eventaaand statess, such as a count, a total, or an argument’s value, andccis a constant bound\. The predicate holds exactly when the comparison holds,P\(s,a,c\)=\[θ\(s,a\)⋈c\]P\(s,a,c\)=\\big\[\\,\\theta\(s,a\)\\bowtie c\\,\\big\], where\[⋅\]\[\\cdot\]is the Iverson bracket, as in𝖢𝗇𝗍⁡\(T\)≤N\\mathsf\{Cnt\}\(T\)\\leq N\. The monitor maintains each accumulated quantity in a*counter*, one entry of the vectorρ\\rhoof Def\.[1](https://arxiv.org/html/2609.18128#Thmmydefinition1), updated deterministically at each event\. Such arithmetic\-constraint atoms are what lift a contract’s logic from propositionalLTLfto its arithmetic extension ALTLf\([Felli et al\. 2023](https://arxiv.org/html/2609.18128#bib.bib19)\)\.

With theLTLfoperators, we use interaction predicates to define agent contracts for trajectory supervision as follows\.

###### Definition 4\(Agent Contract\)

An*agent contract*is a tripleC=\(V,φA,φG\)C=\(V,\\varphi\_\{A\},\\varphi\_\{G\}\), where:

1. 1\.V=Vag∪VenvV=V\_\{\\mathrm\{ag\}\}\\cup V\_\{\\mathrm\{env\}\}is a finite set of interaction predicates \(Def\.[3](https://arxiv.org/html/2609.18128#Thmmydefinition3)\), theAPof the contract’s formulas, whereVagV\_\{\\mathrm\{ag\}\}collects the predicates decided by the agent’s own actions andVenvV\_\{\\mathrm\{env\}\}those decided by its environment\.
2. 2\.The assumptionφA\\varphi\_\{A\}is an ALTLfformula overVenvV\_\{\\mathrm\{env\}\}, and the guaranteeφG\\varphi\_\{G\}is an ALTLfformula overVV, both according to the grammar of §[3](https://arxiv.org/html/2609.18128#S3)\.

The partition ofVVmirrors the distinction between controlled and uncontrolled variables in contract\-based design\([Benveniste et al\. 2008](https://arxiv.org/html/2609.18128#bib.bib7)\)\. For example,𝖢𝖺𝗅𝗅\\mathsf\{Call\},𝖠𝗋𝗀𝖧𝖺𝗌\\mathsf\{ArgHas\}, and𝖢𝗇𝗍\\mathsf\{Cnt\}track the tool calls that the agent itself issues \(Def\.[1](https://arxiv.org/html/2609.18128#Thmmydefinition1)\), their arguments, and the counts derived from them, so they belong toVagV\_\{\\mathrm\{ag\}\}\.𝖮𝗎𝗍𝖧𝖺𝗌\\mathsf\{OutHas\},𝖨𝗇\\mathsf\{In\}, and𝖯𝖾𝗋𝗆\\mathsf\{Perm\}track tool results, user input, and granted permissions, so they belong toVenvV\_\{\\mathrm\{env\}\}\. The actions of other agents also belong to the environment\. Semantically, an agent’s session satisfies the contract when its trace satisfiesφA→φG\\varphi\_\{A\}\\rightarrow\\varphi\_\{G\}, with\(φA,φG\)\(\\varphi\_\{A\},\\varphi\_\{G\}\)instantiating the pair\(A,G\)\(A,G\)of Def\.[2](https://arxiv.org/html/2609.18128#Thmmydefinition2)\. Such contracts capture a wide range of trajectory properties over the tool\-call interface, including order\-, history\-, and count\-dependent ones \(Appendix[B](https://arxiv.org/html/2609.18128#A2)\)\.

Temporal Logic \(ALTLf\)operatorsG​F​X​UG\\ \\,F\\ \\,X\\ \\,Ulift predicates over the trajectory¬𝖢𝖺𝗅𝗅⁡\(𝗋𝖾𝖿𝗎𝗇𝖽\)​U​𝖢𝖺𝗅𝗅​\(𝖺𝗉𝗉𝗋𝗈𝗏𝖾\)∧G⁡\(𝖢𝖺𝗅𝗅⁡\(𝗋𝖾𝖿𝗎𝗇𝖽\)→𝖭𝗎𝗆⁡\(𝗋𝖾𝖿𝗎𝗇𝖽,𝖺𝗆𝗈𝗎𝗇𝗍\)≤42\)\\lnot\\mathsf\{Call\}\(\\mathsf\{refund\}\)\\,U\\,\\mathsf\{Call\}\(\\mathsf\{approve\}\)\\,\\wedge\\,G\\big\(\\mathsf\{Call\}\(\\mathsf\{refund\}\)\\\!\\to\\\!\\mathsf\{Num\}\(\\mathsf\{refund\},\\mathsf\{amount\}\)\\,\\leq\\,42\\big\)Structural Predicatespresence or pattern match𝖢𝖺𝗅𝗅\(𝗋𝖾𝖿𝗎𝗇𝖽\)=⊤\\mathsf\{Call\}\(\\mathsf\{refund\}\)=\\top𝖬𝖺𝗍𝖼𝗁\(𝖺𝖼𝖼𝗈𝗎𝗇𝗍,𝖺𝗉𝗉𝗋\)=⊤\\mathsf\{Match\}\(\\mathsf\{account\},\\mathsf\{appr\}\)=\\top𝖢𝖺𝗅𝗅\(𝖺𝗉𝗉𝗋𝗈𝗏𝖾\)=⊤\\mathsf\{Call\}\(\\mathsf\{approve\}\)=\\topNumeric Predicatesthreshold over accumulators𝖢𝗇𝗍⁡\(𝗋𝖾𝖿𝗎𝗇𝖽\)=3≤5\\mathsf\{Cnt\}\(\\mathsf\{refund\}\)=3\\leq 5𝖳𝗈𝗄=1200≤2000\\mathsf\{Tok\}=1200\\leq 2000𝖺𝗆𝗈𝗎𝗇𝗍=50\>42\\mathsf\{amount\}=50\>42tool\-call eventa=\(𝗋𝖾𝖿𝗎𝗇𝖽,\{𝖺𝗆𝗈𝗎𝗇𝗍:50,…\}\)a=\(\\mathsf\{refund\},\\ \\\{\\mathsf\{amount\}\{:\}\\,50,\\dots\\\}\)extract / accumulateInteraction PredicatesVVFigure 2:One tool\-call event grounded into structural and numeric predicates, then lifted by the ALTLflayer\.###### Example 1

Consider a contract whose guarantee, shown in Figure[2](https://arxiv.org/html/2609.18128#S4.F2), isφG=¬𝖢𝖺𝗅𝗅⁡\(𝗋𝖾𝖿𝗎𝗇𝖽\)​U​𝖢𝖺𝗅𝗅​\(𝖺𝗉𝗉𝗋𝗈𝗏𝖾\)∧G⁡\(𝖢𝖺𝗅𝗅⁡\(𝗋𝖾𝖿𝗎𝗇𝖽\)→𝖭𝗎𝗆⁡\(𝗋𝖾𝖿𝗎𝗇𝖽,𝖺𝗆𝗈𝗎𝗇𝗍\)≤42\)\\varphi\_\{G\}=\\lnot\\mathsf\{Call\}\(\\mathsf\{refund\}\)\\,U\\,\\mathsf\{Call\}\(\\mathsf\{approve\}\)\\wedge G\\big\(\\mathsf\{Call\}\(\\mathsf\{refund\}\)\\rightarrow\\mathsf\{Num\}\(\\mathsf\{refund\},\\mathsf\{amount\}\)\\leq 42\\big\), where $42 is the approved amount recorded by an earlier𝖺𝗉𝗉𝗋𝗈𝗏𝖾\\mathsf\{approve\}call\. Take the call eventa=\(𝗋𝖾𝖿𝗎𝗇𝖽,\{𝖺𝗆𝗈𝗎𝗇𝗍:50,…\}\)a=\(\\mathsf\{refund\},\\\{\\mathsf\{amount\}\{:\}\\,50,\\dots\\\}\)\. The structural predicates hold,𝖢𝖺𝗅𝗅\(𝗋𝖾𝖿𝗎𝗇𝖽\)=⊤\\mathsf\{Call\}\(\\mathsf\{refund\}\)=\\topand𝖬𝖺𝗍𝖼𝗁\(𝖺𝖼𝖼𝗈𝗎𝗇𝗍,𝖺𝗉𝗉𝗋\)=⊤\\mathsf\{Match\}\(\\mathsf\{account\},\\mathsf\{appr\}\)=\\top, since𝖺𝗉𝗉𝗋𝗈𝗏𝖾\\mathsf\{approve\}was called first and the account matches\. The numeric predicate𝖭𝗎𝗆⁡\(𝗋𝖾𝖿𝗎𝗇𝖽,𝖺𝗆𝗈𝗎𝗇𝗍\)≤42\\mathsf\{Num\}\(\\mathsf\{refund\},\\mathsf\{amount\}\)\\leq 42evaluates to⊥\\botat𝖺𝗆𝗈𝗎𝗇𝗍=50\\mathsf\{amount\}=50, so the guarantee, and with it the contract, falls toFAIL\\mathrm\{FAIL\}\.

## 5The𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}Framework

Given the agent contracts, as defined in §[4](https://arxiv.org/html/2609.18128#S4),𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}proceeds in two stages\. In the*offline*stage \(§[5\.1](https://arxiv.org/html/2609.18128#S5.SS1)\), it abstracts requirement artifacts into contracts and translates each contract into a deterministic monitor, theDFAassociated with its ALTLfformula\. In the*online*stage \(§[5\.2](https://arxiv.org/html/2609.18128#S5.SS2)\), it supervises the agent by advancing every monitor over the tool\-call trace and gating each call on the joint verdict \(Problem[1](https://arxiv.org/html/2609.18128#Thmmyproblem1)\)\.

![Refer to caption](https://arxiv.org/html/2609.18128v1/image/framework.png)Figure 3:The𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}framework: authoring inputs compile once into a contract checker \(top\), read online to block the first violating call \(bottom left\) and offline to score a recorded trace \(bottom right\)\.### 5\.1Contract Compilation

Contract compilation extracts contracts from requirement artifacts \(e\.g\., natural language, policy documents, recorded traces\) into ALTLfformulas over the interaction predicates of §[4](https://arxiv.org/html/2609.18128#S4), then compiles them intoDFAs\(Figure[3](https://arxiv.org/html/2609.18128#S5.F3)\)\. The two steps are described next\.

#### Contract formulation\.

Besides manually written ALTLfcontracts, we support translating natural\-language requirements and extracting rules from policy documents\. Following a lift\-then\-ground decomposition\([Liu et al\. 2023](https://arxiv.org/html/2609.18128#bib.bib27)\), theLLMfirst*lifts*each utterance to an ALTLfformula with placeholder leaves, and a deterministic step then*grounds*those placeholders to interaction predicates from Table[1](https://arxiv.org/html/2609.18128#S4.T1), yielding the closed formula\. TheLLMthus fills templates over the fixed vocabulary of Table[1](https://arxiv.org/html/2609.18128#S4.T1)\([Wang et al\. 2023](https://arxiv.org/html/2609.18128#bib.bib42)\)with a few prompt examples\. Each formula is translated back to natural language for human review\([Cosler et al\. 2023](https://arxiv.org/html/2609.18128#bib.bib13)\)\.

#### Automaton construction\.

By the standardLTLf\-to\-DFAconstruction\([De Giacomo and Vardi 2013](https://arxiv.org/html/2609.18128#bib.bib15)\), every contract formula overVVcompiles to aDFAwhose alphabet is the set2V2^\{V\}of predicate valuations\. TheDFAreads a trace one event at a time, taking a transition on the predicate valuation at that event, and accepts exactly the finite traces that satisfy the formula\. We call*grounding*the deterministic step that evaluates each predicate on the current event and the counters, producing the valuation read by theDFA\. For a numeric predicate, grounding evaluates the arithmetic constraintθ⁡\(s,a\)⋈c\\theta\(s,a\)\\bowtie cagainst the session’s counters, and theDFAconstruction stays standard\. The counter state is read only during grounding and is not encoded in theDFA, which keeps it finite\. A contract carries two such formulas, the assumptionφA\\varphi\_\{A\}and the guaranteeφG\\varphi\_\{G\}, so each compiles to its ownDFA\. We store the twoDFAsas one checker corresponding to the contract for agent supervision\.

#### Contract library\.

The compiled checkers form a*contract library*that𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}loads at runtime\. Because a contract is written over interaction predicates rather than any model’s internals, the library is portable: the same checkers apply unchanged across agents andLLMmodels that share a tool interface, so a domain’s policies transfer between models\. For each contract,𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}first checks consistency and compatibility, and also checks the loaded library is*conflict\-free*: the conjunction⋀i\(Ai∧Gi\)\\bigwedge\_\{i\}\(A\_\{i\}\\wedge G\_\{i\}\)of its ALTLfformulas is satisfiable\. When it is not, we extract a minimal unsatisfiable core\([Roveri et al\. 2024](https://arxiv.org/html/2609.18128#bib.bib37);[Ielo et al\. 2026](https://arxiv.org/html/2609.18128#bib.bib21)\)to locate the contracts to repair\.

### 5\.2Contract\-Based Supervision

At each event,𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}evaluates every interaction predicate and advances each loaded contract’s twoDFAson the resulting valuation\. The two runs decide the contract’s value in Def\.[2](https://arxiv.org/html/2609.18128#Thmmydefinition2), and the values of all loaded contracts give the verdictv⁡\(τ\)v\(\\tau\)of Problem[1](https://arxiv.org/html/2609.18128#Thmmyproblem1)\.

Because each contract is a single\(A,G\)\(A,G\)pair checked independently, a violation is fully traceable: it names the contract that violated and the event that triggered it, so an operator can tell whether the fault lies in the agent flow, in its environment, or in a contract that is too restrictive, and repair the last by relaxing the guarantee or weakening the assumption\. This modularity also lets the system enforce multiple policies at once, without merging them into a monolithic formula\.

#### Runtime enforcement\.

At runtime,𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}realizes the enforcement mapσ\\sigmaof Problem[1](https://arxiv.org/html/2609.18128#Thmmyproblem1)\. As shown in Figure[3](https://arxiv.org/html/2609.18128#S5.F3), before the tool executes, it advances every loaded contract and returns𝖻𝗅𝗈𝖼𝗄\\mathsf\{block\}at the first event whose verdict is not\(e,e\)\(e,e\)\. Every event is checked when it enters the trace and before it takes effect \(Def\.[1](https://arxiv.org/html/2609.18128#Thmmydefinition1)\), so the verdict is computed before a call executes and before an incoming event reaches the agent\. A call that would falsify a guarantee is rejected, and a return or input event that would falsify an assumption is*suppressed*\. Neither event is recorded, so the session continues from the last prefix whose verdict was\(e,e\)\(e,e\)\. The first keeps the agent a valid implementation of the contract and the second keeps its environment a valid environment, as in bidirectional runtime enforcement\([Aceto et al\. 2021](https://arxiv.org/html/2609.18128#bib.bib1)\)\. The check is incremental: rather than synthesizing each contract’sDFAsin full,𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}keeps a residual formula and progresses it one event at a time\([Roşu and Havelund 2005](https://arxiv.org/html/2609.18128#bib.bib36)\), so the per\-event cost isO⁡\(\|𝒞\|\)O\(\|\\mathcal\{C\}\|\), where𝒞\\mathcal\{C\}is the set of loaded contracts, independent of the trace length\. Supervision thus scales to long horizons\.

When the blocked event is a call, the enforcement action is decided by the strategy carried by the violated contract:*block*the call \(the default\),*redirect*it to a safe alternative, or*escalate*to a human\. The outcome returns to the model as a structured message: the identifier of the contract involved, a short explanation, and, where it applies, the suggested replacement or required next action, so the agent can steer its trajectory back into the safe region\. For example, a contract that forbids issuing a refund before approval can return a message like “the actionissue\_refundwas rejected: callcheck\_policyfirst”\.

Prompting for a requested action lets𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}act proactively, on a satisfied trigger rather than on a violation\. Consider a prescriptive guaranteeG⁡\(𝑡𝑟𝑖𝑔→X​𝑡𝑜𝑜𝑙\)G\(\\mathit\{trig\}\\rightarrow X\\,\\mathit\{tool\}\); when the trigger𝑡𝑟𝑖𝑔\\mathit\{trig\}is satisfied and gets𝗉𝖺𝗌𝗌\\mathsf\{pass\}, a feedback message can ask the agent to call the required tool next\. An unbounded liveness guaranteeG⁡\(𝑡𝑟𝑖𝑔→F​𝑟𝑒𝑠𝑝\)G\(\\mathit\{trig\}\\rightarrow F\\,\\mathit\{resp\}\)cannot be refuted by any finite prefix: after𝑡𝑟𝑖𝑔\\mathit\{trig\}is satisfied, it stays pending until𝑟𝑒𝑠𝑝\\mathit\{resp\}occurs\. At the end of the agent session,𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}surfaces every still\-pending guarantee as a feedback message asking the agent to perform𝑟𝑒𝑠𝑝\\mathit\{resp\}, and a guarantee left unsatisfied collapses toFAIL\\mathrm\{FAIL\}\.

#### Offline evaluation\.

Contracts also serve as a deterministic evaluation engine for recorded traces:μ:Σ∗→\{0,e,1\}2\\mu:\\Sigma^\{\*\}\\to\\\{0,e,1\\\}^\{2\}of Problem[1](https://arxiv.org/html/2609.18128#Thmmyproblem1), as shown in Figure[3](https://arxiv.org/html/2609.18128#S5.F3)\.𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}replays a recorded trace and returns its end\-of\-trace verdictμ⁡\(τ\)=v⁡\(τ\)\\mu\(\\tau\)=v\(\\tau\)instead of gating actions, one value for the agent and one for its environment\. The difference from enforcement is that the trace is fixed, so there is no intervention; and because eachviv\_\{i\}depends only on the trace, the offline replay and the online monitor traverse the same states and agree on the verdict at every prefix\. When many traces are checked against the same contracts, theDFAsare built once and reused, turning each event into a single table lookup \(O⁡\(1\)O\(1\)\)\. Offline evaluation is thus deterministic and reproducible: the same trace always yields the same verdict and per\-contract attribution, not a single pass/fail rate\.

## 6Evaluation

Our implementation111https://github\.com/yfxiao16/ContrAgentis in Python 3\.12; it exports contract libraries to CHASE\([Nuzzo et al\. 2018](https://arxiv.org/html/2609.18128#bib.bib31)\)for design\-time contract analysis, and usesmus2muc\([Ielo et al\. 2026](https://arxiv.org/html/2609.18128#bib.bib21)\)for conflict\-core extraction and Z3\([de Moura and Bjørner 2008](https://arxiv.org/html/2609.18128#bib.bib16)\)for the numeric consistency check\. The contract library is built with anLLMfollowing the formulation pipeline of §[5\.1](https://arxiv.org/html/2609.18128#S5.SS1), over the interaction predicates of Table[1](https://arxiv.org/html/2609.18128#S4.T1)\. Integration hooks intercept each event and ground it deterministically through pattern matches and counter updates\. Latency measurements reported below were taken on an Apple M4 Pro laptop \(24 GB\)\.

#### Benchmarks\.

We evaluate𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}on four benchmarks, each isolating one claim\. The enforcement role is tested by SOPBench\([Li et al\. 2025](https://arxiv.org/html/2609.18128#bib.bib26)\)\(§[6\.1](https://arxiv.org/html/2609.18128#S6.SS1)\) and AgentDojo\([Debenedetti et al\. 2024](https://arxiv.org/html/2609.18128#bib.bib18)\)\(§[6\.2](https://arxiv.org/html/2609.18128#S6.SS2)\); the evaluation role by R\-Judge\([Yuan et al\. 2024](https://arxiv.org/html/2609.18128#bib.bib53)\)\(§[6\.3](https://arxiv.org/html/2609.18128#S6.SS3)\) andτ2\\tau^\{2\}\-bench\([Barres et al\. 2025](https://arxiv.org/html/2609.18128#bib.bib4)\)\(§[6\.4](https://arxiv.org/html/2609.18128#S6.SS4)\)\.

### 6\.1Standard Operating Procedure Enforcement

SOPBench\([Li et al\. 2025](https://arxiv.org/html/2609.18128#bib.bib26)\)evaluates whether a language agent follows an explicit standard operating procedure \(SOP\) across seven customer\-service domains \(bank,DMV,healthcare,hotel,library,university,online market\), where each task provides a constraint graph, numeric thresholds, an initial database, and a label indicating whether the policy permits the goal\. We compared𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}with three baselines: \(1\) the base model with no SOP, \(2\) the base model prompted with the SOP, and \(3\) a secondLLMthat judges each call against the SOP\. We report*success*and*safety*metrics, representing goal completion on tasks the SOP permits and correct blocking on tasks the SOP forbids, respectively\.

We build each domain’s agent contracts from its public SOP, compiling the SOP’s gate/chain tree\. As shown in Table[2](https://arxiv.org/html/2609.18128#S6.T2),𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}enforcement holds success at the base level while raising safety from32%32\\%to98%98\\%, above prompt’s94%94\\%\. Prompting andLLM\-guard also achieve high safety \(94%94\\%and98%98\\%\), but reduce mean success to64%64\\%and24%24\\%, respectively, because of over\-blocking\. Both residual gaps trace to the agent rather than the enforcement layer: inhealthcareit fails to retry after a block, and inuniversityit makes a permitted change to a target the benchmark’s outcome\-based scoring cannot distinguish from the forbidden one\.

The runtime cost of𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}is lower than both prompt andLLM\-guard, since it neither increases the prompt length nor calls a second model on every action\. Each entry is a mean over three seeded trials;𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}’s enforcement is stable across trials, with per\-domain deviation≤0\.4\\leq 0\.4percentage points \(pp\), versus22to44ppfor the model\-driven conditions\.

Table 2:SOPBench results \(gemini\-2\.5\-flash, 40 tasks/domain\); each cell is success \(Su\.\) / safety \(Sf\.\) %\.avg\. runtime: thebasecell is its median runtime per task; the other cells are the median*extra*time over base\.1–23–45–67–910\+00252550507575100100\# SOP constraintssuccess %basepromptLLM\-grd𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}1–23–45–67–910\+\# SOP constraintssafety %Figure 4:SOPBench success \(left\) and safety \(right\) vs\. SOP constraint count, pooled over seven domains\.baseno detectortrace\-learned

0\.10\.1111010gemini\-2\-flashgemini\-2\-flash\-expgemini\-1\.5\-pro\-2llama\-3\-70bclaude\-3\-sonnetgpt\-4o\-minigemini\-1\.5\-progpt\-4\-turbogpt\-4oclaude\-3\.5\-sonnetgpt\-4\-01250\.10\.1111010claude\-3\.5\-sonnet\-2meta\-secalign\-70bcommand\-rgemini\-1\.5\-flash\-2command\-r\-plusclaude\-3\.7\-sonnetclaude\-3\-haikugpt\-3\.5\-turboclaude\-3\-opusgemini\-1\.5\-flashllama\-3\.3\-70b

Prompt\-injection attack\-success rate \(%, log scale\)

Figure 5:Indirect prompt\-injection prevention across2222LLMson AgentDojo; left and right are the higher\- and lower\-ASR halves\.
pass4joint4

00202040406060o4\-miniGPT\-4\.1\-miniGPT\-4\.1Claude 3\.7o4\-miniGPT\-4\.1\-miniGPT\-4\.1Claude 3\.7o4\-miniGPT\-4\.1\-miniGPT\-4\.1Claude 3\.7RetailAirlineTelecom

Task\-level success rate \(%,k=4k=4\)

Figure 6:Theτ2\\tau^\{2\}\-bench procedural reliability across three domains and four models\.

#### Model\-agnostic supervision\.

With the same contract library, ongemini\-2\.5\-flash\-lite, where the unguarded base stays at27%27\\%, prompt’s mean safety collapses from94%94\\%to45%45\\%, whereas𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}’s enforced safety is unchanged at98%98\\%, because the verdict does not depend on the agent’s model\. Moreover, replaying the same contract library over SOPBench traces from2323base models, the false\-positive rate on safe traces stays below1%1\\%for1919of2323models \(max4\.5%4\.5\\%, Llama\-3\.1\-8B\), even as the per\-model violation rate varies widely with capability \(Appendix[C](https://arxiv.org/html/2609.18128#A3)\)\.

#### SOP constraint scaling\.

Binning tasks by the number of SOP constraints \(which run from11to1717; pooled over the seven domains\) exposes the success/safety tradeoff that a single strategy hides\. As shown in Figure[4](https://arxiv.org/html/2609.18128#S6.F4), with the number of constraints increasing, prompting increasingly over\-refuses: its success on permitted tasks collapses from87%87\\%to18%18\\%in the10\+10\+bin, while the unguarded base’s safety collapses from79%79\\%to0%0\\%\. TheLLM\-guard keeps safety high, but with steep success reduction\.𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}holds success at77%77\\%or above and safety at89%89\\%or above across all bins, and the gap widens as the constraint count grows\. Exact per\-bin values and the weak\-model robustness breakdown are in Appendix[D](https://arxiv.org/html/2609.18128#A4)\.

### 6\.2Indirect Prompt Injection Prevention

AgentDojo\([Debenedetti et al\. 2024](https://arxiv.org/html/2609.18128#bib.bib18)\)embeds attacker text inside tool outputs \(email bodies, calendar entries, search results\) and measures whether the agent is steered into an unsafe action\.𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}prevents indirect prompt injection by filtering tool outputs and blocking any subsequent call that would violate the contract, regardless of whether the agent was tricked into issuing it\. The contract library is built from the task and environment specifications of AgentDojo’s four suites, without knowledge of the attacks\. It tags any value carried in by a tool output as untrusted, and blocks a side\-effecting call whose target is both untrusted\-introduced and outside the task’s legitimate set\.

Figure[6](https://arxiv.org/html/2609.18128#S6.F6)reports three results per model\. The baseline results are from AgentDojo’s published numbers\([Debenedetti et al\. 2024](https://arxiv.org/html/2609.18128#bib.bib18)\)\. We call*no\-detector*the setting in which no component flags the injected text, so that a value counts as untrusted whenever a tool output introduces it and the user has not named it\. In this setting, the library reduces the pooledattack success rate \(ASR\)from18\.0%18\.0\\%to5\.3%5\.3\\%at0\.8%0\.8\\%utilityfalse positive \(FP\)\. Contracts can also be mined from the recorded traces of the attacks themselves \(attacker recipients, unsafe actions, and the injected text as the untrusted source\), which we call*trace\-learned*contracts\. This lowers the pooledASRto1\.7%1\.7\\%at0\.3%0\.3\\%FP\. The attacks𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}misses fall into two kinds\. Most \(82%82\\%\) issue no malicious tool call at all, e\.g\., denial\-of\-service injections that only divert the agent or text\-response attacks answered in the agent’s own reply, outside what a tool\-call shield can do\. The remaining18%18\\%are prompt injections that steer the agent into a tool call whose arguments are themselves legitimate values, leaving the deterministic guard no untrusted target to flag\.

Table 3:AgentDojo defenses ongpt\-4o\(ND: no detector, TL: trace\-learned\)\.Table[3](https://arxiv.org/html/2609.18128#S6.T3)compares𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}with the defenses bundled with AgentDojo on`gpt\-4o`under its main injection attack\. Only the𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}rows are measured here; the baseline rates are AgentDojo’s published numbers, and every utility value is computed from the published runs\. Utility is the fraction of injection\-free tasks completed\. Overhead is the per\-call runtime added by a defense, and prompt\-side defenses add prompt text rather than a call\.𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}replays the recorded runs, so its utility cannot exceed that of the undefended agent\. With no detector,𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}lowers theASRfrom47\.7%47\.7\\%to11\.1%11\.1\\%and completes71\.8%71\.8\\%of the injection\-free tasks, one task fewer than the undefended agent\. The classifier reaches7\.95%7\.95\\%but completes41\.9%41\.9\\%of the tasks\. The trace\-learned variant reaches0\.79%0\.79\\%at the utility of the undefended agent\. Both variants add0\.160\.16ms per call, against5050to500500ms for the classifier and theLLMfilter, and run no model\. The per\-workload latency breakdown is in Appendix[E](https://arxiv.org/html/2609.18128#A5)\.

### 6\.3Agent Safety Risk Evaluation

R\-Judge\([Yuan et al\. 2024](https://arxiv.org/html/2609.18128#bib.bib53)\)tests whether an evaluator can detect unsafe agent behavior*post hoc*across ten operational risk types in571571multi\-turn agent records \(301301unsafe /270270safe\)\. Contracts come from R\-Judge’s risk taxonomy, a policy document \(§[5\.1](https://arxiv.org/html/2609.18128#S5.SS1)\)\.𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}reaches an average F1score of91\.8%91\.8\\%\(97\.0%97\.0\\%precision,87\.0%87\.0\\%recall\) across multiple trials\. This exceeds GPT\-4o \(74\.4%74\.4\\%\) and the R\-Judge human baseline \(≈89%\\approx\\\!89\\%\)\. AgentAuditor\([Luo et al\. 2025](https://arxiv.org/html/2609.18128#bib.bib28)\)outperforms our method at the cost of a Gemini\-2 judge with retrieval over an experiential memory\. The records we miss are semantic rather than procedural, outside what a deterministic tool\-call check can decide\.

### 6\.4Procedural Violation and Outcome Scoring

τ2\\tau^\{2\}\-bench\([Barres et al\. 2025](https://arxiv.org/html/2609.18128#bib.bib4)\)runs customer\-service agents through multi\-turn dual\-control conversations against a written policy document in three domains\. Its nativepasskmetric is outcome\-only \(final database state\)\. AgentPex\([Sharma, Barke, and Zorn 2026](https://arxiv.org/html/2609.18128#bib.bib39)\)showed83%83\\%of reward\-1\.01\.0Claude traces still violate a procedural rule\. With contract libraries built from the policy documents,𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}measures procedural compliance deterministically, whileLLMjudges can only approximate it\. We report ajointkmetric that combines outcome and zero contract violations acrosskkretries\. Figure[6](https://arxiv.org/html/2609.18128#S6.F6)exposes the gap this creates: across the4,4644\{,\}464\-trace matrix Claude 3\.7 reaches an outcomepass4of2525–60%60\\%yet ajoint4of0%0\\%in all three domains, i\.e\., no task is completed reliably without at least one procedural violation, a form of reward hacking\. Per\-cell values for every domain and model are in Appendix[F](https://arxiv.org/html/2609.18128#A6)\.

#### Limitations\.

𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}enforces only what the tool\-call structure exposes, and free\-form semantic harms need a separate content\-level check\. In this paper, the library is inspected by humans before use; autoformalization of natural\-language policies is out of the scope of this work and left as a future direction\. The counters that ground numeric predicates \(§[4](https://arxiv.org/html/2609.18128#S4)\) trust the framework to report events faithfully, and defending this observation channel itself is beyond our scope\.

## 7Conclusion

We presented𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}, a contract\-based framework that formalizes trajectory\-level specifications of large language model \(LLM\) agents as assume\-guarantee \(A/G\) contracts over checkable tool\-call predicates, expressed in arithmetic linear temporal logic on finite traces \(ALTLf\), and compiles each into a deterministic finite automaton \(DFA\) for online enforcement and offline evaluation\. The contract library acts as a model\-agnostic knowledge base of agent policies\. We illustrated the effectiveness of our approach on four benchmarks spanning both roles, where𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}matches LLM\-judge and guardrail baselines while producing deterministic, reproducible verdicts at orders of magnitude lower per\-call latency\. Future work includes compiling contracts into reward machines for post\-training and constrained decoding, and investigating contract\-based decomposition mechanisms for multi\-agent systems\.

## References

- Aceto et al\. \(2021\)Aceto, L\.; Cassar, I\.; Francalanza, A\.; and Ingólfsdóttir, A\. 2021\.On Bidirectional Runtime Enforcement\.In*Proc\. Formal Techniques for Distributed Objects, Components, and Systems \(FORTE\)*, LNCS\. Springer\.
- Anthropic \(2024\)Anthropic\. 2024\.Introducing the Model Context Protocol\.Anthropic; open protocol specification\.
- Baier and Katoen \(2008\)Baier, C\.; and Katoen, J\.\-P\. 2008\.*Principles of Model Checking*\.Cambridge, MA: MIT Press\.
- Barres et al\. \(2025\)Barres, V\.; Dong, H\.; Ray, S\.; Si, X\.; et al\. 2025\.τ2\\tau^\{2\}\-Bench: Evaluating Conversational Agents in a Dual\-Control Environment\.ArXiv preprint arXiv:2506\.07982\.
- Bauer, Leucker, and Schallhart \(2006\)Bauer, A\.; Leucker, M\.; and Schallhart, C\. 2006\.Monitoring of Real\-Time Properties\.In*Proc\. Foundations of Software Technology and Theoretical Computer Science \(FSTTCS\)*, volume 4337 of*Lecture Notes in Computer Science*, 260–272\. Springer\.
- Bauer, Leucker, and Schallhart \(2011\)Bauer, A\.; Leucker, M\.; and Schallhart, C\. 2011\.Runtime Verification for LTL and TLTL\.*ACM Transactions on Software Engineering and Methodology \(TOSEM\)*, 20\(4\): 14:1–14:64\.
- Benveniste et al\. \(2008\)Benveniste, A\.; Caillaud, B\.; Ferrari, A\.; Mangeruca, L\.; et al\. 2008\.Multiple Viewpoint Contract\-Based Specification and Design\.In*Proc\. Formal Methods for Components and Objects \(FMCO\)*, volume 5382 of*LNCS*, 200–225\. Springer\.
- Benveniste et al\. \(2018\)Benveniste, A\.; Caillaud, B\.; Nickovic, D\.; Passerone, R\.; et al\. 2018\.Contracts for System Design\.*Foundations and Trends in Electronic Design Automation*, 12\(2–3\): 124–400\.
- Bhardwaj \(2026\)Bhardwaj, V\. P\. 2026\.Agent Behavioral Contracts: Formal Specification and Runtime Enforcement for Reliable Autonomous AI Agents\.ArXiv preprint arXiv:2602\.22302\.
- Chase \(2022\)Chase, H\. 2022\.LangChain: Building Applications with LLMs through Composability\.Open\-source software\.
- Chen and Goldfarb\-Tarrant \(2025\)Chen, H\.; and Goldfarb\-Tarrant, S\. 2025\.Safer or Luckier? LLMs as Safety Evaluators Are Not Robust to Artifacts\.In*Proc\. Annual Meeting of the Association for Computational Linguistics \(ACL\)*, 19750–19766\.
- Chen, Kang, and Li \(2025\)Chen, Z\.; Kang, M\.; and Li, B\. 2025\.ShieldAgent: Shielding Agents via Verifiable Safety Policy Reasoning\.In*Proc\. International Conference on Machine Learning \(ICML\)*\.
- Cosler et al\. \(2023\)Cosler, M\.; Hahn, C\.; Mendoza, D\.; Schmitt, F\.; et al\. 2023\.nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models\.In*Proc\. Computer Aided Verification \(CAV\)*, volume 13965 of*Lecture Notes in Computer Science*, 383–396\. Springer\.
- Costa et al\. \(2025\)Costa, M\.; Köpf, B\.; Kolluri, A\.; Paverd, A\.; et al\. 2025\.Securing AI Agents with Information\-Flow Control\.ArXiv preprint arXiv:2505\.23643\.
- De Giacomo and Vardi \(2013\)De Giacomo, G\.; and Vardi, M\. Y\. 2013\.Linear Temporal Logic and Linear Dynamic Logic on Finite Traces\.In*Proc\. International Joint Conference on Artificial Intelligence \(IJCAI\)*, 854–860\.
- de Moura and Bjørner \(2008\)de Moura, L\.; and Bjørner, N\. 2008\.Z3: An Efficient SMT Solver\.In*Proc\. Tools and Algorithms for the Construction and Analysis of Systems \(TACAS\)*, volume 4963 of*Lecture Notes in Computer Science*, 337–340\. Springer\.
- Debenedetti et al\. \(2025\)Debenedetti, E\.; Shumailov, I\.; Fan, T\.; Hayes, J\.; et al\. 2025\.Defeating Prompt Injections by Design\.ArXiv preprint arXiv:2503\.18813\.
- Debenedetti et al\. \(2024\)Debenedetti, E\.; Zhang, J\.; Balunović, M\.; Beurer\-Kellner, L\.; et al\. 2024\.AgentDojo: A Dynamic Environment to Evaluate Prompt Injection Attacks and Defenses for LLM Agents\.In*Proc\. Conference on Neural Information Processing Systems \(NeurIPS\), Datasets and Benchmarks Track*\.
- Felli et al\. \(2023\)Felli, P\.; Montali, M\.; Patrizi, F\.; and Winkler, S\. 2023\.Monitoring Arithmetic Temporal Properties on Finite Traces\.In*Proc\. AAAI Conference on Artificial Intelligence \(AAAI\)*, 6346–6354\. AAAI Press\.
- Geatti, Gianola, and Gigante \(2022\)Geatti, L\.; Gianola, A\.; and Gigante, N\. 2022\.Linear Temporal Logic Modulo Theories over Finite Traces\.In*Proc\. International Joint Conference on Artificial Intelligence \(IJCAI\)*, 2641–2647\. ijcai\.org\.
- Ielo et al\. \(2026\)Ielo, A\.; Mazzotta, G\.; Peñaloza, R\.; and Ricca, F\. 2026\.Enumerating Minimal Unsatisfiable Cores of LTLf Formulae\.In*Proc\. AAAI Conference on Artificial Intelligence \(AAAI\)*, 19160–19168\. AAAI Press\.
- Inan et al\. \(2023\)Inan, H\.; Upasani, K\.; Chi, J\.; Rungta, R\.; et al\. 2023\.Llama Guard: LLM\-based Input\-Output Safeguard for Human\-AI Conversations\.ArXiv preprint arXiv:2312\.06674\.
- Jimenez et al\. \(2024\)Jimenez, C\. E\.; Yang, J\.; Wettig, A\.; Yao, S\.; et al\. 2024\.SWE\-bench: Can Language Models Resolve Real\-World GitHub Issues?In*Proc\. International Conference on Learning Representations \(ICLR\)*\.
- Kamath et al\. \(2025\)Kamath, A\.; Zhang, S\.; Xu, C\.; Ugare, S\.; et al\. 2025\.Enforcing Temporal Constraints for LLM Agents\.ArXiv preprint arXiv:2512\.23738\.
- Leucker and Schallhart \(2009\)Leucker, M\.; and Schallhart, C\. 2009\.A Brief Account of Runtime Verification\.*The Journal of Logic and Algebraic Programming*, 78\(5\): 293–303\.
- Li et al\. \(2025\)Li, Z\.; Huang, S\.; Wang, J\.; Zhang, N\.; et al\. 2025\.SOPBench: Evaluating Language Agents at Following Standard Operating Procedures and Constraints\.ArXiv preprint arXiv:2503\.08669\.
- Liu et al\. \(2023\)Liu, J\. X\.; Yang, Z\.; Idrees, I\.; Liang, S\.; et al\. 2023\.Grounding Complex Natural Language Commands for Temporal Tasks in Unseen Environments\.In*Proc\. Conference on Robot Learning \(CoRL\)*\.System name “Lang2LTL”\.
- Luo et al\. \(2025\)Luo, H\.; Dai, S\.; Ni, C\.; Li, X\.; et al\. 2025\.AgentAuditor: Human\-Level Safety and Security Evaluation for LLM Agents\.In*Proc\. Conference on Neural Information Processing Systems \(NeurIPS\)*\.
- Miculicich et al\. \(2025\)Miculicich, L\.; Parmar, M\.; Palangi, H\.; Dvijotham, K\. D\.; et al\. 2025\.VeriGuard: Enhancing LLM Agent Safety via Verified Code Generation\.ArXiv preprint arXiv:2510\.05156\.
- Nous Research \(2026\)Nous Research\. 2026\.Hermes Agent: A Self\-Improving Open\-Source Agent Framework\.Open\-source software\.
- Nuzzo et al\. \(2018\)Nuzzo, P\.; Lora, M\.; Feldman, Y\. A\.; and Sangiovanni\-Vincentelli, A\. L\. 2018\.CHASE: Contract\-based requirement engineering for cyber\-physical system design\.In*Proc\. Design, Automation & Test in Europe Conference \(DATE\)*, 839–844\.
- Nuzzo et al\. \(2015\)Nuzzo, P\.; Sangiovanni\-Vincentelli, A\. L\.; Bresolin, D\.; Geretti, L\.; et al\. 2015\.A Platform\-Based Design Methodology with Contracts and Related Tools for the Design of Cyber\-Physical Systems\.*Proceedings of the IEEE*, 103\(11\): 2104–2132\.
- OpenClaw Project \(2026\)OpenClaw Project\. 2026\.OpenClaw: An Open\-Source Personal AI Agent\.Open\-source software\.
- Palumbo et al\. \(2026\)Palumbo, N\.; Choudhary, S\.; Choi, J\.; Amir, G\.; et al\. 2026\.Formal Policy Enforcement for Real\-World Agentic Systems\.ArXiv preprint arXiv:2602\.16708\.
- Pnueli \(1977\)Pnueli, A\. 1977\.The Temporal Logic of Programs\.In*Proc\. Annual Symposium on Foundations of Computer Science \(FOCS\)*, 46–57\. IEEE\.
- Roşu and Havelund \(2005\)Roşu, G\.; and Havelund, K\. 2005\.Rewriting\-Based Techniques for Runtime Verification\.*Automated Software Engineering*, 12\(2\): 151–197\.
- Roveri et al\. \(2024\)Roveri, M\.; Di Ciccio, C\.; Di Francescomarino, C\.; and Ghidini, C\. 2024\.Computing Unsatisfiable Cores for LTLf Specifications\.*Journal of Artificial Intelligence Research*, 80: 517–558\.
- Schneider \(2000\)Schneider, F\. B\. 2000\.Enforceable Security Policies\.*ACM Transactions on Information and System Security \(TISSEC\)*, 3\(1\): 30–50\.
- Sharma, Barke, and Zorn \(2026\)Sharma, R\. K\.; Barke, S\.; and Zorn, B\. 2026\.Willful Disobedience: Automatically Detecting Failures in Agentic Traces\.In*Proc\. ACM Conference on AI and Agentic Systems \(CAIS\)*\.
- Shi et al\. \(2025\)Shi, T\.; He, J\.; Wang, Z\.; Li, H\.; et al\. 2025\.Progent: Securing AI Agents with Privilege Control\.ArXiv preprint arXiv:2504\.11703\.
- Sotiropoulos et al\. \(2025\)Sotiropoulos, J\.; Del Rosario, R\. F\.; Kokuykin, E\.; Oakley, H\.; et al\. 2025\.OWASP Top 10 for LLM Apps & Gen AI Agentic Security Initiative\.OWASP Foundation\.
- Wang et al\. \(2023\)Wang, B\.; Wang, Z\.; Wang, X\.; Cao, Y\.; et al\. 2023\.Grammar Prompting for Domain\-Specific Language Generation with Large Language Models\.In*Proc\. Conference on Neural Information Processing Systems \(NeurIPS\)*\.
- Wang, Poskitt, and Sun \(2026\)Wang, H\.; Poskitt, C\. M\.; and Sun, J\. 2026\.AgentSpec: Customizable Runtime Enforcement for Safe and Reliable LLM Agents\.In*Proc\. IEEE/ACM International Conference on Software Engineering \(ICSE\)*\.
- Wang et al\. \(2025\)Wang, H\.; Poskitt, C\. M\.; Wei, J\.; and Sun, J\. 2025\.ProbGuard: Proactive Runtime Monitoring for LLM Agent Safety via Probabilistic Prediction\.ArXiv preprint arXiv:2508\.00500\.
- Wen et al\. \(2026\)Wen, X\.; Mo, W\. J\.; Xie, Y\.; Qi, P\.; et al\. 2026\.Learning Efficient Guardrails for Compliance\.In*Proc\. International Conference on Machine Learning \(ICML\)*\.
- Wu et al\. \(2024\)Wu, Q\.; Bansal, G\.; Zhang, J\.; Wu, Y\.; et al\. 2024\.AutoGen: Enabling Next\-Gen LLM Applications via Multi\-Agent Conversation\.In*Proc\. Conference on Language Modeling \(COLM\)*\.
- Xiao et al\. \(2026\)Xiao, Y\.; Lutz, C\. D\.; Castillo\-Effen, M\.; and Nuzzo, P\. 2026\.Contract\-Based Consistency and Availability Analysis for Distributed Cyber\-Physical Systems\.In*Proc\. ACM/IEEE International Conference on Formal Methods and Models for System Design \(MEMOCODE\)*\.To appear\.
- Xiao and Nuzzo \(2026\)Xiao, Y\.; and Nuzzo, P\. 2026\.Contract\-Based Architecture Exploration of Cyber\-Physical Systems via Satisfiability Modulo Convex Programming\.In*Proc\. Design, Automation & Test in Europe Conference \(DATE\)*, 1–7\. IEEE\.
- Xiao et al\. \(2024\)Xiao, Y\.; Oh, C\.; Lora, M\.; and Nuzzo, P\. 2024\.Efficient Exploration of Cyber\-Physical System Architectures Using Contracts and Subgraph Isomorphism\.In*Proc\. Design, Automation & Test in Europe Conference \(DATE\)*\.
- Xu et al\. \(2026\)Xu, H\.; Li, C\.; Ma, X\.; Ou, X\.; et al\. 2026\.The Evolution of Tool Use in LLM Agents: From Single\-Tool Call to Multi\-Tool Orchestration\.ArXiv preprint arXiv:2603\.22862\.
- Yang et al\. \(2024\)Yang, Z\.; Raman, S\. S\.; Shah, A\.; and Tellex, S\. 2024\.Plug in the Safety Chip: Enforcing Constraints for LLM\-driven Robot Agents\.In*Proc\. IEEE International Conference on Robotics and Automation \(ICRA\)*\.
- Yao et al\. \(2023\)Yao, S\.; Zhao, J\.; Yu, D\.; Du, N\.; et al\. 2023\.ReAct: Synergizing Reasoning and Acting in Language Models\.In*Proc\. International Conference on Learning Representations \(ICLR\)*\.
- Yuan et al\. \(2024\)Yuan, T\.; He, Z\.; Dong, L\.; Wang, Y\.; et al\. 2024\.R\-Judge: Benchmarking Safety Risk Awareness for LLM Agents\.In*Proc\. Findings of the Association for Computational Linguistics: EMNLP*\.
- Zheng et al\. \(2023\)Zheng, L\.; Chiang, W\.\-L\.; Sheng, Y\.; Zhuang, S\.; et al\. 2023\.Judging LLM\-as\-a\-Judge with MT\-Bench and Chatbot Arena\.In*Proc\. Conference on Neural Information Processing Systems \(NeurIPS\), Datasets and Benchmarks Track*\.
- Zhong et al\. \(2025\)Zhong, P\. Y\.; Chen, S\.; Wang, R\.; McCall, M\.; et al\. 2025\.RTBAS: Defending LLM Agents Against Prompt Injection and Privacy Leakage\.ArXiv preprint arXiv:2502\.08966\.
- Zhou et al\. \(2024\)Zhou, S\.; Xu, F\. F\.; Zhu, H\.; Zhou, X\.; et al\. 2024\.WebArena: A Realistic Web Environment for Building Autonomous Agents\.In*Proc\. International Conference on Learning Representations \(ICLR\)*\.

## Appendix AFull Interaction\-Predicate Catalogue

Table[4](https://arxiv.org/html/2609.18128#A1.T4)lists the complete interaction\-predicate vocabulary of𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}\. The main text \(Table[1](https://arxiv.org/html/2609.18128#S4.T1)\) shows the representative subset that the examples and experiments use; the remaining predicates extend the same two families to model outputs, response lengths, and delegation depth\.𝖲𝗂𝗇𝖼𝖾⁡\(e\)\\mathsf\{Since\}\(e\)reads a wall\-clock timestamp the framework records with each event; time is an implementation\-level extension and does not enter the formal model of Def\.[1](https://arxiv.org/html/2609.18128#Thmmydefinition1)\.

Table 4:Complete interaction\-predicate vocabulary of𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}\.TTis a tool,ffan argument field,ppa regular\-expression or literal\-value pattern,PPa path or permission set,SSa value set,s,ds,dargument or result fields as source and sink, andk,vk,va context key/value\.
## Appendix BTemporal Expressiveness

Table[5](https://arxiv.org/html/2609.18128#A2.T5)lists four temporal property classes that distinguish𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}’s trajectory\-level enforcement from a stateless, single\-call guard \(§[4](https://arxiv.org/html/2609.18128#S4)\)\. For each we construct a minimal violating trace in which*every individual call is locally legitimate*\(the same calls occur in a compliant trace\), so the violation is purely temporal\.𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}’sDFAcatches all four and raises no false positive on the compliant control; a stateless guard catches none by construction\. The fourth class, “after reading untrusted content, a side\-effecting send requires reconfirmation,” is exactly the indirect\-prompt\-injection contract that drives the AgentDojo and R\-Judge results \(§[6\.2](https://arxiv.org/html/2609.18128#S6.SS2), §[6\.3](https://arxiv.org/html/2609.18128#S6.SS3)\)\.

Table 5:Temporal expressiveness: each violating trace’s every call is individually legitimate, so the violation is detectable only from order, history, or count\. A stateless guard catches none;𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}’sDFAcatches all four, clean on the compliant control\. Tool names in the formulas are abbreviated per row\.
## Appendix CPer\-Model Violation Profiles and Grounding Ablation

This appendix expands the grounding and per\-model robustness summary in §[6\.1](https://arxiv.org/html/2609.18128#S6.SS1.SSS0.Px1)\.

#### The residual gap is coverage, not grounding\.

SOPBench’s decisive predicates are*structural*\(a tool was called, a call returned success\), read directly off the trace, so grounding is exact by construction\. We confirm this with an oracle ablation over5,4355\{,\}435recorded unsafe traces: perfecting the single most influentialAP, the goal action’s success flag, moves pooled detection recall from75\.1%75\.1\\%to75\.4%75\.4\\%\(a\+0\.3\+0\.3ppdelta\)\. There is essentially no grounding error to remove; the residual∼25%\\sim\\\!25\\%is contract*coverage*\(§[6\.1](https://arxiv.org/html/2609.18128#S6.SS1.SSS0.Px1)\)\. Oracle grounding thus matters for content and semantic sensors \(e\.g\., R\-Judge’s semantic residual cases, §[6\.3](https://arxiv.org/html/2609.18128#S6.SS3)\), not for structural enforcement\.

#### Per\-model violation profiles\.

Table[6](https://arxiv.org/html/2609.18128#A3.T6)profiles the contract library across base models on their recorded traces\. The violation*rate*tracks capability: the strongest models almost never complete a forbidden action \(gpt\-5:1414unsafe traces in the sample; o1:33\), whereas mid\-tier models do so routinely \(Claude\-3\.5:417417\), a direct, model\-specific “willful\-disobedience” measure\.𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}’s behaviour on those violations stays stable regardless: recall sits in the54\.754\.7–100%100\\%band and the dominant family of caught violations is value/threshold for every model \(7474–100%100\\%of its catches\), at<1%<\\\!1\\%false positives, so the supervision behavior does not depend on the backbone model\.

Table 6:Per\-model violation profiles on SOPBench recorded traces \(deterministic,00LLMcalls; all2323base models\)\.recall= unsafe caught,FPR= safe wrongly blocked,nuns= sampled unsafe traces\. FPR stays below1%1\\%for1919of2323backbones \(max4\.5%4\.5\\%, llama3\.1\-8b\)\.

## Appendix DSOPBench Live Enforcement: Per\-Constraint Scaling and Robustness

Table[7](https://arxiv.org/html/2609.18128#A4.T7)gives the exact per\-bin values plotted in Figure[4](https://arxiv.org/html/2609.18128#S6.F4): SOPBench success \(on permitted tasks\) and safety \(on forbidden tasks\) as a function of the number of SOP constraints, pooled over the seven domains, for the base, prompt,LLM\-guard, and𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}\-enforce conditions ongemini\-2\.5\-flash\.𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}is the only condition that stays high on*both*axes across the whole range: prompt’s success collapses from87%87\\%to18%18\\%as the policy grows, and the unguarded base’s safety collapses from79%79\\%to0%0\\%, while𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}\-enforce holds success≥77%\\geq\\\!77\\%and safety≥89%\\geq\\\!89\\%throughout, with its safety matching or exceeding prompt at every bin\.

Table 7:Exact per\-bin values for Figure[4](https://arxiv.org/html/2609.18128#S6.F4): SOPBench success \(permitted\) and safety \(forbidden\) % vs\. SOP constraint count, pooled over the seven domains \(gemini\-2\.5\-flash\)\. As the policy grows, prompt’s success and base’s safety both collapse;𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}\-enforce stays high on both axes\.#### Robustness to a weaker base model\.

The weak\-model result in §[6\.1](https://arxiv.org/html/2609.18128#S6.SS1.SSS0.Px1)reports the mean over domains; the effect is consistent across domains\. On the weakergemini\-2\.5\-flash\-liteagent, prompt’s mean safety falls from94%94\\%to45%45\\%\(the agent stops reliably reading and obeying the prompted SOP\), whereas𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}\-enforce reproduces its strong\-model safety \(98%98\\%, unchanged\) because the monitor verdict is computed deterministically from the trace, not inferred by the agent\. Success drops for every condition under the weaker agent \(enforce mean→6890\\\!\\to\\\!68\), confirming that success tracks model capability while𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}’s safety does not\. This confirms the distinction between deterministic and probabilistic supervision\. A prompted SOP’s assurance degrades with the model that carries it, whereas a compiled contract’s does not\.

## Appendix EHot\-Path Latency Breakdown

Table[8](https://arxiv.org/html/2609.18128#A5.T8)gives the per\-workload before\-call latency of the online verifier\.

Table 8:Hot\-path before\-call latency \(ms\) on the incremental online verifier \(O⁡\(\|𝒞\|\)O\(\|\\mathcal\{C\}\|\)per call\)\.Cis the number of contracts evaluated\.
## Appendix FPer\-Cellτ2\\tau^\{2\}\-bench Reliability Matrix

Figure[6](https://arxiv.org/html/2609.18128#S6.F6)plots thepass4andjoint4endpoints of theτ2\\tau^\{2\}\-bench reliability matrix\. Table[9](https://arxiv.org/html/2609.18128#A6.T9)gives the exact per\-cell values, including the intermediateproc\-clean4column \(all four retries had zero𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}rule fires\)\.pass4is the native outcome metric,joint4requires both outcome and procedure\-clean on every retry, and thepass4\-to\-joint4gap quantifies the loss of procedural reliability\.

Table 9:τ2\\tau^\{2\}\-bench task\-level reliability \(k=4k=4, percentages\)\.pass4is the native outcome metric \(all four retries reach the correct final state\);proc\-clean4requires zero𝖢𝗈𝗇𝗍𝗋𝖠𝗀𝖾𝗇𝗍\{\\mathsf\{ContrAgent\}\}rule fires on all four retries;joint4requires both\. Claude 3\.7 reachesproc\-clean4=0%\{\}^\{4\}=0\\%in every domain, so itsjoint4is 0% despite a 25 to 60% outcomepass4\.