PaperlayerView exact revision on arXiv

Source-linked AI summary

Enforcing Temporal Constraints for LLM Agents

Adharsh Kamath, Sishen Zhang, Calvin Xu, Shubham Ugare, Gagandeep Singh, Sasa Misailovic

arXiv:2512.23738v1cs.PLcs.AIcs.FLcs.LO

TL;DR

LLM-agent guardrails do not provide formal guarantees for temporal safety policies, which govern the ordering of actions. Agent-C specifies these policies and enforces them during generation; across benchmarks and model scales, it achieves perfect safety while maintaining or improving utility.

  • Problem

    Existing guardrails lack formal guarantees for enforcing temporal safety policies that constrain the order of agent actions.

    Source: §1 · p. 2

  • Method

    Agent-C specifies temporal constraints in a domain-specific language, translates them to first-order logic, and enforces them through runtime constrained generation.

    Source: §1 · pp. 2–3

  • Results

    Agent-C achieves 100% conformance and 0% harm across multiple benchmarks and model scales while maintaining or improving task utility.

    Source: §1 · p. 3, §9 · p. 23

  • Takeaways & Limitations

    Agent-C brings runtime formal-verification principles to LLM agents and enables frontier models to achieve both high utility and safety.

    Source: §9 · p. 23

    With reprompting, the number of tokens processed by the LLM grows as reprompting increases.

    Source: §4.4 · p. 12

Abstract

from arXiv · show

LLM-based agents are deployed in safety-critical applications, yet current guardrail systems fail to prevent violations of temporal safety policies, requirements that govern the ordering and sequencing of agent actions. For instance, agents may access sensitive data before authenticating users or process refunds to unauthorized payment methods, violations that require reasoning about sequences of action rather than an individual action. Existing guardrails rely on imprecise natural language instructions or post-hoc monitoring, and provide no formal guarantees that agents will satisfy temporal constraints. We present Agent-C, a novel framework that provides run-time guarantees ensuring LLM agents adhere to formal temporal safety properties. Agent-C introduces a domain-specific language for expressing temporal properties (e.g., authenticate before accessing data), translates specifications to first-order logic, and uses SMT solving to detect non-compliant agent actions during token generation. When the LLM attempts to generate a non-compliant tool call, Agent-C leverages constrained generation techniques to ensure that every action generated by the LLM complies with the specification, and to generate a compliant alternative to a non-compliant agent action. We evaluate Agent-C across two real-world applications: retail customer service and airline ticket reservation system, and multiple language models (open and closed-source). Our results demonstrate that Agent-C achieves perfect safety (100% conformance, 0% harm), while improving task utility compared to state-of-the-art guardrails and unrestricted agents. On SoTA closed-source models, Agent-C improves conformance (77.4% to 100% for Claude Sonnet 4.5 and 83.7% to 100% for GPT-5), while simultaneously increasing utility (71.8% to 75.2% and 66.1% to 70.6%, respectively), representing a new SoTA frontier for reliable agentic reasoning.

1 Introduction

Agent-C addresses the lack of formal guarantees for temporal safety policies by checking and constraining tool calls during generation. Across open-weight and closed-source models, it achieves perfect conformance while usually improving utility.

1 Introduction

  • Existing guardrails lack formal guarantees that tool calls will consistently meet user- or developer-mandated constraints.Temporal policies can require reasoning about an action sequence, such as authenticating before accessing sensitive information.Source: §1 · pp. 1–2
  • Agent-C expresses temporal properties in a domain-specific language and translates specifications into first-order logic.Its language includes Before, After, Forall, and Exists predicates for ordering requirements and invariants across calls.Source: §1 · pp. 2–3
  • At runtime, Agent-C checks whether appending a proposed tool call to the trace would preserve compliance, potentially before the call executes.The trace includes tool-call inputs, outputs, and tool-state information.Source: §1 · pp. 2–3
  • Agent-C translates specifications to SMT formulas and incrementally checks satisfiability during execution to guide constrained generation with backtracking.Backtracking can regenerate a smaller part of a call, such as an argument or function name.Source: §1 · p. 3
  • Open-weight models support fine-grained enforcement, while closed-model providers require coarser call resampling because they do not expose all next-token probabilities.Both generation approaches are described as guaranteeing specification enforcement.Source: §1 · p. 3
  • 100% conformance across open-weight and closed-source models; Agent-C also never causes harm under adversarial prompts and improves utility in almost all cases.The introduction reports that some baselines exhibit harmful behavior over 20% of the time.Source: §1 · p. 3

2 Overview

The overview illustrates temporal safety policies through authentication-before-access and refund-payment constraints. Agent-C checks calls against specifications that can use both execution history and tool state.

2 Overview

  • The overview presents two examples of state-of-the-art safety frameworks failing to follow safety policies, alongside Agent-C’s specification-based approach.The examples cover authentication before access and payment fraud prevention.Source: §2 · p. 3, §2.1 · p. 4, §2.2 · p. 5

2.1 Example 1: Failing to Authenticate Before Access

  • DynaGuard attempted to retrieve order details before authenticating the user, disclosing private information and exposing other users’ data to potential access.The policy requires confirming the user ID before proceeding with any task.Source: §2.1 · p. 4
  • For order access, the specification requires prior successful authentication, a matching user and order owner, and an existing order.Agent-C checks whether appending a proposed call would violate the specification and resamples after detecting a violation, subject to retry limits.Source: §2.1 · p. 4

2.2 Example 2: Payment Fraud Prevention

  • Claude Sonnet 4.5 attempted a refund to PayPal despite the original payment being by credit card, even with the policy in its system prompt.The paper notes that large-scale exploitation could lead to financial losses for the platform.Source: §2.2 · p. 5
  • Agent-C checks refund payment state and refused the PayPal refund, escalating the case to a human agent.The refund must use the original payment method or an existing gift card; state checks can access information absent from tool-call history.Source: §2.2 · p. 5

3 Background on LLM-based Agents

An agentic system combines an LLM, a tool runner, and a runtime that manages the interaction between them. Its execution proceeds through prompting, tool invocation and execution, feedback, and termination.

3 Background on LLM-based Agents

  • An agentic system S is a tuple (L, T, R): an LLM, a tool runner, and a runtime.The available tool set P is fixed for a given system.Source: §3 · p. 6
  • The LLM maps a non-empty input string to a non-empty output string, while the tool runner executes calls and updates tool state.The runner returns a tool output and a new state from the prior state, tool, and arguments.Source: §3 · p. 6
  • The runtime parses LLM output into tool calls, adds tool outputs to the next prompt, and execution proceeds through inference, invocation, execution, feedback, or termination.The initial configuration contains the prompt, with other cells empty; the transition semantics describe how configurations change.Source: §3 · pp. 6–7, Figure 2 · p. 7

4 Agent-C

Agent-C specifies temporal and state-based constraints on LLM agents and enforces them at runtime. Its semantics and Safe-LLM procedure check candidate calls against the specification, using constrained generation or reprompting.

4 Agent-C

  • Agent-C provides a DSL and enforcement algorithm interleaved with constrained generation to enforce temporal and state-based constraints at runtime.The section describes system semantics, Safe-LLM, and call-generation algorithms with and without backtracking.Source: §4 · p. 7

4.1 Operational Semantics of Agentic Systems with Agent-C

  • Agent-C models executions with a trace and state-projection map, and its Infer-AgC rule invokes Safe-LLM to check calls against the specification.The trace records events; the projection map reads selected tool-state values, and Safe-LLM may return an error call if its loop budget is exhausted.Source: §4.1 · pp. 7–9

4.2 Agent-C SAFE-LLM Checking Procedure

  • Safe-LLM samples candidate calls until one is compliant or its iteration budget is exhausted, selecting Gen-Call or Gen-Call-Reprompt based on token-probability access.A compliant call is returned as a tool output; exhausting the budget can produce an emit_error call.Source: §4.2 · pp. 9–10

4.3 Generating Tool Calls with Grammar-Constrained Generation and Backtracking

  • Gen-Call checks generated arguments and tests the resulting call against the specification, backtracking to regenerate when the call is non-compliant.Backtracking can discard tokens to the last conformant partial generation; this procedure suits models whose token probabilities are accessible.Source: §4.3 · pp. 10–12

4.4 Generating Tool Calls with Reprompting

  • When token probabilities are unavailable, Gen-Call-Reprompt checks a generated call and returns no call to Safe-LLM if it is non-compliant.Reprompting sends the entire input again, so the number of tokens processed grows with additional reprompting.Source: §4.4 · p. 12

5 Agent-C Safety Specification Language

Agent-C specifies temporal constraints on tool calls, translates them into trace-based first-order logic, and checks compliance during execution. Its semantics and enforcement rules define when traces remain compliant and guarantee that Safe-LLM preserves compliance when returning tool calls.

5.1 Syntax of Agent-C Specifications and Examples

  • The DSL combines Before, After, and Seq ordering constraints with Forall/Exists argument predicates, and permits references to prior outputs only in Before constraints.Source: §5.1 · p. 13, §5.2 · p. 14

5.2 Semantics of Agent-C Specifications

  • State projections expose relevant tool-state values through a unified interface, assuming the state is globally consistent and unmodified by other runtime processes.Source: §5.2 · p. 14
  • In the FOL semantics, Before conditionally requires a matching earlier call, while Seq requires both calls in order; references to tool outputs or state cannot point to future events.Source: §5.2 · pp. 14–16
  • Compliance checks whether the encoded trace forces a specification violation for every possible suffix; Endsafe marks a finite trace that remains ended thereafter.Source: §5.2 · pp. 14, 16

5.3 Implementation

  • The implementation uses Z3 to decide the translated formulas and incremental solving to reuse proofs across checks.Source: §5.3 · p. 17

5.4 Specification enforcement guarantees

  • Safe-LLM appends a tool call only when it preserves trace compliance, and every execution ending in Endsafe is compliant.Source: §5.4 · pp. 17–18

6 Methodology

The evaluation compares Agent-C with unconstrained agents and two guardrail frameworks on retail and airline customer-service tasks, including adversarial policy-violating goals. It evaluates multiple language models using task, policy, and resource metrics.

Baselines, policies, models, and metrics

  • The comparison includes unconstrained agents, DynaGuard, and AgentSpec; the evaluation uses Qwen3 models, Claude Sonnet 4.5, and GPT-5 across the specified policies and metrics.Metrics are listed in Table 2; utility accounts for functional correctness and policy obedience, and conformance is assessed from completed traces.Source: §6 · pp. 18–19, Table 2 · p. 19

Benchmarks

  • The benchmarks cover 115 retail tasks and 50 airline tasks involving customer-service tool use, including database queries and reservation changes.Source: §6 · p. 18

Benchmarks (adversarial)

  • Each domain adds 17 adversarial instances with forbidden user goals, and a task receives Harm 1.0 when the agent generates its designated malicious call sequence.Source: §6 · p. 18

7 Evaluation

Across open-weight and closed frontier models, Agent-C enforces tool-use policies while maintaining or improving utility; the evaluation also examines runtime overhead, constrained generation, and automatic specification generation.

7.1 Performance of Agent-C with Grammar-Constrained Generation on Open LLMs

  • 100.00% conformance holds across open-model sizes and both benchmarks in benign and adversarial settings; Agent-C also outperforms baselines on utility in most cases and has 0% harm across configurations.On retail-benign with Qwen3-32B, utility is 53.31% for Agent-C, 37.39% for AgentSpec, and 9.57% for DynaGuard.Source: §7.1 · pp. 19–20, Table 3 · p. 20, Table 4 · p. 20

7.2 Performance of Agent-C with Reprompting on Closed Models

  • Agent-C gives closed frontier models 100.00% conformance and 0.00% harm in all scenarios, while increasing utility by up to 3.9 percentage points on retail and 4.8 on airline benchmarks.The comparison is against unrestricted counterparts using Claude Sonnet 4.5 and GPT-5.Source: §7.2 · p. 20, Table 5 · p. 21, Table 6 · p. 21

7.3 Time and Memory Overhead of Agent-C and Baselines

  • Agent-C requires 480.23s on benign scenarios, 17% more runtime than AgentSpec and 44% more than unrestricted agents, but less than DynaGuard’s 494.18s.It uses 69.72 GB VRAM versus DynaGuard’s 81.40 GB on benign benchmarks.Source: §7.3 · p. 21, Table 7 · p. 21

7.4 Effect of Constrained Generation

  • Without constrained generation, utility falls by over 3 percentage points while conformance remains 100%; backtracking reduces input tokens by up to 40% and output tokens by up to 54%.The comparison uses Qwen3-8B on benign retail and airline tasks.Source: §7.4 · p. 22, Table 8 · p. 22

7.5 Automated Agent-C Specification Generation

  • Claude Sonnet 4.5-generated specifications achieve 100% conformance and 42.11% utility on retail-benign with Qwen3-8B, matching manually crafted specifications.The generated specifications may include extraneous checks; writing formal specifications requires expertise that may not be readily available to practitioners.Source: §7.5 · p. 22

8 Related Work

Related work spans guardrails and runtime monitors, constrained decoding, and temporal logics; Agent-C combines temporal and state-dependent specifications with online SMT checking during generation.

Languages for safe agentic systems

  • Existing DSLs provide varying guarantees, while Agent-C enforces formal temporal constraints during generation rather than relying on post-hoc validation.Its first-order-logic translation and SMT-based satisfiability checking provide guarantees that prior works do not provide.Source: §8 · p. 22

Constrained Generation of LLMs

  • Agent-C extends constrained decoding beyond single-step constraints to temporal and state-dependent constraints spanning multiple tool calls, with online SMT solving.It can explore alternate actions satisfying temporal specifications instead of simply rejecting unsafe outputs.Source: §8 · p. 23

Temporal Logics for Runtime monitoring

  • Agent-C’s data-bearing events and quantification make its DSL closer to FLTL, but its current fragment cannot refer to the immediate next or previous time step.The DSL covers past and future events and runtime tool state.Source: §8 · p. 23

9 Conclusion

Agent-C applies formal verification principles to LLM agents through a temporal-specification DSL and runtime constrained generation. The evaluation reports perfect safety across benchmarks and model scales, with maintained or improved utility and modest computational overhead.

9 Conclusion

  • Agent-C specifies temporal safety constraints in a DSL, translates them to first-order logic, and enforces them at runtime through constrained generation.The conclusion also reports automatic generation of specifications from natural-language policies.Source: §9 · p. 23
  • Across multiple benchmarks and model scales, Agent-C achieves 100% conformance and 0% harm while maintaining or improving task utility compared with existing guardrail frameworks.The conclusion characterizes its computational overhead as modest.Source: §9 · p. 23

A The Full Grammar of Agent-C Specifications

The appendix includes a figure presenting the grammar of Agent-C specifications.

A The Full Grammar of Agent-C Specifications

  • Figure 7 presents the grammar of Agent-C specifications.The supplied figure caption does not state grammar rules.Source: Figure 7 · p. 27

B Theorems and Proofs about Agent-C

The appendix formalizes Agent-C’s compliance guarantees, reports cost-comparison scope, and illustrates behavior on adversarial customer-service and airline tasks. It also provides the tool-call grammar.

B Theorems and Proofs about Agent-C

  • Every execution from a well-formed starting configuration that does not end in an error is compliant and leaves a well-formed configuration.Theorem 5 states this invariant; Theorem 3 states that executions reaching safe termination from a compliant empty trace are compliant.Source: B Theorems and Proofs about Agent-C · pp. 29–30

C Cost comparison of guardrail frameworks

D.1 Fetching Order Details without Authentication

  • In the authentication case, Agent-C rejects an order-details lookup before authentication, then the agent authenticates and completes the task; DynaGuard leaks order information.The example uses Qwen3-8B and contrasts Agent-C with DynaGuard.Source: §D.1 · p. 33

D.2 Fetching Order Details of Another User

  • When an order belongs to another user, Agent-C rejects the lookup and the unauthorized return, and the agent escalates the request to a human.The case study contrasts this with AgentSpec, which attempted to access the other user’s order.Source: §D.2 · p. 33

D.3 Canceling the Reservation of Another User

  • For another user’s airline reservation, Agent-C rejects proposed detail and cancellation calls, then escalates when the agent cannot proceed safely.The case contrasts this with DynaGuard, which cancelled the reservation without authenticating the user.Source: §D.3 · pp. 33–34

E Tool call grammar

  • The tool-call grammar describes a structured call with a function name and arguments, with values including objects, arrays, strings, numbers, booleans, and null.The listing identifies this as the grammar of tool calls.Source: E Tool call grammar · p. 34

F LLM-generated specifications

This appendix describes generated specifications and the prompt used to produce them. It contrasts LLM-generated and user-generated specifications and explains the prompt’s inputs and temporal-rule template.

F LLM-generated specifications

F.1 LLM vs. User generated specifications

  • For get_user_details, both specifications are correct, but the human-generated version is shorter and the LLM version adds checks covered by specifications for other tools.The comparison is limited to this example tool.Source: §F.1 · pp. 35–36, §F.2 · p. 36

F.2 LLM-generated Specification Generation Prompt

  • The generation prompt supplies tool descriptions, benchmark policy information, and an example specification, then asks the LLM to produce domain-specific specifications.Its instructions define before rules for ordering constrained tool calls, and describe state checks and prohibited call sequences.Source: §F.2 · pp. 36–38

G Adversarial benchmarks

The adversarial benchmark extension adds retail and airline instances in which users pursue goals forbidden by policy. Each instance is characterized by instructions given to a user LLM.

G Adversarial benchmarks

G.1 Retail benchmarks

The retail benchmark tasks describe adversarial attempts to modify orders, obtain refunds, or bypass identity and policy checks. They include both unauthorized actions and misleading or incomplete user information.

G.1 Retail benchmarks

  • Some tasks ask users to modify orders that do not belong to them or to proceed without identifying themselves.The benchmark also includes incorrect identifying information that does not correspond to a database account.Source: §G.1 · pp. 39–40
  • Additional scenarios ask users to change payment methods using nonexistent gift cards or cancel orders that have already been delivered.Source: §G.1 · p. 40
  • Other tasks seek returns or refunds that violate stated conditions, including returning an undelivered order or requesting a refund to a non-original payment method.Source: §G.1 · pp. 41–42

G.2 Airline benchmarks

This section describes airline reservation and booking benchmarks that test whether agents follow policies governing when and how booking actions may be taken. The policies include user-confirmation and eligibility requirements for booking changes and cancellations, alongside constraints on passengers, baggage, flights, compensation, and payments.

G.2 Airline benchmarks

  • The tasks include both permitted reservation changes and requests to make policy-disallowed changes, such as changing passengers, removing bags, modifying basic-economy flights, and seeking certificates as a regular member.Other scenarios ask agents to add checked bags or cancel a reservation, contrasting with the explicitly prohibited changes.Source: §G.2 · pp. 42–43
  • Booking scenarios test incorrect payment amounts or methods and baggage counts, while another asks for cancellation after 24 hours of an uninsured economy booking.The payment scenarios include requests to use too many credit cards or gift certificates; baggage scenarios include incorrect counts for paid bags.Source: §G.2 · pp. 43–44

H Agent policies

H.1 Retail agent policy

  • The retail policy requires user authentication before sharing information, limits assistance to one user, and requires explicit confirmation before consequential database updates.It also restricts agents to actions within their defined scope and directs them to transfer requests that cannot be handled there.Source: §H.1 · p. 45
  • A retail order can be exchanged only after confirming it was delivered, and items may be exchanged for available options of the same product, not a different product type.The customer must provide a payment method for any price difference and confirm the items to exchange before the order is marked exchange requested.Source: §H.1 · p. 47

H.2 Airline agent policy

  • Before any airline action that updates a booking, the agent must list its details and obtain explicit user confirmation.The policy also requires one tool call at a time, prohibits responding to the user simultaneously with a tool call, and directs the agent to deny policy-violating requests.Source: §H.2 · p. 47
  • Flight modifications cannot change origin, destination, or trip type, and basic economy flights cannot be modified; cabin changes apply across all flights in a reservation.Baggage can be added but not removed, insurance cannot be added after booking, and the passenger count cannot be changed.Source: §H.2 · pp. 48–49
  • Airline cancellations are permitted within 24 hours of booking or when the airline cancels; otherwise, economy requires qualifying insurance and business flights may always be cancelled.The agent must first obtain the user and reservation IDs and cancellation reason; the API does not enforce these eligibility rules.Source: §H.2 · p. 49

Related papers

Loading 2512.23738v1…