Controller-Agnostic Runtime Safety Certificates for Tool-Using AI Agents via Data-Driven Robust Reachability

Abstract

Software agents built on large language models act by issuing tool calls, some of which cannot be undone. To control theory the model is an opaque feedback controller, replaced every few months, whose closed loop cannot be analyzed directly. We propose a runtime filter, or shield, between any such controller and its environment that certifies a bound on the probability of reaching an unsafe condition during a bounded task. Given a predicate abstraction and candidate successor sets, everything else comes from logs: the loop becomes a finite controlled Markov chain, the estimated kernel is surrounded by a distribution-free confidence region, and robust reach-avoid value iteration runs over it. The certificate is probably approximately correct and uniform over controllers respecting the filter, so one model may replace another without recomputation. In all tested datasets the true risk stayed within certificate and budget; in a file-system sandbox the filter stays sound against a hazard the logs barely covered, where a plug-in baseline certifies safety and fails; and it holds seven controllers, three of them open-weights models, to zero unsafe outcomes in 1050 episodes.