Researchers have built a tool that grades AI agents on how they work, not just what they produce.
The paper introduces AgentLTL, a specification language derived from First-Order Linear Temporal Logic. It lets developers write procedural rules — things like "always verify inputs before calling this tool" or "never skip step three" — and then score an agent's action trace against those rules automatically. No LLM judge needed; the compliance score is deterministic. The same specification can either block rule-violating tool calls in real time or serve as a reward signal during fine-tuning. On a benchmark covering ordering, branching, iteration, and grounding tasks, the block-and-warn mode improved compliance on five of seven tested models. Fine-tuning with the compliance score as a dense reward produced gains of 38 and 17.5 percentage points in accuracy and compliance on held-out patterns, including tool names the model had never seen before.
Most agent evaluation today stops at the finish line: did the model return the right answer? In safety-critical domains — medical triage, financial workflows, legal research — the sequence of steps matters as much as the outcome. AgentLTL offers a way to enforce and measure that sequence without trusting a second language model to referee the first one. The generalization to unseen tool aliases is a quietly important result; it suggests models trained this way internalize the procedure rather than memorizing specific tool names.
Formal verification has a long history of being theoretically elegant and practically underused. Whether AI teams adopt a logic-derived compliance layer depends on how painful it is to write those specs — a question this paper does not fully answer.