Symbolic Temporal Supervision of LLM Agents Using Contracts

Researchers introduced ContrAgent, a contract-based framework that uses assume-guarantee contracts in linear temporal logic over finite traces (LTLf) to supervise LLM agents, compiling each contract into a deterministic finite automaton (DFA) that both gates agent actions online and evaluates recorded traces offline. In tests on four benchmarks, ContrAgent matched state-of-the-art LLM-judge and rule-based guardrail baselines while producing deterministic, reproducible verdicts and, in online mode, orders-of-magnitude lower per-call latency, according to the arXiv paper 2609.18128v1. The framework's contract library is maintained independently of the agent's model and can be reused across different agents within the same task domain.

arXiv:2609.18128v1 Announce Type: new 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 ContrAgent, a contract-based framework for symbolic temporal supervision of LLM agents. 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 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.