Agent Behavioral Contracts: Formal Specification and Runtime Enforcement for Reliable Autonomous AI Agents

agent 2602.22302
behavioral-contractverificationdrift-detectionjsd-thresholdagent-safety

§1 TL;DR #

Agent Behavioral Contracts (ABC) brings Design-by-Contract to AI agents: a six-tuple $(\mathcal{P}, \mathcal{I}_{\text{hard}}, \mathcal{I}_{\text{soft}}, \mathcal{G}_{\text{hard}}, \mathcal{G}_{\text{soft}}, \mathcal{R})$ with probabilistic $(p,\delta,k)$-satisfaction, Ornstein–Uhlenbeck drift bounds ($D^* = \alpha/\gamma$), compositionality for multi-agent chains, and <10 ms enforcement overhead across 1,980 sessions.

§2 Q1 / Q2 / Q3 #

Q1 痛点 #

AI agents operate on natural-language prompts with no formal behavioral specification. Training-time alignment (Constitutional AI, RLHF) shapes general tendencies but cannot enforce deployment-specific invariants. Output-filtering guardrails (NeMo, Guardrails AI) lack session-level state, drift detection, and composability. Wang et al. (2026a) prove the self-evolution trilemma: passive safety is provably insufficient without external intervention. The result: behavioral drift manifests silently over multi-turn interactions until harm occurs.

Q2 方法 #

Contract structure: $\mathcal{C} = (\mathcal{P}, \mathcal{I}_{\text{hard}}, \mathcal{I}_{\text{soft}}, \mathcal{G}_{\text{hard}}, \mathcal{G}_{\text{soft}}, \mathcal{R})$ where hard constraints are safety properties ("bad never happens") and soft constraints with bounded recovery window $k$ encode bounded liveness ("good eventually happens within $k$ steps").

$(p,\delta,k)$-satisfaction: Probabilistic compliance for stochastic LLM agents. Hard guarantee: $\mathbb{P}[C_{\text{hard}}(t) = 1 \;\forall t] \geq p$. Soft guarantee: violations must recover within $k$ steps with probability $\geq p$. Recovery transforms exponential compliance decay ($q^T$) to linear decay ($1 - T(1-q)(1-r)$).

Drift dynamics: Modeled as Ornstein–Uhlenbeck process: $dD(t) = (\alpha - \gamma D(t))dt + \sigma dW(t)$. Stationary distribution $\mathcal{N}(\alpha/\gamma, \sigma^2/(2\gamma))$. The drift score combines compliance drift (lagging indicator) with JSD distributional drift (leading indicator): $D(t) = w_c \cdot D_{\text{compliance}}(t) + w_d \cdot \mathrm{JSD}(P_{\text{obs}}(t) \| P_{\text{ref}})$.

Contract design criterion: To ensure $\mathbb{P}(D > D_{\max}) \leq \varepsilon$: $\gamma \geq \alpha/D_{\max} + \sigma\sqrt{2\ln(1/\varepsilon)}/(2D_{\max})$.

Compositionality: For serial chain $A \to B$, composed contract preserves safety under four conditions (C1–C4). Reliability degrades multiplicatively ($p_{\text{chain}} \geq \prod p_i \cdot \prod p_{h_i}$), drift accumulates additively ($\delta_{\text{chain}} \leq \sum \delta_i + \sum \delta_{h_i}$).

核心技术壁垒: The JSD-based distributional drift component serves as a leading indicator — detecting behavioral shifts before they manifest as constraint violations. This is qualitatively different from all prior approaches that can only detect violations after they occur.

Q3 结果 #

MetricValue
Soft violations surfaced per session (contracted vs uncontracted)5.2–6.8 vs 0.0–0.3
Cohen's $d$ for violation detection6.7–33.8 (all $p < 0.0001$)
Hard constraint compliance88–100%
Mean behavioral drift $\bar{D}$0.073–0.154
Max drift $D_{\max}$0.264 (Mistral, 12-turn)
Recovery rate (frontier models)100%
Enforcement overhead<10 ms per action
Models evaluated7 (6 vendors), 1,980 sessions
Total experimental cost$3.09

§3 架构 / 方法图 #

stateDiagram-v2 [*] --> CheckPreconditions: session start CheckPreconditions --> ActionLoop: P(s₀) = true state ActionLoop { AgentAction --> EvalConstraints EvalConstraints --> UpdateDrift: compute C_hard, C_soft, D(t) UpdateDrift --> CheckThresholds CheckThresholds --> RecoveryMechanism: soft violation CheckThresholds --> BlockAction: hard violation CheckThresholds --> Continue: compliant RecoveryMechanism --> AgentAction: re-prompt within k steps Continue --> AgentAction }

The enforcement loop evaluates all constraints per action, updates compliance/drift metrics, and triggers recovery for soft violations within the bounded recovery window.

§4 作者证明 #

The paper provides formal proofs for all core theorems:

CheckStatusLocation
Drift bounds via Lyapunov/Itô calculusProven (Theorem 4.3)§4.2, Appendix A.1
Recovery linearizes decay (Lemma 3.10)Proven§3.4, Appendix A.2
Compositionality theorem (Theorem 4.9)Proven§4.3, Appendix A.3
Probabilistic compositionality (Theorem 4.11)Proven§4.3, Appendix A.4
SPRT certification efficiencyProven (Proposition A.14)Appendix A.5
Runtime complexity $\mathcal{O}(k +\mathcal{A})$Proven (Proposition 4.15)§4.4

OU stationary distribution existence proven via Foster–Lyapunov criterion; uniqueness via ergodicity; Gaussian tail bound from the stationary $\mathcal{N}(\alpha/\gamma, \sigma^2/(2\gamma))$.

§5 实验与数据 #

E1 Transparency Effect (Table 9–10): Contracted agents show lower soft compliance than uncontracted — not regression, but visibility. All 7 models exhibit 5.2–6.8 additional soft violations per session detected by contracts ($p < 0.0001$, Cohen's $d = 6.7$–$33.8$).

E2 Drift Prevention (Table 11): 12-turn sessions. Drift trajectory fits OU mean-reversion (R² = 0.49–0.75). Maximum $D_{\max} = 0.264$ (Mistral), well below alert threshold. Recovery: 100% for GPT-5.2 and Claude Opus; 17% for Mistral Large 3.

E3 Adversarial Stress (Table 12): Hard compliance never drops below 0.911 under prompt injection, conflicting instructions, and social engineering. GPT-5.2 maintains $C_{\text{hard}} = 1.000$ across all stress types.

E4 Ablation (Table 13): Recovery + soft constraints are dominant $\Theta$ contributors (removing either causes $\Delta\Theta \approx -0.2$). The "$\Theta$ paradox": removing measurement components increases the composite score because it eliminates the measurement penalty.

Platform guardrail interference: Azure "DefaultV2" content filter blocks 40–60% of legitimate financial advisory sessions — contracts and platform guardrails operate at complementary abstraction layers.

§6 论证链 #

StepClaimEvidenceDepends on
1AI agents lack formal behavioral specification; passive alignment is provably insufficientWang et al. (2026a) self-evolution trilemma; Cartagena & Teixeira (2026) text≠tool safety
2ABC contract tuple with hard/soft separation formalizes the specification gapDefinition 3.1, mapping to PCTL (Remark 3.9)Step 1
3Recovery transforms exponential to linear compliance decayLemma 3.10, provenStep 2
4OU drift model bounds behavioral deviation with Gaussian concentrationTheorem 4.3, full proof via Itô/Lyapunov/Foster–LyapunovSteps 2, 3
5Contracts compose for multi-agent chains with quantified degradationTheorem 4.9, 4.11 (C1–C4 conditions)Step 4
6Transparency effect: contracts make violations measurable, not preventableE1: 5.2–6.8 violations surfaced, $d = 6.7$–$33.8$Steps 2, 3
7Drift bounded in practice: $D^* < 0.27$ over extended sessionsE2: OU fit R² = 0.49–0.75Step 4

§7 实现 cross-reference #

AgentAssert: ~3,000 lines of Python, >95% test coverage. ContractSpec DSL (YAML-based, intentionally not Turing-complete). Available as library with 3 API entry points.

[实现未公开] — No public repository URL provided in the paper.

关键实现细节:

  1. Reference distribution calibration — the JSD distributional drift component requires a calibrated baseline $P_{\text{ref}}$ from compliant sessions. No automated tooling exists for calibration or recalibration; in non-stationary deployments this becomes a manual maintenance burden.
  2. Recovery is monitoring by default — out-of-box AgentAssert emits events but does not auto-correct unless the deployer registers a custom recovery handler. The "recovery" mechanism that drives the theoretical $\gamma$ parameter requires explicit implementation per deployment.