CaMeLoT: CaMeL orchestrated with Temporal logic for static verification and liveness
Researchers present CaMeLoT, extending CaMeL with CTL model checking that statically rejects unsafe LLM agent plans before any tool executes.
CaMeLoT adds a static verification layer to CaMeL, a runtime defense against prompt injection in tool-using LLM agents. It translates a generated plan into a finite-state transition system, labels it with tool calls, provenance, and taint information, and checks it against CTL temporal policies using the nuXmv model checker before any tool is invoked. Failed checks return counterexamples for plan repair, avoiding LLM calls, tool calls, and sandbox teardown. Evaluation covers policies derived from AgentDojo, SOC workflows, and prompt-extraction experiments.
40