# Efficient and Sound Probabilistic Verification for AI Agents

arXiv: https://arxiv.org/abs/2606.20510 · HTML: https://mlsanity.com/paper/2606.20510/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 34 of its 60 references that are in the map.
- First posted on arXiv 18 Jun 2026.

## Builds on (most cited first, 30 of 34)

- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [Toolformer: Language Models Can Teach Themselves to Use Tools](https://mlsanity.com/paper/2302.04761/) (2023)
- [Generative Agents: Interactive Simulacra of Human Behavior](https://mlsanity.com/paper/2304.03442/) (2023)
- [SWE-bench: Can Language Models Resolve Real-World GitHub Issues?](https://mlsanity.com/paper/2310.06770/) (2023)
- [Llama Guard: LLM-based Input-Output Safeguard for Human-AI Conversations](https://mlsanity.com/paper/2312.06674/) (2023)
- [Terminal-Bench: Benchmarking Agents on Hard, Realistic Tasks in Command Line Interfaces](https://mlsanity.com/paper/2601.11868/) (2026)
- [InjecAgent: Benchmarking Indirect Prompt Injections in Tool-Integrated Large Language Model Agents](https://mlsanity.com/paper/2403.02691/) (2024)
- [Neural Probabilistic Logic Programming in DeepProbLog](https://mlsanity.com/paper/1907.08194/) (2019)
- [StruQ: Defending Against Prompt Injection with Structured Queries](https://mlsanity.com/paper/2402.06363/) (2024)
- [Agent Security Bench (ASB): Formalizing and Benchmarking Attacks and Defenses in LLM-based Agents](https://mlsanity.com/paper/2410.02644/) (2024)
- [NeMo Guardrails: A Toolkit for Controllable and Safe LLM Applications with Programmable Rails](https://mlsanity.com/paper/2310.10501/) (2023)
- [Defeating Prompt Injections by Design](https://mlsanity.com/paper/2503.18813/) (2025)
- [InterCode: Standardizing and Benchmarking Interactive Coding with Execution Feedback](https://mlsanity.com/paper/2306.14898/) (2023)
- [AgentSpec: Customizable Runtime Enforcement for Safe and Reliable LLM Agents](https://mlsanity.com/paper/2503.18666/) (2025)
- [SecAlign: Defending Against Prompt Injection with Preference Optimization](https://mlsanity.com/paper/2410.05451/) (2024)
- [ShieldAgent: Shielding Agents via Verifiable Safety Policy Reasoning](https://mlsanity.com/paper/2503.22738/) (2025)
- [Progent: Securing AI Agents with Privilege Control](https://mlsanity.com/paper/2504.11703/) (2025)
- [Securing AI Agents with Information-Flow Control](https://mlsanity.com/paper/2505.23643/) (2025)
- [On Prompt-Driven Safeguarding for Large Language Models](https://mlsanity.com/paper/2401.18018/) (2024)
- [NL2Bash: A Corpus and Semantic Parser for Natural Language Interface to the Linux Operating System](https://mlsanity.com/paper/1802.08979/) (2018)
- [System-Level Defense against Indirect Prompt Injection Attacks: An Information Flow Control Perspective](https://mlsanity.com/paper/2409.19091/) (2024)
- [DRIFT: Dynamic Rule-Based Defense with Injection Isolation for Securing LLM Agents](https://mlsanity.com/paper/2506.12104/) (2025)
- [Scallop: A Language for Neurosymbolic Programming](https://mlsanity.com/paper/2304.04812/) (2023)
- [Contextual Agent Security: A Policy for Every Purpose](https://mlsanity.com/paper/2501.17070/) (2025)
- [AgentDoG: A Diagnostic Guardrail Framework for AI Agent Safety and Security](https://mlsanity.com/paper/2601.18491/) (2026)
- [VeriGuard: Enhancing LLM Agent Safety via Verified Code Generation](https://mlsanity.com/paper/2510.05156/) (2025)
- [Formal-LLM: Integrating Formal Language and Natural Language for Controllable LLM-based Agents](https://mlsanity.com/paper/2402.00798/) (2024)
- [Operationalizing Contextual Integrity in Privacy-Conscious Assistants](https://mlsanity.com/paper/2408.02373/) (2024)
- [Enforcing Temporal Constraints for LLM Agents](https://mlsanity.com/paper/2512.23738/) (2025)
- [Formal Policy Enforcement for Real-World Agentic Systems](https://mlsanity.com/paper/2602.16708/) (2026)

## Built on by (most cited first, 2 of 2)

- [ScopeJudge: Cost-Aware Pre-Execution Gating for Offensive Security Agents](https://mlsanity.com/paper/2607.07774/) (2026)
- [Kairos: Transactional Security Enforcement at the System Boundary for LLM Agents](https://mlsanity.com/paper/2610.18457/) (2026)

## Abstract (arXiv)

Securing AI agents that operate in complex digital environments has become a critical need, and runtime monitoring approaches that formulate and enforce policies expressed in a formal language like Datalog offer a promising solution. However, existing approaches are restricted to deterministic policies. In many practical applications of AI agents, there is a need to enforce security policies in the face of ambiguity, leading to probabilistic predicates or state transitions (for example, a declassifier or Personally Identifiable Information (PII) detector that has some failure probability on each invocation). Furthermore, in many such applications, one cannot easily make the independence assumptions necessary to invoke prior work on probabilistic inference in Datalog. We address this by introducing a sound and efficient framework for such verification based on distributionally robust optimization, computing sound upper bounds on the probability of policy violation regardless of possible correlations between predicates. On standard benchmarks for terminal and tool calling agents, we demonstrate that our approach outperforms prior art and improves the security-utility trade-off while ensuring rigorous bounds on the probability of policy violation.