ContrAgent compiles temporal-logic contracts into one automaton that both gates calls online and grades traces offline.

arXiv 2609.18128 closes the split between LLM judges that score recorded trajectories after the fact and rule engines that block one action at a time. Required behavior goes in as assume-guarantee contracts in LTL over finite traces, compiled to a DFA used for both jobs. It matches state-of-the-art LLM-judge and rule-based baselines across four benchmarks with deterministic reproducible verdicts and orders-of-magnitude lower per-call latency online. The contract library is maintained separately from the agent's model, so it survives a model swap, which is the operational property I'd care about most.