Large language model (LLM) agents can automate multi‑step tasks such as web navigation, code generation, and workflow orchestration by invoking external tools. However, hallucinations, distributional instability, adversarial manipulations, and the irreversible impact of certain tool calls may produce harmful outcomes. Existing safeguards either grade recorded trajectories post‑hoc with stochastic LLM judges or block unsafe actions one call at a time, lacking a single deterministic artifact that serves both purposes.\
We introduce 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. Required behaviors are specified with assume‑guarantee contracts expressed in linear temporal logic over finite traces (LTLf). Each contract is compiled into a deterministic finite automaton (DFA) that simultaneously gates actions online and evaluates traces offline.\
A contract library, maintained independently of the agent model, acts as a reusable knowledge base and can be applied across different agents within the same task domain. We evaluate the approach on four benchmarks covering both online guarding and offline evaluation. Results show that ContrAgent matches state‑of‑the‑art LLM‑judge and rule‑based guardrail baselines while delivering deterministic, reproducible verdicts and, in online mode, orders‑of‑magnitude lower per‑call latency.\
Review