Proof of Execution: Runtime Verification for Governed AI Agent Actions

• URL: http://arxiv.org/abs/2607.05397v1
• Date: Sun, 26 Apr 2026 12:30:54 GMT
• Title: Proof of Execution: Runtime Verification for Governed AI Agent Actions
• Abstract summary: Agent systems increasingly execute rather than advise.<n>We formalize this as runtime proof of execution.<n>PoE binds authorization, effect, history, and replay into a single runtime-checkable object.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Agent systems increasingly execute rather than advise. When an AI agent queries regulated data, invokes effectful tools, and mutates persistent state, correctness is not captured by whether a terminal output looks plausible. The operative questions are whether each step was authorized under a contract, whether the recorded history is tamper-evident, and whether the trajectory can be reconstructed deterministically. We formalize this as runtime proof of execution. An execution is a triple $x = (C, T, R)$: a contract $C$, an Execution Causal Event Stream (ECES) $T$, and a replay context $R$. A well-formedness predicate and five validator-checkable invariants form the PoE validity predicate. Five semantic guarantees describe authorization, path compliance, null effect on deny, history integrity, and replayability. We prove soundness under explicit cryptographic and deployment assumptions: any PPT adversary that produces a PoE-valid execution violating a semantic guarantee yields a signature forgery, a hash collision, or a quantified deployment-failure event. The Prime Execution Model (PEM) separates planning, enforcement, effect, and recordkeeping into distinct authority planes; a lemma reduces trace completeness to Effector-exclusive credentialing. An Execution Attestation Certificate is issued only when PoE = 1. In a single-node TypeScript prototype, PoE adds approximately 2.7 ms on a minimal flow and 4.4% overhead on concurrent batch workloads; a standard eight-event trace compresses to approximately 1.1 KB; injected Gateway-bypass and trace-mutation attacks are rejected. PoE does not replace consensus, TEEs, or zkVMs; it binds authorization, effect, history, and replay into a single runtime-checkable object so that governed execution becomes attestable under contract.

Related papers

• From Intent to Execution Grant: An Execution-Boundary Conformance Profile for High-Risk AI Actions [9.27474112226667]
  EBL-Core decides whether one canonical, fully materialized AI-generated candidate may receive action-scoped execution authority under explicit conditions.<n>It binds, policy non-weakening, evidence handling, deterministic adjudication, verification, and grant lifecycle behavior.<n>Across 100 trials, 32 concurrent Redemption attempts yielded exactly one successful Redemption and protected test effect per trial.
  arXiv  Detail & Related papers  (2026-09-10T14:21:45Z)
• Zero-Knowledge Predicate Proofs Between AI Agents: A Measured, Cross-Protocol Gateway and the Source-Integrity Gap [0.0]
  Multi-agent AI platforms move quickly from staging to production, but the way agents establish trust remains rudimentary.<n>We take provable data minimisation between agents from proposal to running system.<n>A 32-bit threshold predicate proves in 6.2 ms and verifies in 1.0 ms with a 608-byte Bulletproofs proof.
  arXiv  Detail & Related papers  (2026-08-30T23:16:17Z)
• ROPE: Routed Origin Policy Enforcement against Indirect Prompt Injection [61.4148196085256]
  We present ROPE (Routed Origin Policy Enforcement), which is anchored in a structural notion of trust.<n>Our approach admits two provable guarantees: 1) at every step of a trajectory, no value whose only origin is attacker-writable content reaches an origin-guarded parameter, and 2) no rewording of an injection changes an admission decision.
  arXiv  Detail & Related papers  (2026-08-27T01:22:14Z)
• PACE: Policy-Attested Contract Execution for Safe AI Agents in Decentralized Finance [9.22772901752634]
  We present PACE, a transaction-level authorization framework that interposes between an LLM-based agent and on-chain execution.<n> PACE cryptographically bind the approved intent, policy, and simulation report to the exact execution bytes, with replay and expiration protection.<n> PACE achieves a 0.00 unsafe execution rate and 0.00 false-positive rate on benign tasks, compared to 0.80 for the unguarded baseline.
  arXiv  Detail & Related papers  (2026-08-18T00:22:46Z)
• PhyAgentOS: A Self-Evolving Operating System for Embodied Agents with Decoupled Cognitive Planning and Physical Execution [49.776611937968]
  We present PhyAgentOS, a foundation delivering scheduling, verification, memory, benchmarking, and safety as system-level services.<n>Its Session-Centered treats a session, not an action, as the minimum unit of scheduling, compatibility, supervised execution, evidence collection, and acceptance.<n>SessionVerifier distinguishes execution termination from semantic task completion via evidence-grounded verdicts of success, failure, or replan.<n> Benchmarking reuses the deployment session and verification path, so results trace to real execution.
  arXiv  Detail & Related papers  (2026-07-18T04:46:53Z)
• CAVA: Canonical Action Verification and Attestation for Runtime Governance of Agentic AI Systems [0.6526824510982799]
  This paper presents a runtime-semantics layer for converting heterogeneous agent activity into canonical runtime objects.<n>The contribution is a systems formulation of action-level canonicalization and policy-addressable semantic patterns as a necessary substrate for deployer-side AI governance.
  arXiv  Detail & Related papers  (2026-07-15T11:34:34Z)
• Sovereign Assurance Boundary: Certificate-Bound Admission for Agentic Infrastructure [2.124730017640531]
  Sovereign Assurance Boundary is a certificate-bound runtime admission layer for autonomous execution authority.<n>We detail the airlock-broker architecture, formalize its admission and revocation invariants, and report preliminary feasibility measurements from a Go prototype.
  arXiv  Detail & Related papers  (2026-06-10T03:49:57Z)
• VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents [57.240036084348354]
  We introduce VASO, a framework for verification-guided self-evolution of robot skill contracts.<n>VASO verifies logically inconsistent skill contracts, then verifies plans induced by the skill against global and local temporal specifications.<n>On Clearpath Jackal and PX4 quadcopter tasks, VASO reaches 97.2% formal-specification compliance using fewer than 100 optimization samples.
  arXiv  Detail & Related papers  (2026-06-03T20:02:35Z)
• Proof-Carrying Agent Actions: Model-Agnostic Runtime Governance for Heterogeneous Agent Systems [0.6526824510982799]
  This paper presents Proof-Carrying Agent Actions (PCAA), a runtime-neutral governance model centered on an action certificate.<n>PCAA organizes control around five checkpoints: pre-action admissibility, action open, assumption capture, approval, and outcome closure.<n>We study the model through a reference implementation in a heterogeneous agent control plane and a disclosure-bounded evaluation protocol.
  arXiv  Detail & Related papers  (2026-06-02T18:10:35Z)
• From Patches to Trajectories: Privileged Process Supervision for Software-Engineering Agents [56.31499185764872]
  Supervised fine-tuning (SFT) on long teacher trajectories is the dominant way to instill investigation and reasoning in open software-engineering (SWE) agents.<n>We propose Patches-to-Trajectories (P2T), which uses $pstar$ as privileged information during curation and formulates trajectory construction as bi-objective optimization over per-step effectiveness and trajectory length.
  arXiv  Detail & Related papers  (2026-05-21T04:54:55Z)
• Compiling Activation Steering into Weights via Null-Space Constraints for Stealthy Backdoors [48.881343993730844]
  Safety-aligned large language models (LLMs) are increasingly deployed in real-world pipelines.<n> adversaries can distribute backdoored checkpoints that behave normally under standard evaluation but jailbreak when a hidden trigger is present.<n>Recent post-hoc weight-editing methods offer an efficient approach to injecting such backdoors.
  arXiv  Detail & Related papers  (2026-04-14T06:48:33Z)
• A Physical Agentic Loop for Language-Guided Grasping with Execution-State Monitoring [5.437966695589128]
  We reformulate language-guided grasping as a bounded embodied agent operating over grounded execution states.<n>We introduce a physical agentic loop that wraps an unmodified learned manipulation primitive.<n>We validate the resulting loop on a mobile manipulator with an eye-in-hand D405 camera.
  arXiv  Detail & Related papers  (2026-04-08T08:01:35Z)
• Zero-Trust Runtime Verification for Agentic Payment Protocols: Mitigating Replay and Context-Binding Failures in AP2 [0.0]
  We present a security analysis of the AP2 mandate lifecycle and identify enforcement gaps that arise during runtime in agent-based payment systems.<n>We propose a zero-trust runtime verification framework that enforces explicit context binding and consume-once mandate semantics.<n>We show that context-aware binding and consume-once enforcement address distinct and complementary attack classes, and that both are required to prevent replay and context-redirect attacks.
  arXiv  Detail & Related papers  (2026-02-06T03:22:11Z)
• Runaway is Ashamed, But Helpful: On the Early-Exit Behavior of Large Language Model-based Agents in Embodied Environments [54.67512489842682]
  Large language models (LLMs) have demonstrated strong planning and decision-making capabilities in complex embodied environments.<n>We take a first step toward exploring the early-exit behavior for LLM-based agents.
  arXiv  Detail & Related papers  (2025-05-23T08:23:36Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.