ContrAgent compiles LTLf contracts to a DFA that both gates tool calls online and grades recorded traces offline, replacing the stochastic LLM judge

arXiv 2609.18128·medium signalXBlueskyLinkedInCopy link

Existing agent safeguards split into two incompatible artifacts: LLM judges that grade recorded trajectories after the fact, and per-call rule engines that block one action at a time. ContrAgent expresses required behavior as assume-guarantee contracts in linear temporal logic over finite traces, compiles each to a deterministic finite automaton, and uses the same automaton for online gating and offline evaluation. Across four benchmarks it matches 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. The contract library is maintained independently of the agent's model, so it survives a model swap.