
Symbolic Temporal Supervision of LLM Agents Using Contracts
It replaces stochastic post-hoc LLM judges and per-call rule-based blockers with a single deterministic artifact: assume-guarantee contracts in finite-trace LTL, compiled to DFAs that gate tool calls online and evaluate recorded traces offline. The cost is engineering effort, not compute: someone must formalize checkable predicates over tool calls and author and maintain a correct contract library per task domain, plus DFA compilation overhead. It can fail when contracts are incomplete, wrongly specified, or the predicate set cannot observe the relevant state, in which case harmful actions pass deterministically or benign ones are blocked, and coverage does not transfer across domains without rewriting contracts.








































