Deterministic Runtime Enforcement: The Execution Authority for Autonomous AI Agents

Abstract

Autonomous AI agents now hold execution authority over high-consequence enterprise actions in finance, healthcare, and infrastructure, where catastrophic failures are rare yet dominate systemic risk and probabilistic content filtering does not constitute a reference monitor over what is executed. This paper introduces L-DREA, a deterministic runtime-enforcement architecture that generalizes Anderson’s 1972 reference-monitor primitive from mediation of data access to mediation of externally effective action. L-DREA separates capability generation from execution authority, binds every candidate action to an epoch-keyed Permit-to-Act token, and interlocks externalization through a commit-before-actuate substrate. Five structural properties generalize Anderson’s primitive — complete mediation, tamper-resistance, verifiability, non-compensatory aggregation, and epistemic bounding — and six runtime invariants are established analytically, the first additionally mechanized in TLA+ with a released TLC log. A software (Tier-S) reference implementation is evaluated on two disjoint evidence tracks: a seeded synthetic corpus of 1,217,906 runtime proposals (360,000 adversarial), and the public ULB credit-card dataset (284,807 transactions) as a golden-oracle authorization trace, plus a blind committed-before-label-reveal protocol on three public datasets. Across both tracks, a 120,000-attempt full-knowledge adaptive attacker, 2,394 injected runtime attacks, live revocation and watchdog suites, and an executed offline AgentDojo run, zero unauthorized externalizations were observed; exact one-sided Clopper–Pearson and Wilson upper bounds accompany every zero-event claim, with replay determinism of 100.0000% over 1,217,906 cycles and 24,912 Ed25519-signed permit tokens runtime-verified at 100% integrity. All results are bounded to the documented threat surface and released as a seeded, one-command reproducible artifact; hardware substrates and HSM key custody are specified, not claimed.