AI agents that can send emails, write code, or click checkout need a leash that doesn't argue back.
A paper posted to arXiv (2609.18128) presents ContrAgent, a framework that turns required agent behavior into contracts written in linear temporal logic, then compiles each one into a deterministic finite state machine. That machine can run two jobs: watch an agent live and block a bad tool call before it fires, or replay a finished session log and grade it after the fact. The same contract library works across different agents doing the same task, so switching models doesn't mean rewriting the rules. Across four benchmarks, ContrAgent matched the accuracy of both LLM-judge scoring and existing rule-based guardrails.
The real gain is speed and repeatability, not the safety catch itself. Because each check is a table lookup instead of a fresh model call, the paper reports orders-of-magnitude lower latency for live gating, and the verdict comes out identical every time you run it. That is a real gap right now: most agent safety checks are LLM judges scoring transcripts, and LLM judges can disagree with themselves from one run to the next.
Formal verification has kept compilers and chip designs honest for decades. Pointing the same math at chatty, unpredictable AI agents suggests the industry is finally admitting these systems need engineering guardrails, not just better prompts.