CaMeLoT checks AI agent plans for safety before execution
CaMeLoT: CaMeL orchestrated with Temporal logic for static verification and liveness
Cryptography and SecurityLogic in Computer Science
Summary
Large language model (LLM) agents use tools that can handle sensitive data or commands, so it’s important to ensure their entire plan is safe, not just each step. The authors present CaMeLoT, a system that examines the agent’s plan before any action happens, verifying it against rules expressed in temporal logic. If the plan is unsafe, CaMeLoT rejects it early and provides feedback for correction, saving resources and preventing harmful tool use. They tested CaMeLoT on various benchmarks and confirmed it can verify many safety properties efficiently before execution.
What this means in practice
- •For software security teams: Prevent unsafe AI agent behaviors by verifying multi-step plans for policy compliance before any tool use happens.
- •For automation engineers: Ensure AI-driven workflows access only authorized data and commands by statically checking execution plans ahead of time.
Authors
Elia Nikolaou, Magnus Wiik Eckhoff, Robert Flood, Gudmund Grov, Vasileios Mavroeidis, David Aspinall
Abstract
LLM-based agents generate and execute multi-step plans that invoke external tools which can access private data or execute commands. In this setting, security is a property of the entire execution that a plan creates, not just any single step. The plan itself is a critical artefact that captures the tool calls, control flow, and data dependencies. We present CaMeLoT, a complement to CaMeL, an existing defence against prompt injection in tool-using LLM agents. CaMeLoT extends CaMeL by adding a static verification layer that checks an agent's plan before any tool is invoked. CaMeLoT translates a generated plan into a finite-state transition system, labels it with tool calls, provenance and taint information, and checks it against temporal policies expressed in CTL using the nuXmv model checker. Because verification happens before execution, unsafe plans are rejected without using LLM calls or tool calls, saving tokens that runtime could have cost, as well as the need to unwind changes or teardown temporary sandboxes. When a verification fails, the model checker returns a counterexample to give feedback to the agent to repair the plan. We evaluate CaMeLoT on policies derived from the AgentDojo benchmark, SOC workflows, and prompt-extraction experiments, showing that it verifies a broad class of temporal properties before execution while preserving CaMeL's runtime-checkable coverage.