Summary
Ensuring safety for AI agents that use tools is hard because current rules are often specific to one application and don't handle complex, step-by-step processes well. The authors tried using a formal logic method called metric first-order temporal logic (MFOTL) to check AI actions after the fact, without running the AI again. Their tests showed this method can spot many unsafe actions but also sometimes flags safe ones due to missing information in the records. When the data fully captures the history of decisions and approvals, the method works better and can block some tricks used to hide attacks. The authors propose a better data format to improve future safety checks.
What this means in practice
- •For software security teams: Add formal runtime checks to detect multi-step suspicious actions by AI agents using tools when trustworthy historical records are available.
- •For ai platform engineers: Improve audit and safety tools for AI agents by adopting richer trace formats that bind provenance data to action sources, enabling stronger attack detection.
Authors
Nikolaos Kekatos, Stylianos Basagiannis, Marinelio Chintri, Alexios Lekidis, Tom Nianios, Ioannis Seitoglou, Anastasios Temperekidis, Panagiotis Katsaros
Abstract
Guardrails for tool-using LLM agents are usually application-specific rules, which makes multi-step, data-dependent safety policies hard to specify, audit and reuse. As a declarative alternative, we evaluate metric first-order temporal logic (MFOTL), replaying the recorded trajectories that AgentDojo, STAC and R-Judge already ship through the unmodified MonPoly monitor, offline and without running an agent. On these corpora, five generic obligations flag 71.8% of STAC attack chains and 70.1% of successful AgentDojo attacks, but also fire on 29.3% of benign runs. This imprecision stems from the corpora rather than the logic: they rarely record approvals and never record timestamps, so history-dependent obligations reduce to detecting risky action types. Where the trace does carry relational context, provenance-aware policies discriminate better; that context, however, is itself attackable, and one planted line defeats a naive provenance check on 94-99% of the runs it would otherwise flag. Binding provenance to the lookup that produced it closes this evasion at no cost in detection or benign firing. Taken together, these results show that formal temporal monitoring adds value exactly when the trace exposes trustworthy history. We therefore quantify how far current benchmarks are from that point and propose a twelve-field enforcement-ready trace schema.