Efficient and Sound Probabilistic Verification for AI Agents

Runtime monitoring using formal policy languages like Datalog offers a promising framework for securing AI agents. However, existing methods are restricted to deterministic policies and cannot handle real-world ambiguities, such as probabilistic state transitions or noisy classifiers (e.g., PII detectors). Moreover, standard probabilistic Datalog inference relies on unrealistic input independence assumptions. To address this limitation, we propose a sound and efficient verification framework based on distributionally robust optimization. Our approach computes guaranteed upper bounds on the probability of policy violation under arbitrary input correlations. Evaluations on standard benchmarks for terminal and tool-calling agents show that our framework outperforms prior art, significantly improving the security-utility trade-off while maintaining rigorous safety guarantees.