# Provably Secure Agent Guardrail

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Agent threats, guardrails and governance, one of 16 directions in LLM agents and tool use.
- Builds on 34 of its 62 references that are in the map.
- First posted on arXiv 28 May 2026.

## Placed in

- LLM agents and tool use / [Agent threats, guardrails and governance](https://mlsanity.com/agents/agent-threats-guardrails-and-governance/)
- LLM safety and security / [Prompt injection and agent security](https://mlsanity.com/safety/prompt-injection-and-agent-security/)

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

- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [ToolLLM: Facilitating Large Language Models to Master 16000+ Real-world APIs](https://mlsanity.com/paper/2307.16789/) (2023)
- [Jailbroken: How Does LLM Safety Training Fail?](https://mlsanity.com/paper/2307.02483/) (2023)
- [Not what you've signed up for: Compromising Real-World LLM-Integrated Applications with Indirect Prompt Injection](https://mlsanity.com/paper/2302.12173/) (2023)
- [Language Models Don't Always Say What They Think: Unfaithful Explanations in Chain-of-Thought Prompting](https://mlsanity.com/paper/2305.04388/) (2023)
- [Program of Thoughts Prompting: Disentangling Computation from Reasoning for Numerical Reasoning Tasks](https://mlsanity.com/paper/2211.12588/) (2022)
- [Large Language Models Cannot Self-Correct Reasoning Yet](https://mlsanity.com/paper/2310.01798/) (2023)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Faith and Fate: Limits of Transformers on Compositionality](https://mlsanity.com/paper/2305.18654/) (2023)
- [AgentHarm: A Benchmark for Measuring Harmfulness of LLM Agents](https://mlsanity.com/paper/2410.09024/) (2024)
- [StruQ: Defending Against Prompt Injection with Structured Queries](https://mlsanity.com/paper/2402.06363/) (2024)
- [ShieldAgent: Shielding Agents via Verifiable Safety Policy Reasoning](https://mlsanity.com/paper/2503.22738/) (2025)
- [Optimization-based Prompt Injection Attack to LLM-as-a-Judge](https://mlsanity.com/paper/2403.17710/) (2024)
- [DataSentinel: A Game-Theoretic Detection of Prompt Injection Attacks](https://mlsanity.com/paper/2504.11358/) (2025)
- [AirGapAgent: Protecting Privacy-Conscious Conversational Agents](https://mlsanity.com/paper/2405.05175/) (2024)
- [One Token to Fool LLM-as-a-Judge](https://mlsanity.com/paper/2507.08794/) (2025)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?](https://mlsanity.com/paper/2310.01831/) (2023)
- [Provably safe systems: the only path to controllable AGI](https://mlsanity.com/paper/2309.01933/) (2023)
- [AgentSentinel: An End-to-End and Real-Time Security Defense Framework for Computer-Use Agents](https://mlsanity.com/paper/2509.07764/) (2025)
- [Uncovering Security Threats and Architecting Defenses in Autonomous Agents: A Case Study of OpenClaw](https://mlsanity.com/paper/2603.12644/) (2026)
- [Logic Jailbreak: Efficiently Unlocking LLM Safety Restrictions Through Formal Logical Expression](https://mlsanity.com/paper/2505.13527/) (2025)
- [Your Agent Is Mine: Measuring Malicious Intermediary Attacks on the LLM Supply Chain](https://mlsanity.com/paper/2604.08407/) (2026)
- [Self-Jailbreaking: Language Models Can Reason Themselves Out of Safety Alignment After Benign Reasoning Training](https://mlsanity.com/paper/2510.20956/) (2025)
- [VerifyThisBench: Generating Code, Specifications, and Proofs All at Once](https://mlsanity.com/paper/2505.19271/) (2025)
- [Agentic JWT: A Secure Delegation Protocol for Autonomous AI Agents](https://mlsanity.com/paper/2509.13597/) (2025)
- [Bridging Natural Language and Formal Specification--Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs](https://mlsanity.com/paper/2512.17334/) (2025)
- [Generating API Parameter Security Rules with LLM for API Misuse Detection](https://mlsanity.com/paper/2409.09288/) (2024)
- [ORFuzz: Fuzzing the "Other Side" of LLM Safety -- Testing Over-Refusal](https://mlsanity.com/paper/2508.11222/) (2025)
- [Automating Agent Hijacking via Structural Template Injection](https://mlsanity.com/paper/2602.16958/) (2026)

## Abstract (arXiv)

As large language models transition from bounded generative engines to agents with expansive execution privileges, AI going out of control precipitates a fundamental crisis in artificial intelligence security. Existing defense architectures heavily rely on empirical semantic guardrails and probabilistic large model adjudicators, mechanisms that fail to provide deterministic security lower bounds when facing complex semantic symbol decoupling attacks. To overcome this empirical semantic guardrail dilemma, this paper proposes a new security paradigm for agents based on the fundamental limitations of logical reasoning. Based on this paradigm, we further introduce an executable Proof-Constrained Action (ePCA) framework with a neural symbolic isolation architecture. This framework abandons semantic trust in natural language, forcing agents to losslessly formalize their intentions into first-order logical mathematical constraints before performing physical operations. Empirical evaluations of macroscopic and microscopic two-dimensional dynamic adversarial systems demonstrate that our formal verification mechanism achieves zero attack success rate and zero false positive rate across the evaluated scenarios, with extremely low computational latency. This research provides a conditional formal foundation under explicit system assumptions and an engineering paradigm for constructing the underlying defense foundation for future intelligent systems.