# Alignment Contracts for Agentic Security Systems

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in Agent threats, guardrails and governance, one of 16 directions in LLM agents and tool use.
- Builds on 10 of its 45 references that are in the map.
- First posted on arXiv 30 Apr 2026.

## Placed in

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

## Builds on (most cited first, 10 of 10)

- [Not what you've signed up for: Compromising Real-World LLM-Integrated Applications with Indirect Prompt Injection](https://mlsanity.com/paper/2302.12173/) (2023)
- [InjecAgent: Benchmarking Indirect Prompt Injections in Tool-Integrated Large Language Model Agents](https://mlsanity.com/paper/2403.02691/) (2024)
- [AgentSpec: Customizable Runtime Enforcement for Safe and Reliable LLM Agents](https://mlsanity.com/paper/2503.18666/) (2025)
- [Adaptive Attacks Break Defenses Against Indirect Prompt Injection Attacks on LLM Agents](https://mlsanity.com/paper/2503.00061/) (2025)
- [Firewalls to Secure Dynamic LLM Agentic Networks](https://mlsanity.com/paper/2502.01822/) (2025)
- [Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization (Extended Version)](https://mlsanity.com/paper/2403.04651/) (2024)
- [Enforcing Temporal Constraints for LLM Agents](https://mlsanity.com/paper/2512.23738/) (2025)
- [Multi-Agent Penetration Testing AI for the Web](https://mlsanity.com/paper/2508.20816/) (2025)
- [AgentGuard: Runtime Verification of AI Agents](https://mlsanity.com/paper/2509.23864/) (2025)
- [EVMbench: Evaluating AI Agents on Smart Contract Security](https://mlsanity.com/paper/2603.04915/) (2026)

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

- [LeaseGuard: Incumbent-Preserving Admission Control for Privileged LLM Agents](https://mlsanity.com/paper/2609.24077/) (2026)

## Abstract (arXiv)

Agentic security systems increasingly combine LLM planners with tools that can discover, validate, and report vulnerabilities. This creates an asymmetric control problem: the system should retain strong offensive capability inside an authorized engagement, while the same capabilities must be denied outside scope. Existing guardrails provide useful policy controls, but they do not make this boundary a first-class formal contract over observable effects. We introduce alignment contracts, a framework for specifying and enforcing behavioral constraints over observable effect traces. A contract defines scope, allowed and forbidden effects, resource budgets, and disclosure policies. We give the language finite-trace semantics, characterize satisfaction as a safety property with finite violation witnesses, develop refinement and one-way composition rules for modular contract engineering, and show that admissibility checking is decidable. We instantiate the framework for web-focused agentic security workflows and show how the same structure extends to other effect profiles. Under an explicit Effect Observability Assumption, where all SigmaEff-effects are mediated, the soundness theorem quantifies over the agent model and gives guarantees for mediated SigmaEff-effects, including enforcement soundness for monitor-realized traces. We also state an assumption-lifted adaptation result and formalize limits through undecidability transfer and observability-boundary theorems. A Lean 4 artifact checks the formal core theorems used by the paper.