Enforcing Temporal Constraints for LLM Agents

TL;DR

Agent-C tackles the lack of formal temporal guarantees for LLM-based agents by introducing a runtime framework that encodes temporal safety properties in a domain-specific language and enforces them during token generation via SMT-based verification. It supports grammar-constrained generation with backtracking for open models and reprompting for closed models, guaranteeing compliant tool calls and preventing unsafe sequences. Across tau-bench retail and airline tasks and multiple models, Agent-C achieves 100% conformance with 0% harm, often improving task utility while maintaining acceptable overhead. The work demonstrates practical, scalable formal safety for agentic systems, including the ability to generate specifications from natural-language policies to lower adoption barriers.

Abstract

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.

Figures (8)

• Figure 1: We present an example in which a user requests access to their SSN (Social Security Number), a personal identifier. The generic agent sees that it has a tool, get-ssn, and uses it to respond to the user query, inadvertently leaking sensitive information. With Agent-C, the LLM generates the same tool call, but Agent-C finds the tool call to be non-compliant because the specification requires that the auth tool have been called previously. This result is then used to constrain the LLM, resulting in a policy-compliant response.
• Figure 2: Transition semantics for agentic systems
• Figure 3: Transition semantics rules for Agent-C system
• Figure 4: Grammar of tool calls (following JSON syntax)
• Figure 5: Grammar of Agent-C specifications

Theorems & Definitions (25)

• definition 1: Compliance
• Lemma 1: Simplification
• proof
• Theorem 1: Soundness
• proof
• Theorem 2
• definition 2: Configuration Well-Formedness
• Lemma 2
• proof
• Lemma 3