arXiv:2609.11596v1 [cs.CR] 10 Sep 2026
From Intent to Execution Grant: An Execution-Boundary Conformance Profile for High-Risk AI Actions Mengting Wu∗
Lin Wang
[email protected] Chengdu Havenlon Security Technology Co., Ltd. Chengdu, China
Chengdu Havenlon Security Technology Co., Ltd. Chengdu, China
Yong Zhang
Jiang Deng
Chengdu Havenlon Security Technology Co., Ltd. Chengdu, China
Chengdu Havenlon Security Technology Co., Ltd. Chengdu, China
Abstract AI agents increasingly propose externally consequential actions, including financial transfers, infrastructure changes, software deployments, information disclosures, and physical actuation. Authorization engines, policy languages, runtime monitors, provenance mechanisms, and agent guardrails provide important control foundations, but their interfaces do not necessarily define a common semantic contract for the final transition from a particular candidate action to execution authority. We specify EBL-Core, an execution-boundary conformance profile for determining whether one canonical, fully materialized AIgenerated candidate may receive action-scoped execution authority under explicit conditions. EBL-Core relates a structured intent object, a Root Policy, an Operational Policy, root and operational Evidence Obligations, typed evidence, explicit context and time, and a verifiable Decision Derivation. These elements are bound through an Execution Release Contract (ERC), defined as a decision-binding release-condition object. An ERC is not itself an authority-bearing token; a verified ALLOW ERC may support issuance of a separate Execution Grant, whose exercise is governed by Redemption-time validation. The contribution is the semantic release-and-redemption contract joining these existing mechanism classes, together with conformance requirements for action binding, policy non-weakening, evidence-obligation handling, deterministic adjudication, derivation verification, and grant lifecycle behavior. EBL-Core does not establish human-intent correctness, evidence truth, complete mediation, global non-bypassability, faithful execution, or correct external outcomes; those properties remain conditional on explicit deployment and trust assumptions. The accompanying minimal reference artifact instantiates one financial-transfer profile with machine-readable schemas, a reference adjudicator, a separately implemented verifier and Semantic Replay path, and a linearizable in-memory grant store. In the retained run, 34 static vectors and 15 lifecycle and mutation checks matched their specified outcomes; 100 trials of 32 concurrent Redemption attempts produced exactly one successful Redemption and one protected test effect per trial, and 100 Revoke–Redeem
∗ Corresponding author.
races ended in a valid terminal outcome. These results demonstrate executability of the specified subset, not production readiness, mechanized correctness, or deployment-level security.
Keywords AI agents, execution boundaries, authorization, runtime enforcement, formal semantics, conformance profiles
1 Introduction 1.1 Motivation AI systems are increasingly used not only to generate information, recommendations, or plans, but also to propose actions that can change external state. Such actions include initiating financial operations, modifying production infrastructure, deploying software, disclosing protected information, and actuating physical devices. In these settings, an agent’s output is not necessarily the terminal result of computation. It may instead become an input to an execution mechanism that possesses credentials, invokes tools, commits transactions, or controls devices. This transition changes the relevant safety question. For an information-producing system, evaluation can often focus on the quality, correctness, or acceptability of generated content. For an action-producing system, an additional question arises: under what conditions may a particular generated action acquire the authority required to affect an external system? The distinction is important because an AI-generated action is typically constructed through several stages. A user request may be interpreted into an internal goal, refined into a plan, translated into one or more tool invocations, and finally materialized as a concrete operation containing execution-relevant parameters. These parameters may include a financial amount and recipient, an infrastructure resource and configuration change, a software artifact and deployment environment, a data object and disclosure destination, or a device command and target state. The final action may therefore differ materially from the natural-language request or intermediate plan from which it was derived. At the same time, the conditions governing an action may change during this process. Evidence may expire, operational state may change, a policy version may be replaced, an approval may cover an earlier object rather than the final one, or the candidate action may be modified after adjudication. A decision that was justified at one
Wu et al.
stage is not necessarily valid at the moment execution authority is exercised. These observations motivate an explicit semantic interface between action proposal and externally consequential execution.
1.2
by themselves establish that execution is causally dependent on the decision. Complete mediation, correct Grant Issuance, linearized Redemption, faithful realization of the candidate by the Effector, protection of trusted components, and exclusion of alternative authority paths remain deployment properties.
The Execution-Release Problem
Many authorization systems determine whether a principal or structured request is permitted to perform an operation on a resource under applicable policies and contextual attributes. Some can evaluate highly specific requests, including exact operation parameters. These capabilities remain necessary for AI-agent systems: neither an agent nor a supporting service should obtain authority beyond the permissions assigned to the relevant identities, roles, credentials, and policies. The execution-boundary question specializes this decision rather than replacing it: What minimum semantic release-and-redemption contract must hold before one canonical, fully materialized AI-generated candidate may receive actionscoped execution authority? The distinguishing issue is not merely whether an authorization engine can inspect detailed inputs. It is whether the system defines a common contract that binds the final candidate to all decision-relevant conditions and preserves those bindings through the release and Redemption of authority. Depending on the action, this contract may require that: • the candidate remains within the immutable constraints and permitted refinement dimensions of a trusted intent object; • the candidate is canonical and fully materialized before adjudication; • the Root Policy permits the candidate; • the Operational Policy independently permits the candidate without weakening the Root Policy; • every obligation in 𝑄 𝐾 ∪ 𝑄 𝑃 is discharged by evidence classified VALID; • the governing policy, evidence, context, schema, and profile versions are explicit; • a supplied Decision Derivation verifies under the committed inputs; • decision-relevant changes trigger denial or re-adjudication; and • any resulting authority is scoped to the committed candidate and governed by the specified grant lifecycle. We refer to this as the execution-release problem. It concerns the semantic transition from a concrete action proposal to conditions under which action-scoped execution authority may be issued and redeemed. These requirements can be implemented using existing authorization languages, proof systems, capability mechanisms, and runtime monitors. EBL-Core does not claim that such mechanisms are unable to represent them. Its purpose is to define which bindings must be jointly present for an implementation to conform to a shared execution-release profile. The distinction also separates semantic adjudication from deployment enforcement. An ALLOW decision and a valid ERC do not
1.3
Relationship to Existing Abstractions
The execution-release problem builds on several established areas of research and engineering. Authorization languages define policies over principals, actions, resources, attributes, and contextual inputs. Policy decision points and policy enforcement points separate the evaluation of authorization rules from the application mechanisms that enforce the resulting decisions. These abstractions provide the foundation for representing and evaluating many of the constraints considered in this paper. Reference monitors characterize the architectural requirements for enforcing a security policy, including complete mediation, tamper resistance, and verifiability. Runtime-assurance architectures similarly place an assured decision component between an untrusted or insufficiently assured controller and a protected system. These approaches establish why a decision mechanism must be positioned outside the authority of the component whose actions it governs. Agent guardrails and runtime policy systems apply related principles to model-generated actions. They may constrain tool selection, validate arguments, enforce preconditions, restrict privileges, monitor execution histories, or route selected operations through human review. Provenance and audit systems record the origin and evolution of requests, decisions, and execution events. Proof-carrying authorization systems further demonstrate how a decision can be accompanied by evidence that it follows from specified policies and credentials. These mechanisms address substantial portions of the executioncontrol problem. The objective of this paper is not to characterize them as generally insufficient, but to identify the integration contract required at a particular boundary. A general authorization engine need not prescribe how natural-language input becomes a trusted intent object. A runtime monitor need not define a portable evidence-obligation representation. A provenance system may describe recorded events without deciding whether a candidate should receive execution authority. Depending on its interface, a guardrail may block a tool invocation without exposing a Decision Derivation that an independent verifier can check. Similarly, an authorization derivation may establish permission from declared premises without specifying how candidate mutation, state change, ERC Generation, Grant Issuance, and Redemption affect the continued usability of that result. Consequently, two conforming and individually well-designed systems may still disagree about: • which object was authorized; • which evidence was required; • which policy versions governed the decision; • whether an earlier approval covers a refined candidate; • when a decision becomes stale; • what authority an ALLOW result releases; and
From Intent to Execution Grant: An Execution-Boundary Conformance Profile for High-Risk AI Actions
• what an independent verifier must reconstruct. The residual abstraction considered here is a shared contract for these execution-release semantics. Such a contract can be implemented using existing policy languages, proof systems, reference monitors, and agent runtimes. It does not require replacing them.
1.4
Execution-Boundary Semantics
We define an execution boundary as the last scoped mediation point at which a proposed action can still be denied before an externally relevant effect occurs. The definition is scoped to declared action classes and execution paths. Whether every path capable of producing a protected effect actually traverses the boundary is a deployment property. EBL-Core specifies the semantic behavior required at this boundary. Its adjudication function has the form
may release action-scoped execution authority only from a verified ALLOW ERC. Under the baseline profile, the grant begins in ISSUED and a successful, linearized Redemption changes it to CONSUMED; CONSUMED, EXPIRED, and REVOKED are terminal for that grant instance. EBL-Core defines semantic properties required of conforming adjudicators, ERC generators, Grant Issuers, verifiers, and Redemption Interfaces. Stronger claims about external effects require the designated grant to be necessary for the scoped action, the protected transition and grant-state update to be linearized, the Effector to realize the committed candidate faithfully, and alternative effectproducing paths to be excluded or separately governed.
1.5
1. An execution-boundary conformance model. We characterize the execution-release problem and define the typed actors, objects, lifecycle stages, trust assumptions, and deployment boundary required to connect one canonical AI-generated candidate to action-scoped execution authority. 2. Intent-bound, evidence-aware, non-weakening adjudication semantics. We specify adjudication over trusted intent, one canonical candidate, Root Policy, Operational Policy, separately derived obligations 𝑄 𝐾 and 𝑄 𝑃 , typed evidence, explicit context, and explicit time. The profile separates root-policy dominance, conjunctive rule addition, and policy-version evolution, and requires deterministic, side-effect-free, inputclosed, and bounded evaluation. 3. The Execution Release Contract. We define the ERC as a decision-binding release-condition object connecting adjudication to separate Grant Issuance and Redemption operations. It commits to the exact candidate and decision state, including a supplied Decision Derivation, and provides a common verification and conformance target without defining a new general-purpose capability primitive.
Γ𝐾 (𝑃, 𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) → (𝑑, 𝑟, 𝜋), where 𝐼 is a trusted intent object; 𝑥 is one canonical, fully materialized candidate action; 𝐾 is the versioned Root Policy; 𝑃 is the versioned Operational Policy; 𝐸𝑣 is the complete materialized evidence input; 𝐶𝑡𝑥 is explicit decision-relevant context; 𝑡 is explicit adjudication time; 𝑑 is the decision; 𝑟 is a stable reason code; and 𝜋 is a Decision Derivation. The applicable Evidence Obligations are derived separately: 𝑄 𝐾 = 𝑂𝑏𝑙𝑖𝑔𝑎𝑡𝑖𝑜𝑛𝑠𝐾 (𝐾, 𝐼, 𝑥, 𝐶𝑡𝑥) and 𝑄 𝑃 = 𝑂𝑏𝑙𝑖𝑔𝑎𝑡𝑖𝑜𝑛𝑠𝑃 (𝑃, 𝐼, 𝑥, 𝐶𝑡𝑥). The Operational Policy may add obligations through 𝑄 𝑃 , but it cannot remove, weaken, rename, or reinterpret obligations in 𝑄 𝐾 . This requirement is part of root-policy dominance. It is distinct from conjunctive rule addition and from the compatibility relation used to classify Operational Policy evolution. The candidate, rather than an earlier plan or textual request, is the immediate object of adjudication. Bound(I,x,Ctx,t) permits explicitly authorized refinement but requires the final candidate to preserve immutable intent constraints. This relation establishes consistency with the trusted intent object; it does not establish that the object correctly represents a human’s latent intent. For a positive decision, every applicable obligation in 𝑄 𝐾 ∪ 𝑄 𝑃 must resolve to VALID. UNKNOWN, MISSING, EXPIRED, and CONFLICT remain distinct diagnostic states, but none discharges a positive obligation. Evidence classification concerns the declared evidence interface and does not establish external truth. Adjudication is connected to authority through four distinct operations: Adjudicate(B) -> (d, r, pi) GenerateERC(B, d, r, pi, ...) -> erc | bottom IssueGrant(erc, B, pi) -> g | bottom Redeem(g, erc, B, pi, R) -> EXECUTE | DENY ERC Generation creates a decision-binding release-condition object. The ERC commits to the adjudicated inputs, obligations, decision, reason code, validity conditions, and supplied Decision Derivation, but is not inherently authority-bearing. Grant Issuance
Contributions
This paper makes three contributions.
Together, these contributions define an execution-release profile that can be implemented over heterogeneous authorization, evidence, capability, and runtime mechanisms. The included artifact validates a bounded transfer profile; interoperability among independently developed implementations remains an empirical question for future conformance studies.
2
Related Work
This section organizes related work by the abstraction each research family treats as primary. The purpose is not to argue that existing mechanisms cannot implement EBL requirements. In many cases, they can and should serve as EBL backends. The relevant distinction is between capabilities that a system may provide and obligations that its primary abstraction specifies by default. EBL does not claim that policy evaluation, capability security, proof-carrying authorization, runtime mediation, or agent action control is new. Its proposed residual is a common execution-release profile that specifies which versioned facts must jointly justify
Wu et al.
• how a trusted intent constrains the candidate’s permitted refinements; • whether the decision covers the exact canonical candidate submitted for Redemption; • how 𝑄 𝐾 and 𝑄 𝑃 are derived and protected from operational weakening; • how evidence freshness, absence, or conflict affects those obligations; • which candidate, policy, evidence, context, and time changes invalidate the result; • which Decision Derivation an independent verifier must accept; • whether a decision may support Grant Issuance; or • how grant state and current conditions are checked during Redemption.
an action-scoped execution grant, how that grant is bound to the final candidate action, and when the grant must be rejected or re-adjudicated.
2.1
Authorization Languages
Authorization languages define how policies determine whether an identified principal may perform an action on a resource under a given set of attributes and environmental conditions. Attributebased access control provides the general principal–operation– object–environment foundation on which these policy engines build [11]. They provide the most direct foundation for EBL’s policyevaluation semantics. Cedar [5] defines an expressive and analyzable authorization language organized around principal, action, resource, and context. Its design includes schema-based validation, explicit permit and forbid policies, default denial, and formal modeling suitable for policy analysis. Cedar demonstrates that a policy language can combine practical evaluation performance with a semantics precise enough to support equivalence and authorization analysis. Open Policy Agent and Rego [14] provide a domain-independent policy-decision mechanism over structured input. Rego separates policy evaluation from application logic and permits applications to request structured decisions from an external or embedded policy engine. This separation allows the same policy framework to govern API access, infrastructure configuration, deployment controls, and other application-specific decisions. XACML [13] defines a standardized attribute-based accesscontrol architecture involving policy administration, policy decision, policy information, and policy enforcement points. It also defines Permit, Deny, NotApplicable, and several forms of Indeterminate, together with policy-combining algorithms, obligations, and advice. Owned abstraction. These systems own the abstraction of a policy decision over structured authorization inputs. Their central question is whether a request, usually represented through subject, action, resource, and environment attributes, is permitted under a policy set. What EBL inherits. EBL inherits declarative policy evaluation, explicit decision inputs, schema or type validation, default-denial behavior, policycombining semantics, separation of decision logic from application code, and the treatment of unavailable information as distinct from positive authorization. EBL’s root and operational policies need not be evaluated by a new engine; a conforming implementation could compile them to Cedar or Rego or express them through an XACML profile. What remains unspecified. Within the base abstractions and documented integrations considered here, authorization languages do not uniformly require one execution-release contract relating trusted intent, one canonical candidate, Evidence Obligations, policy versions, DecisionDerivation Verification, Grant Issuance, and Redemption. Individual requirements may be expressed using attributes, policies, obligations, or application logic, but their cross-component semantics depend on the integration. In particular, a policy decision does not necessarily specify:
EBL-Core does not claim greater general policy expressiveness. It makes these conditions mandatory within a restricted executionrelease conformance profile.
2.2
Capability and Proof-Carrying Authorization
Capability-based systems [6] represent authority through protected references or tokens that designate both an object and the operations permitted on it. Possession of an appropriate capability is a prerequisite for exercising the associated authority. Capability systems support least authority by allowing rights to be scoped, delegated, attenuated, and, depending on the design, revoked or time-bounded. Macaroons illustrate how contextual caveats can be bound to decentralized authorization credentials without prescribing EBL’s candidate and Redemption lifecycle [3]. Proof-Carrying Authorization extends authorization with machine-checkable evidence that a request follows from a set of policies and credentials. In a typical design, an untrusted requester supplies credentials and a logical derivation, while a trusted verifier checks whether the derivation establishes the requested authorization. The Proof-Carrying Authorization System [2] establishes this general architecture, while systems such as the Proof-Carrying File System [8] connect proof verification to dynamic policies and conditional capabilities. Owned abstraction. Capability systems own the representation and controlled exercise of authority. Proof-carrying authorization owns the derivation and verification of an authorization conclusion from declared policies, credentials, and trusted roots. What EBL inherits. EBL inherits the principle that authorization should be represented by an object whose scope can be independently checked, rather than by an informal statement that an action was approved. It also inherits the distinction between proof construction and proof verification, the use of explicit trusted roots, and the requirement that a protected operation depend on successful verification. The EBL decision derivation is consequently not proposed as a new proof-carrying primitive. It is an execution-specific derivation whose obligations may be implemented using established authorization logics or proof systems.
From Intent to Execution Grant: An Execution-Boundary Conformance Profile for High-Risk AI Actions
What remains unspecified. General capability and proof-carrying authorization models do not, by themselves, standardize the lifecycle through which an AIgenerated proposal becomes a final candidate action. They do not necessarily prescribe: • a trusted representation of the request-level intent; • a refinement relation between that intent and the materialized action; • commitments to the final payload and its execution-relevant parameters; • typed evidence obligations and their freshness conditions; • invalidation after policy, evidence, context, or candidate mutation; • a common execution-release certificate format; or • a redemption-time check against the current decisionrelevant state. These properties can be represented in sufficiently expressive authorization logics. EBL’s proposed contribution is to make them mandatory parts of a specific conformance profile. The distinction is also epistemic. A proof-carrying authorization mechanism may establish that an authorization conclusion follows from supplied policies, credentials, and premises. Within EBL-Core, successful Decision-Derivation Verification similarly establishes only that the recorded decision follows under the declared profile semantics, committed inputs, and trust assumptions. It does not establish that the evidence premises accurately describe the external world or that the authorized effect subsequently occurred.
2.3
Reference Monitor and Runtime Assurance
A reference monitor [1] is an architectural abstraction for policy enforcement. Its reference-validation mechanism is expected to mediate every relevant access, resist tampering, and remain sufficiently small and well specified to support analysis. Complete mediation requires authorization to be reconsidered on every relevant access because decision state may change [19]; execution monitoring further distinguishes policies enforceable from observed event prefixes [20]. The reference-monitor concept therefore addresses where enforcement authority must reside and what structural properties the enforcement mechanism must possess. Runtime Assurance and Simplex architectures [10, 17] apply a related pattern to safety-critical control. An unverified advanced controller may operate while a trusted monitor determines whether its behavior remains within a safety envelope. When the relevant safety condition can no longer be maintained, control is transferred to an assured or reduced-capability controller. These architectures separate high-performance but insufficiently assured decision-making from the component responsible for preserving system safety. Owned abstraction. Reference monitors own complete mediation and protected policy enforcement. Runtime-assurance systems own the supervisory relationship between an untrusted controller, a safety monitor, and an assured fallback or recovery controller. What EBL inherits. EBL inherits the separation between an untrusted action proposer and a trusted enforcement decision. A model, planner, tool selector,
or policy generator may propose an action or a policy update, but it is not the final authority for releasing action-scoped execution authority. EBL also inherits fail-closed mediation and the principle that a reduced operating mode should be represented as an explicitly restricted capability regime rather than as an ambiguous authorization result. If a deployment supports a safe mode, its available actions and transition rules must be specified independently from the Boolean decision concerning an individual candidate action. What remains unspecified. A reference monitor is parametrized by the policy it enforces. The abstraction does not determine which intent, approval, evidence, policy-version, or action-identity obligations should govern an AIgenerated transaction. Runtime-assurance frameworks commonly focus on whether a controller’s proposed behavior preserves a state-space safety condition. They do not necessarily define the authorization and evidence semantics required for heterogeneous digital actions involving identities, recipients, assets, infrastructure resources, disclosure destinations, or externally issued approvals. Conversely, EBL semantics do not establish that an implementation possesses reference-monitor properties. EBL-Core can require an Execution Grant to remain bound to a verified Decision Derivation and committed decision state, but those semantic requirements do not establish that every effect-producing path requires the grant. Complete mediation, protection of the verifier, exclusive control of the necessary capability, and exclusion of alternative execution paths remain deployment assumptions. Usage-control models provide a further foundation by treating authorizations, obligations, mutable attributes, and continuing decisions during usage as first-class concepts [16]. EBL inherits the need to reconsider current conditions but narrows its scope to a candidate-bound release and single-use Redemption contract. The relationship is therefore complementary: reference-monitor and usage-control work define structural and continuing enforcement concerns, while EBL defines the proposed execution-release decision profile that such mechanisms may enforce.
2.4
AI Agent Action Control
Recent agent-security systems place enforcement closer to modelgenerated tool calls and action proposals. This work establishes that action-time mediation for agents is already an active research area. AgentSpec [23] introduces a domain-specific language for specifying runtime constraints through triggers, predicates, and enforcement mechanisms. It demonstrates that agent behavior can be checked against structured rules across code execution, embodiedagent, and autonomous-driving scenarios. Progent [21] represents agent privilege through symbolic policies over tool names and arguments. Every tool call is checked through a deterministic procedure. Progent also distinguishes narrowing policy updates from privilege expansions, using an SMT solver to permit automatic narrowing while requiring separate approval for expansion. This makes monotonic confinement an explicit part of the agent-policy lifecycle. ToolGate [12] models tools using preconditions and postconditions over a typed symbolic state. Preconditions control invocation,
Wu et al.
while postconditions determine whether tool results may update the trusted symbolic state. ToolGate therefore treats tool execution as a contract-governed state transition rather than as an unconstrained continuation of model reasoning. Intent-Governed Access Control [25] converts a trusted request into a short-lived intent certificate, narrows the statically authorized tool manifest, and checks proposed tool and payload effects before execution. IGAC explicitly distinguishes static-policy nonexpansion from request-level confinement and treats the model, intent classifier, and planner as non-authoritative components. FORGE [15] treats policy enforcement as a cross-cutting concern independent of agent reasoning. It uses Datalog policies, a reference monitor, and an observability service governed by an assume–guarantee contract. Its policies may depend on causal execution history and may be enforced across multiple agents at policy-relevant actions. Atomic Decision Boundaries [7] makes the relationship between decision validity and protected state transition explicit. Its primary abstraction is the atomic or linearized boundary needed to avoid a gap between checking decision-relevant state and applying the corresponding effect. EBL-Core inherits this requirement for Redemption; it does not claim to originate atomic decision-effect coupling. Proof-Carrying Agent Actions [24] introduces portable action certificates and runtime verification for agent actions. Its primary abstraction is a proof-carrying action artifact that can accompany an action across system boundaries. EBL-Core does not claim the first portable action certificate or proof-carrying agent action. Its residual concerns the particular decision inputs, policy and obligation separation, ERC role, grant lifecycle, and Redemption semantics required by its conformance profile. Owned abstraction. AgentSpec owns a runtime constraint language for agent behavior; Progent owns symbolic tool-policy enforcement and monotonic privilege management; ToolGate owns typed precondition and postcondition checking for tool-mediated state transitions; IGAC owns request-derived intent certification and payload-level confinement; FORGE owns formal, history-aware runtime policy enforcement; Atomic Decision Boundaries owns decision-effect coupling and linearization; and Proof-Carrying Agent Actions owns portable action certificates and runtime verification. What EBL inherits. EBL-Core inherits external mediation of model-generated actions, typed tool and candidate representations, deterministic policy evaluation, request-scoped confinement, non-expanding policy changes, history- and context-sensitive predicates, portable verification artifacts, and linearized checking at the protected transition. These systems establish substantial portions of the mechanism space on which EBL-Core builds. What remains unspecified. Across the systems compared here, the properties required by EBLCore are distributed rather than uniformly specified by one shared profile. The residual addressed by EBL-Core is the joint contract among: • one canonical, fully materialized candidate; • a trusted intent object and its permitted refinement relation;
• a Root Policy and Operational Policy; • separately identified 𝑄 𝐾 and 𝑄 𝑃 ; • complete typed evidence and explicit context; • a verifiable Decision Derivation; • an ERC that is not inherently authority-bearing; • separate ERC Generation and Grant Issuance; • the ISSUED, CONSUMED, EXPIRED, and REVOKED grant lifecycle; and • single-use, linearized Redemption at the protected transition. This residual is narrower than discovering action-time mediation, intent certificates, action certificates, deterministic tool gates, atomic boundaries, or proof-carrying authorization. EBL-Core instead defines the contents and lifecycle that an implementation must expose to claim conformance with this particular executionrelease profile. Provenance and remote-attestation architectures address another complementary interface. W3C PROV models entities, activities, agents, and derivation relations [22]; RATS separates an Attester, Verifier, and Relying Party when evidence is appraised [4]. EBLCore can consume records produced by such systems, but its VALID status remains an obligation-relative adjudication result rather than a general provenance or attestation truth claim.
2.5
The Execution-Release Gap
The preceding work establishes the component abstractions on which EBL-Core relies. Table 1 maps six close baselines to the joint obligations of the profile. The classification concerns what each cited abstraction specifies directly, not what a sufficiently programmable implementation could encode. N denotes native semantics, A an explicit adapter convention, E an external component, and U a property not established by the cited abstraction. An A, E, or U entry is not a quality judgment. No comparison row is expected to reproduce EBL-Core because each baseline owns a different abstraction. The residual is the mandatory composition of one canonical candidate, trusted-intent binding, non-weakening policy and obligation separation, typed evidence resolution, a verifiable Decision Derivation, an ERC distinct from released authority, and single-use linearized Redemption. Cedar, Rego, or XACML may evaluate predicates; a proof system may encode a derivation; a capability system may represent the grant; and a reference monitor may govern Redemption. EBL-Core defines the observable joint contract by which that composition can claim conformance.
3 System Model and Execution Release Contract 3.1 System Overview We consider an AI-assisted system in which an agent may propose an action whose execution can produce an externally consequential state transition. The agent does not obtain execution authority merely by generating a syntactically valid action. Instead, the proposed action passes through logically distinct stages: Intent Establishment | Candidate Action Materialization
From Intent to Execution Grant: An Execution-Boundary Conformance Profile for High-Risk AI Actions Primary abstraction
Intent–candidate
Policy–obligation split
Verifiable derivation
Contract–authority split
Grant lifecycle
Linearized Redemption
Cedar [5] Proof-Carrying Authorization [2, 8] Progent [21] Intent-Governed Access Control [25] Atomic Decision Boundaries [7] Proof-Carrying Agent Actions [24]
A A E N E A
A A A A E E
U N U U E N
E A U U E U
E E E E E E
E E E E N E
EBL-Core
N
N
N
N
N
N
Table 1: Conservative mapping of documented primary abstractions to EBL-Core obligations. The table distinguishes semantic ownership from expressibility and does not rank implementation strength or performance.
| Adjudication | ERC Generation | Grant Issuance | Grant Redemption | External Effect
These stages define semantic responsibilities rather than a required deployment topology. A conforming system may colocate several stages within one service or distribute them across multiple trust domains. Properties that depend on separation remain conditional on the deployment. Intent establishment converts an authenticated instruction into a structured intent object 𝐼 . The object identifies the authority under which an action may be considered and the constraints that must survive subsequent refinement. EBL-Core begins after this object has been established; it does not define how natural-language requests are interpreted. Candidate-action materialization produces one concrete candidate 𝑥. Every decision-relevant parameter required to identify the proposed operation must have a committed value. A plan, operation class, partial payload, unresolved parameter, or later-selected target is not a materialized EBL-Core candidate. Adjudication evaluates the candidate against the intent object, the applicable root-policy version, the operational-policy version, their separately derived evidence obligations, explicit context, and explicit time. It returns a decision, a reason, and a decision derivation. ERC generation binds the adjudication result to its decision inputs and release conditions. The resulting Execution Release Contract is a decision-binding release-condition object. It is not inherently authority-bearing. Grant issuance releases action-scoped execution authority from a verified ALLOW ERC. Issuance creates a grant in the ISSUED state. A DENY ERC cannot support grant issuance. Grant redemption validates whether the issued authority may be exercised for the exact candidate under current decision-relevant conditions. The baseline profile permits one successful redemption. Successful redemption changes the grant state from ISSUED to CONSUMED.
External effect is the protected state transition produced through the governed interface. Let 𝑆 denote protected state and let Δ :𝑆 ×𝑋 ⇀𝑆 be the partial transition function for candidate actions. EBL-Core requires validation, single-use grant consumption, and the protected transition to be linearized with respect to decision-relevant state. It specifies this semantic requirement without prescribing an implementation mechanism. The resulting path is: 𝐼 −→ 𝑥 −→ Γ𝐾 (𝑃, 𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) −→ 𝑒𝑟𝑐 −→ 𝑔 −→ Δ(𝑠, 𝑥). An adjudication result is not an ERC; an ERC is not an execution grant; successful grant redemption does not establish that the external action completed correctly or produced its intended outcome.
3.2
Semantic Objects
Let the semantic domains be: 𝐼 ∈ 𝐼𝑛𝑡𝑒𝑛𝑡, 𝑥 ∈ 𝐶𝑎𝑛𝑑𝑖𝑑𝑎𝑡𝑒, 𝐸𝑣 ∈ 𝐸𝑣𝑖𝑑𝑒𝑛𝑐𝑒𝑆𝑒𝑡, 𝑃 ∈ 𝑂𝑝𝑒𝑟𝑎𝑡𝑖𝑜𝑛𝑎𝑙𝑃𝑜𝑙𝑖𝑐𝑦, 𝐾 ∈ 𝑅𝑜𝑜𝑡𝑃𝑜𝑙𝑖𝑐𝑦, 𝐶𝑡𝑥 ∈ 𝐶𝑜𝑛𝑡𝑒𝑥𝑡, 𝑡 ∈ 𝑇𝑖𝑚𝑒, 𝑒𝑟𝑐 ∈ 𝐸𝑥𝑒𝑐𝑢𝑡𝑖𝑜𝑛𝑅𝑒𝑙𝑒𝑎𝑠𝑒𝐶𝑜𝑛𝑡𝑟𝑎𝑐𝑡, 𝑔 ∈ 𝐺𝑟𝑎𝑛𝑡 . We additionally use: 𝑑 ∈ {𝐴𝐿𝐿𝑂𝑊 , 𝐷𝐸𝑁𝑌 },
𝑟 ∈ 𝑅𝑒𝑎𝑠𝑜𝑛,
𝜋 ∈ 𝐷𝑒𝑟𝑖𝑣𝑎𝑡𝑖𝑜𝑛,
and 𝑠𝑡𝑎𝑡𝑒 (𝑔) ∈ {𝐼𝑆𝑆𝑈 𝐸𝐷, 𝐶𝑂𝑁 𝑆𝑈 𝑀𝐸𝐷, 𝐸𝑋 𝑃𝐼𝑅𝐸𝐷, 𝑅𝐸𝑉 𝑂𝐾𝐸𝐷 }. For a semantic object 𝑜, let 𝑖𝑑 𝑣 (𝑜) = 𝐶𝑜𝑚𝑚𝑖𝑡 𝑣 (𝐶𝑎𝑛𝑜𝑛 𝑣 (𝑜))
Wu et al.
denote its identity commitment under profile version 𝑣. We omit the subscript on 𝑖𝑑 where 𝑣 is fixed. 𝐶𝑎𝑛𝑜𝑛 𝑣 is a deterministic canonical representation, and 𝐶𝑜𝑚𝑚𝑖𝑡 𝑣 is an abstract commitment mechanism selected by the applicable profile. A concrete profile may instantiate these operations using a specified canonical encoding and collision-resistant digest, such as a JSON canonicalization scheme and a named hash function [18]. 3.2.1 Intent. An intent object 𝐼 is a structured input established by an identified Intent Authority:
Each obligation identifies its policy origin and the versioned resolution semantics under which it is evaluated. Operational policy 𝑃 cannot remove, weaken, rename, or reinterpret an obligation in 𝑄 𝐾 . It may introduce additional obligations through 𝑄 𝑃 . For each 𝑞 ∈ 𝑄, 𝑆𝑡𝑎𝑡𝑢𝑠 (𝑞, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) ∈ {𝑉 𝐴𝐿𝐼𝐷, 𝑈 𝑁 𝐾𝑁𝑂𝑊 𝑁 , 𝑀𝐼𝑆𝑆𝐼 𝑁𝐺, 𝐸𝑋 𝑃𝐼𝑅𝐸𝐷, 𝐶𝑂𝑁 𝐹 𝐿𝐼𝐶𝑇 }. Only VALID discharges a positive obligation:
𝐼 = ⟨𝑠𝑢𝑏 𝑗𝑒𝑐𝑡, 𝑝𝑢𝑟𝑝𝑜𝑠𝑒, 𝑠𝑐𝑜𝑝𝑒, 𝑐𝑜𝑛𝑠𝑡𝑟𝑎𝑖𝑛𝑡𝑠, 𝑟𝑒 𝑓 𝑖𝑛𝑒𝑚𝑒𝑛𝑡, 𝑎𝑢𝑡ℎ𝑜𝑟𝑖𝑡𝑦, 𝑣𝑎𝑙𝑖𝑑𝑖𝑡𝑦⟩. The relation 𝐵𝑜𝑢𝑛𝑑 (𝐼, 𝑥, 𝐶𝑡𝑥, 𝑡) holds when the exact candidate 𝑥 is an authorized materialization of 𝐼 under context 𝐶𝑡𝑥 at time 𝑡. This relation concerns conformance to the structured intent object. It does not establish that 𝐼 correctly represents latent or natural-language human intent. 3.2.2 Candidate Action. A candidate action is one fully materialized proposed operation: 𝑥 = ⟨𝑎𝑐𝑡𝑜𝑟, 𝑜𝑝𝑒𝑟𝑎𝑡𝑖𝑜𝑛, 𝑡𝑎𝑟𝑔𝑒𝑡, 𝑝𝑎𝑟𝑎𝑚𝑒𝑡𝑒𝑟𝑠, 𝑑𝑒𝑐𝑙𝑎𝑟𝑒𝑑𝐸 𝑓 𝑓 𝑒𝑐𝑡𝑠, 𝑎𝑢𝑡ℎ𝑜𝑟𝑖𝑡𝑦𝑆𝑐𝑜𝑝𝑒⟩. Complete(x) holds only when every decision-relevant parameter has one committed value. A parameter domain permitted by 𝐼 must therefore be resolved to a concrete value before adjudication. If a target, payload, recipient, artifact, or other effect-relevant value is selected or changed later, the result is a different candidate requiring a new adjudication. Two candidates are equivalent only when their canonical decision-relevant representations are equivalent: 𝑥 1 ≡ 𝑥 2 ⇐⇒ 𝐶𝑎𝑛𝑜𝑛 𝑣 (𝑥 1 ) = 𝐶𝑎𝑛𝑜𝑛 𝑣 (𝑥 2 ). The applicable candidate profile must identify every field that may affect the governed operation or its declared effect. The baseline EBL-Core profile does not authorize a set of alternative candidates through one ERC. Set-valued or bounded-action authorization is reserved for a future extension profile. Candidate completeness and declared-effect binding do not establish that the Effector will implement the declared effect faithfully. Effector correctness remains a deployment assumption. 3.2.3
𝐷𝑖𝑠𝑐ℎ𝑎𝑟𝑔𝑒𝑑 (𝑞, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) ⇐⇒ 𝑆𝑡𝑎𝑡𝑢𝑠 (𝑞, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) = 𝑉 𝐴𝐿𝐼 𝐷. These values classify obligation resolution under the declared evidence profile. They do not assign context-free truth values to external assertions. 3.2.4 Root Policy. The root policy 𝐾 defines non-overridable constraints for one identified policy regime and version. It is fixed for a particular adjudication and recorded in the ERC. Root-policy dominance does not imply that 𝐾 is correct, complete, or immutable across administrative updates. Operational policy cannot change: • the semantics of 𝑃𝑒𝑟𝑚𝑖𝑡𝐾 ; • the contents or interpretation of 𝑄 𝐾 ; • the canonicalization rules applied to root-policy objects; or • the root-policy version recorded for the decision. A change to 𝐾 produces a different adjudication input and invalidates baseline reuse of the earlier ERC. Within a profile, a policy-version identifier is immutable and content-bound: it denotes one canonical policy object and its declared evaluation semantics. Any semantic change requires a new identifier; reuse after a content change is non-conformant. 3.2.5 Operational Policy. The operational policy 𝑃 contains mutable authorization, workflow, and deployment restrictions. It may deny additional candidates or generate additional evidence obligations. Define: 𝑃𝑒𝑟𝑚𝑖𝑡𝐾 (𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) and 𝑃𝑒𝑟𝑚𝑖𝑡𝑃 (𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡). The combined direct policy condition is conjunctive:
Evidence. The submitted evidence set is finite:
𝐸𝑣 = {𝑒 1, . . . , 𝑒𝑛 }. Root and operational evidence obligations are generated separately: 𝑄 𝐾 = 𝑂𝑏𝑙𝑖𝑔𝑎𝑡𝑖𝑜𝑛𝑠𝐾 (𝐾, 𝐼, 𝑥, 𝐶𝑡𝑥), 𝑄 𝑃 = 𝑂𝑏𝑙𝑖𝑔𝑎𝑡𝑖𝑜𝑛𝑠𝑃 (𝑃, 𝐼, 𝑥, 𝐶𝑡𝑥), and composed as: 𝑄 = 𝑄𝐾 ∪ 𝑄𝑃 .
𝑃𝑒𝑟𝑚𝑖𝑡𝐾,𝑃 = 𝑃𝑒𝑟𝑚𝑖𝑡𝐾 ∧ 𝑃𝑒𝑟𝑚𝑖𝑡𝑃 . This conjunction is evaluated together with the separately composed obligation set 𝑄 𝐾 ∪ 𝑄 𝑃 . Root-policy dominance follows only under the constraint that 𝑃 cannot modify the root-policy predicate or root obligations. 3.2.6 Context and Time. 𝐶𝑡𝑥 is the finite, explicit decision-relevant context supplied to adjudication. Upstream state may be projected into 𝐶𝑡𝑥, but the resulting projection must contain every contextual field on which the decision depends. Time 𝑡 is a separate explicit input. Evidence freshness, intent validity, policy validity, and other time-dependent predicates are
From Intent to Execution Grant: An Execution-Boundary Conformance Profile for High-Risk AI Actions
evaluated against 𝑡. Trust in the supplied time source is a deployment assumption. 3.2.7 Adjudication. Define the complete adjudication input bundle:
3.3.1 ERC versus an Audit Record. An audit record describes an event for later inspection. An ERC is evaluated prospectively as part of grant issuance or redemption. It may subsequently be retained in an audit trail, but its existence does not establish that: • a grant was issued; • the grant was redeemed; • the Effector executed the candidate; or • the expected external outcome occurred.
𝐵 = ⟨𝑝𝑟𝑜 𝑓 𝑖𝑙𝑒𝑉 𝑒𝑟𝑠𝑖𝑜𝑛, 𝐾, 𝑃, 𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡⟩. The adjudication function is: Γ𝐾 (𝑃, 𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) → (𝑑, 𝑟, 𝜋). For well-formed inputs, ALLOW is produced only if: 𝑊 𝑒𝑙𝑙𝐹𝑜𝑟𝑚𝑒𝑑 (𝐵)
3.3.2 ERC versus a Decision-Derivation Record. A decisionderivation record explains how an evaluator derived a decision. The ERC additionally binds that derivation to:
∧ 𝐵𝑜𝑢𝑛𝑑 (𝐼, 𝑥, 𝐶𝑡𝑥, 𝑡)
• the exact intent and candidate; • the applicable authority scope; • root and operational policy versions; • root and operational evidence obligations; • the submitted evidence; • decision-relevant context and time; • validity conditions; • issuer identity; and • grant-release conditions.
∧ 𝑃𝑒𝑟𝑚𝑖𝑡𝐾 (𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) ∧ 𝑃𝑒𝑟𝑚𝑖𝑡𝑃 (𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) ∧ ∀𝑞 ∈ 𝑄 𝐾 : 𝑆𝑡𝑎𝑡𝑢𝑠 (𝑞, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) = 𝑉 𝐴𝐿𝐼𝐷 ∧ ∀𝑞 ∈ 𝑄 𝑃 : 𝑆𝑡𝑎𝑡𝑢𝑠 (𝑞, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) = 𝑉 𝐴𝐿𝐼𝐷. The decision derivation 𝜋 binds the complete input bundle, the separately generated obligation sets, the evidence classifications, the applied inference steps, and the final decision and reason. 3.2.8 Execution Release Contract. An ERC binds an adjudication result to the conditions under which action-scoped authority may be issued and redeemed. An ERC concerns exactly one canonical candidate action.
The ERC commits to the supplied derivation through 𝑖𝑑 (𝜋). An independently generated derivation need not have the same serialization, provided that it verifies against the same input bundle and yields the same semantic decision and reason.
3.3
3.3.3
Execution Release Contract
Action Binding. An ERC is action-bound when:
Conceptually, an ERC is: 𝑒𝑟𝑐.𝑐𝑎𝑛𝑑𝑖𝑑𝑎𝑡𝑒𝐼𝑑 = 𝑖𝑑 (𝑥). 𝑒𝑟𝑐 = ⟨𝑒𝑟𝑐𝑉 𝑒𝑟𝑠𝑖𝑜𝑛, 𝑝𝑟𝑜 𝑓 𝑖𝑙𝑒𝑉 𝑒𝑟𝑠𝑖𝑜𝑛, 𝑖𝑑 (𝐵), 𝑖𝑑 (𝐼 ), 𝑖𝑑 (𝑥), 𝑎𝑢𝑡ℎ𝑜𝑟𝑖𝑡𝑦𝑆𝑐𝑜𝑝𝑒,
A grant issued from the ERC may be redeemed only for that candidate:
𝑣𝑒𝑟𝑠𝑖𝑜𝑛(𝐾), 𝑣𝑒𝑟𝑠𝑖𝑜𝑛(𝑃), 𝑖𝑑 (𝑄 𝐾 ), 𝑖𝑑 (𝑄 𝑃 ), 𝑖𝑑 (𝐸𝑣), 𝑖𝑑 (𝐶𝑡𝑥), 𝑡, 𝑖𝑛𝑡𝑒𝑟𝑣𝑎𝑙, 𝑑, 𝑟, 𝑖𝑑 (𝜋), 𝑖𝑠𝑠𝑢𝑒𝑟, 𝑛𝑜𝑛𝑐𝑒⟩. Here 𝑡 is the explicit adjudication time already contained in 𝐵; redemption time is written separately as 𝑡𝑟 . The ERC may contain commitments rather than complete embedded objects, provided that a verifier can obtain the bound objects through a defined verification context. An ERC is a decision-binding release-condition object. It is not inherently an authority-bearing token; it specifies the conditions under which authority may be released. A deployment may embed an ERC, an ERC commitment, or an ERC reference in a capability or credential format, but the following semantic roles remain distinct: ERC: Which decision and release conditions were established? Execution Grant: Which action-scoped authority was actually released? Redemption: May that authority be exercised now?
A nonce distinguishes an ERC or issuance instance and supports identity and correlation. It does not, by itself, enforce single use or prevent replay. Replay prevention requires grant-state consumption or an equivalent linearizable mechanism.
𝑖𝑑 (𝑥 ′ ) ≠ 𝑒𝑟𝑐.𝑐𝑎𝑛𝑑𝑖𝑑𝑎𝑡𝑒𝐼𝑑 =⇒ 𝑅𝑒𝑑𝑒𝑒𝑚(𝑔, 𝑒𝑟𝑐, 𝑥 ′, . . .) = 𝐷𝐸𝑁𝑌 . The authority representation may narrow the permissions needed to execute 𝑥, but it cannot substitute another candidate. Authorization of a candidate set is outside the EBL-Core baseline. 3.3.4
State and Policy Binding. The adjudication fingerprint is: 𝐹 (𝐵) = 𝐶𝑜𝑚𝑚𝑖𝑡 (𝑝𝑟𝑜 𝑓 𝑖𝑙𝑒𝑉 𝑒𝑟𝑠𝑖𝑜𝑛, 𝑖𝑑 (𝐼 ), 𝑖𝑑 (𝑥), 𝑣𝑒𝑟𝑠𝑖𝑜𝑛(𝐾), 𝑣𝑒𝑟𝑠𝑖𝑜𝑛(𝑃), 𝑖𝑑 (𝑄 𝐾 ), 𝑖𝑑 (𝑄 𝑃 ), 𝑖𝑑 (𝐸𝑣), 𝑖𝑑 (𝐶𝑡𝑥), 𝑡).
The ERC records 𝐹 (𝐵), the component commitments needed to reconstruct it, or both. The baseline profile requires the root- and operational-policy versions at redemption to match the versions used at adjudication. A policy-version change invalidates reuse of the earlier ERC and requires re-adjudication. A separately established policy-evolution compatibility relation may classify a new operational policy as no more permissive than an earlier one. That classification does not, by itself, preserve a previously issued ALLOW decision or authorize reuse of an old grant.
Wu et al.
3.3.5 Evidence Binding. The ERC records both 𝑄 𝐾 and 𝑄 𝑃 , together with a commitment to the complete evidence set used for adjudication. Recording evidence without its obligations is insufficient because it does not show whether all required positive premises were considered. Evidence binding establishes that identified evidence was evaluated under declared obligation and resolution rules. It does not establish the external truth of an assertion. At redemption, all timeand state-dependent evidence conditions must still hold. Otherwise, the grant is rejected or the candidate is re-adjudicated.
𝑉 𝑎𝑙𝑖𝑑𝑅𝑒𝑑𝑒𝑒𝑚(𝑔, 𝑒𝑟𝑐, 𝐵𝑎 , 𝜋, 𝑅) ⇐⇒ 𝑉 𝑒𝑟𝑖 𝑓 𝑦𝐸𝑅𝐶 (𝑒𝑟𝑐, 𝐵𝑎 , 𝜋) = 𝑉 𝐴𝐿𝐼𝐷 ∧ 𝑒𝑟𝑐.𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛 = 𝐴𝐿𝐿𝑂𝑊 ∧ 𝑠𝑡𝑎𝑡𝑒 (𝑔) = 𝐼𝑆𝑆𝑈 𝐸𝐷 ∧ 𝐺𝑟𝑎𝑛𝑡𝐵𝑜𝑢𝑛𝑑𝑇𝑜 (𝑔, 𝑒𝑟𝑐) ∧ 𝑖𝑑 (𝑥𝑟 ) = 𝑒𝑟𝑐.𝑐𝑎𝑛𝑑𝑖𝑑𝑎𝑡𝑒𝐼𝑑 ∧ 𝑆𝑐𝑜𝑝𝑒 (𝑔) ⊆ 𝑒𝑟𝑐.𝑎𝑢𝑡ℎ𝑜𝑟𝑖𝑡𝑦𝑆𝑐𝑜𝑝𝑒 ∧ 𝑡𝑟 ∈ 𝑒𝑟𝑐.𝑖𝑛𝑡𝑒𝑟𝑣𝑎𝑙
3.3.6 Validity Interval. Each positive ERC contains a validity interval:
[𝑡𝑠𝑡𝑎𝑟𝑡 , 𝑡𝑒𝑛𝑑 ]. This interval cannot extend any applicable validity condition imposed by the intent, root policy, operational policy, evidence obligations, or context. An empty effective interval cannot support grant issuance. 3.3.7
∧ 𝐶𝑢𝑟𝑟𝑒𝑛𝑡𝐶𝑜𝑛𝑑𝑖𝑡𝑖𝑜𝑛𝑠𝐻𝑜𝑙𝑑 (𝑒𝑟𝑐, 𝐵𝑎 , 𝑅). In the baseline profile, CurrentConditionsHold is not an implementation-defined catch-all. It requires: exact Root and Operational Policy version equality; equality of the committed evidence and context identities; continued 𝐵𝑜𝑢𝑛𝑑 (𝐼, 𝑥𝑟 , 𝐶𝑡𝑥𝑟 , 𝑡𝑟 ); continued satisfaction of both policy predicates; VALID status for every obligation in the committed 𝑄 𝐾 ∪ 𝑄 𝑃 ; and satisfaction of every declared temporal predicate. Any extension predicate must be named, versioned, and included in the ERC commitment. A successful redemption performs the logical transition:
Grant Lifecycle. The baseline grant lifecycle is:
+----------> EXPIRED | ISSUED -----------+----------> REVOKED | +-- successful redemption -> CONSUMED CONSUMED, EXPIRED, and REVOKED are terminal for the grant instance. A second redemption attempt against any terminal state returns DENY. Redemption, revocation, and expiry are competing transitions from ISSUED. Their authoritative state changes must be linearized. If revocation or expiry linearizes first, a concurrent Redemption observes a terminal state and is denied. If successful Redemption linearizes first, the grant becomes CONSUMED and a later revocation or expiry request cannot change that terminal state. This ordering requirement follows the standard linearizability criterion for concurrent objects [9]. Grant issuance requires a verified ALLOW ERC and creates 𝑔 such that:
𝑠𝑡𝑎𝑡𝑒 (𝑔) = 𝐼𝑆𝑆𝑈 𝐸𝐷 and
𝐺𝑟𝑎𝑛𝑡𝐵𝑜𝑢𝑛𝑑𝑇𝑜 (𝑔, 𝑒𝑟𝑐) = 𝑡𝑟𝑢𝑒. 3.3.8 Redemption Conditions. Let 𝐵𝑎 be the original adjudication bundle, 𝜋 its supplied derivation, and let
𝑅 = ⟨𝐾𝑟 , 𝑃𝑟 , 𝑥𝑟 , 𝐸𝑣𝑟 , 𝐶𝑡𝑥𝑟 , 𝑡𝑟 ⟩ be the redemption-time inputs. Redemption is eligible only if:
𝑅𝑒𝑑𝑒𝑒𝑚 (𝑔,𝑥𝑟 )
⟨𝑠𝑡𝑎𝑡𝑒 (𝑔) = 𝐼𝑆𝑆𝑈 𝐸𝐷, 𝑠⟩ −−−−−−−−−−−→ ⟨𝑠𝑡𝑎𝑡𝑒 (𝑔) = 𝐶𝑂𝑁 𝑆𝑈 𝑀𝐸𝐷, Δ(𝑠, 𝑥𝑟 )⟩. Validation, the ISSUED-to-CONSUMED transition, and the protected effect must be linearized with respect to decision-relevant state. Acceptable realizations may include an atomic transaction, version-conditional commit, transactional state transition, or another mechanism with equivalent semantics. A separate recheck followed by an interleavable effect does not satisfy this requirement. EBL-Core specifies the linearization requirement, not the implementation mechanism.
3.4
Threat Model and Non-Goals
The adversary may control the Agent and untrusted content available to it. The adversary may attempt to: • construct an action inconsistent with the established intent; • substitute or mutate a candidate after adjudication; • omit execution-relevant parameters; • supply malformed, missing, expired, or conflicting evidence; • cause operational policy to omit root-policy obligations; • replay an earlier ERC or grant; • race two redemption attempts; • exploit a state transition between validation and effect; • present an ERC under different policy or profile versions; or • cause disagreement between an adjudicator and verifier. Under the base model, operational policy cannot change 𝑃𝑒𝑟𝑚𝑖𝑡𝐾 , 𝑄 𝐾 , or the resolution semantics of root obligations. This restriction establishes root-policy dominance within the declared policy regime. It does not establish that the root policy is correct or that its administrative authority can never replace it. The semantic properties of EBL-Core include:
From Intent to Execution Grant: An Execution-Boundary Conformance Profile for High-Risk AI Actions
• deterministic semantic decisions and reasons over equivalent closed inputs; • root-policy dominance under constrained obligation composition; • binding to one canonical candidate; • rejection when a positive evidence obligation is not discharged; • verification of a decision derivation against the complete input bundle; • single-use grant-consumption semantics; and • rejection when current redemption conditions do not match the ERC.
3. Stable replay identity Implementations using the same profile and semantic object derive the same canonical representation and commitment. Canonical identity establishes equality within the model. It does not establish authenticity, authorization, provenance, or external truth.
4.2
Intent-to-Candidate Binding Semantics
An intent object 𝐼 is a trusted structured input, not a representation of unobservable mental intent. Let: 𝐶𝑜𝑚𝑝𝑙𝑒𝑡𝑒𝐶𝑜𝑟𝑒 (𝑥)
The following properties remain deployment assumptions: • complete mediation of every relevant effect-producing path; • integrity and availability of trusted inputs; • protection of the applicable root-policy version; • correct implementation of the verifier, issuer, and Effector; • exclusive control of the authority needed for the protected effect; • linearizable redemption, consumption, and protected transition; • prevention of unauthorized credential extraction or delegation; and • faithful execution of the candidate by the Effector. The model does not claim global non-bypassability, correct human-intent understanding, evidence truth, root-policy correctness, correct external outcomes, or security after compromise of every trusted role.
4 Formal Execution-Boundary Semantics 4.1 Semantic Domains and Canonical Identity Let: 𝐵 = ⟨𝑣, 𝐾, 𝑃, 𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡⟩ be the complete input bundle for one adjudication, where 𝑣 is the EBL-Core profile version. For each decision-relevant object 𝑜, 𝑖𝑑 (𝑜) = 𝐶𝑜𝑚𝑚𝑖𝑡 𝑣 (𝐶𝑎𝑛𝑜𝑛 𝑣 (𝑜)).
hold only when 𝑥 denotes one candidate action and every execution-relevant parameter has a concrete committed value. The EBL-Core binding predicate is: 𝐵𝑜𝑢𝑛𝑑 (𝐼, 𝑥, 𝐶𝑡𝑥, 𝑡 ) ⇐⇒ 𝑊 𝑒𝑙𝑙𝐹𝑜𝑟𝑚𝑒𝑑𝐼𝑛𝑡𝑒𝑛𝑡 (𝐼 ) ∧ 𝐴𝑢𝑡ℎ𝑜𝑟𝑖𝑧𝑒𝑑𝐼𝑛𝑡𝑒𝑛𝑡𝐼𝑠𝑠𝑢𝑒𝑟 (𝐼 ) ∧ 𝑡 ∈ 𝑊 𝑖𝑛𝑑𝑜𝑤 (𝐼 ) ∧ 𝐶𝑜𝑚𝑝𝑙𝑒𝑡𝑒𝐶𝑜𝑟𝑒 (𝑥 ) ∧ 𝑆𝑐𝑜𝑝𝑒 (𝑥 ) ⊑ 𝑆𝑐𝑜𝑝𝑒 (𝐼 ) ∧ 𝐴𝑢𝑡ℎ𝑜𝑟𝑖𝑧𝑒𝑑𝑅𝑒 𝑓 𝑖𝑛𝑒𝑚𝑒𝑛𝑡 (𝐼, 𝑥, 𝐶𝑡𝑥, 𝑡 ) ∧ 𝑃𝑟𝑒𝑠𝑒𝑟 𝑣𝑒𝑠𝐼𝑚𝑚𝑢𝑡𝑎𝑏𝑙𝑒𝐶𝑜𝑛𝑠𝑡𝑟𝑎𝑖𝑛𝑡𝑠 (𝐼, 𝑥, 𝐶𝑡𝑥, 𝑡 ).
Permitted refinement may resolve an intent-authorized domain to one concrete operation, target, or parameter value. It cannot leave an execution-relevant choice to be selected after adjudication. Consequently: 𝑥 = {𝑥 1, . . . , 𝑥𝑛 }
or 𝑥 = an unresolved bounded action family
does not satisfy 𝐶𝑜𝑚𝑝𝑙𝑒𝑡𝑒𝐶𝑜𝑟𝑒 (𝑥). Support for action families requires an extension profile with separate identity, refinement, and redemption semantics. Intent binding establishes conformance between structured objects. It does not establish that 𝐼 correctly captures a human request or that execution of 𝑥 will achieve its declared purpose.
4.3
Evidence-Obligation Semantics
Root and operational obligations are generated independently: The applicable profile defines canonical equality 𝑜 1 ≡𝑣 𝑜 2 over all decision-relevant fields. EBL-Core requires:
𝑄 𝐾 = 𝑂𝑏𝑙𝑖𝑔𝑎𝑡𝑖𝑜𝑛𝑠𝐾 (𝐾, 𝐼, 𝑥, 𝐶𝑡𝑥),
1. Canonical determinism 𝑄 𝑃 = 𝑂𝑏𝑙𝑖𝑔𝑎𝑡𝑖𝑜𝑛𝑠𝑃 (𝑃, 𝐼, 𝑥, 𝐶𝑡𝑥), 𝑜 1 ≡𝑣 𝑜 2 =⇒ 𝐶𝑎𝑛𝑜𝑛 𝑣 (𝑜 1 ) = 𝐶𝑎𝑛𝑜𝑛 𝑣 (𝑜 2 ). 2. Computational binding For distinct canonical decision-relevant objects, finding 𝑜 1 .𝑣 𝑜 2 such that 𝐶𝑜𝑚𝑚𝑖𝑡 𝑣 (𝐶𝑎𝑛𝑜𝑛 𝑣 (𝑜 1 )) = 𝐶𝑜𝑚𝑚𝑖𝑡 𝑣 (𝐶𝑎𝑛𝑜𝑛 𝑣 (𝑜 2 )) is computationally infeasible under the selected commitment assumption.
𝑄 = 𝑄𝐾 ∪ 𝑄𝑃 . An obligation contains at least: • a policy-origin identifier; • an assertion, subject, and scope; • admissible evidence types and sources; • freshness conditions; • conflict and aggregation rules; and • the versioned resolution semantics used to classify it.
Wu et al.
Root Policy
Intent Object
Canonical Candidate
Operational Policy
Evidence Obligations
Adjudication
ERC Generation
produces
ERC Decision-binding contract (not authority)
committed
supports issuance
Execution Grant state = ISSUED
Decision Derivation
revocation
REVOKED
Redemption
time
External Effect
success
EXPIRED
CONSUMED
Figure 1: Execution-release lifecycle in EBL-Core. Adjudication consumes the Root Policy, Operational Policy, and Evidence Obligations and produces a Decision Derivation. ERC Generation creates a decision-binding contract, while separate Grant Issuance creates action-scoped authority. Redemption validates current conditions and linearizes the protected effect with the grant-state transition; CONSUMED, EXPIRED, and REVOKED are terminal grant states. For every 𝑞 ∈ 𝑄 𝐾 , its identity and resolution semantics are determined by 𝐾. Operational policy cannot remove, weaken, replace, or reinterpret it. For each 𝑞 ∈ 𝑄: 𝑆𝑡𝑎𝑡𝑢𝑠 (𝑞, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) ∈ {𝑉 𝐴𝐿𝐼𝐷, 𝑈 𝑁 𝐾𝑁𝑂𝑊 𝑁 , 𝑀𝐼𝑆𝑆𝐼 𝑁𝐺,
𝑆𝑡𝑎𝑡𝑢𝑠 (𝑞, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) ≠ 𝑉 𝐴𝐿𝐼𝐷 =⇒ ¬𝐷𝑖𝑠𝑐ℎ𝑎𝑟𝑔𝑒𝑑 (𝑞, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡). These judgments establish satisfaction of declared obligations under the profile. They do not establish the external truth of the underlying assertion.
𝐸𝑋 𝑃𝐼𝑅𝐸𝐷, 𝐶𝑂𝑁 𝐹 𝐿𝐼𝐶𝑇 }. The status function is deterministic under the identified evidence profile. A profile must define mutually exclusive classification rules or a total precedence relation for overlapping diagnostic conditions. In particular, no obligation may be classified VALID while an applicable unresolved conflict remains. The discharge predicate is:
4.4
Policy-Composition Semantics
Define: 𝑅𝑜𝑜𝑡𝑂𝐾𝐾 (𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡 ) ⇐⇒ 𝑃𝑒𝑟𝑚𝑖𝑡𝐾 (𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡 ) ∧ 𝐸𝑣𝑖𝑑𝑒𝑛𝑐𝑒𝑂𝐾𝐾 (𝐾, 𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡 ), and:
𝐷𝑖𝑠𝑐ℎ𝑎𝑟𝑔𝑒𝑑 (𝑞, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) ⇐⇒ 𝑆𝑡𝑎𝑡𝑢𝑠 (𝑞, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) = 𝑉 𝐴𝐿𝐼𝐷. 𝑂𝑝𝑒𝑟𝑎𝑡𝑖𝑜𝑛𝑎𝑙𝑂𝐾𝑃 (𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡 ) ⇐⇒ 𝑃𝑒𝑟𝑚𝑖𝑡𝑃 (𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡 )
Define:
∧ 𝐸𝑣𝑖𝑑𝑒𝑛𝑐𝑒𝑂𝐾𝑃 (𝑃, 𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡 ).
𝐸𝑣𝑖𝑑𝑒𝑛𝑐𝑒𝑂𝐾𝐾 (𝐾, 𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) ⇐⇒
For the empty operational policy:
∀𝑞 ∈ 𝑄 𝐾 : 𝐷𝑖𝑠𝑐ℎ𝑎𝑟𝑔𝑒𝑑 (𝑞, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡), and:
𝑃𝑒𝑟𝑚𝑖𝑡 ∅ = 𝑡𝑟𝑢𝑒,
𝐸𝑣𝑖𝑑𝑒𝑛𝑐𝑒𝑂𝐾𝑃 (𝑃, 𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) ⇐⇒
𝑄 ∅ = ∅,
𝑂𝑝𝑒𝑟𝑎𝑡𝑖𝑜𝑛𝑎𝑙𝑂𝐾∅ = 𝑡𝑟𝑢𝑒.
For fixed 𝜂 = ⟨𝐼, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡⟩, define:
∀𝑞 ∈ 𝑄 𝑃 : 𝐷𝑖𝑠𝑐ℎ𝑎𝑟𝑔𝑒𝑑 (𝑞, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡). The combined evidence condition is:
𝐴𝑙𝑙𝑜𝑤𝜂 (𝐾, 𝑃) = {𝑥 | 𝑊 𝑒𝑙𝑙𝐹𝑜𝑟𝑚𝑒𝑑 (𝐵) ∧ 𝐵𝑜𝑢𝑛𝑑 (𝐼, 𝑥, 𝐶𝑡𝑥, 𝑡)
𝐸𝑣𝑖𝑑𝑒𝑛𝑐𝑒𝑂𝐾𝐾,𝑃 = 𝐸𝑣𝑖𝑑𝑒𝑛𝑐𝑒𝑂𝐾𝐾 ∧ 𝐸𝑣𝑖𝑑𝑒𝑛𝑐𝑒𝑂𝐾𝑃 . Therefore:
∧ 𝑅𝑜𝑜𝑡𝑂𝐾𝐾 (𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) ∧ 𝑂𝑝𝑒𝑟𝑎𝑡𝑖𝑜𝑛𝑎𝑙𝑂𝐾𝑃 (𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡)}.
From Intent to Execution Grant: An Execution-Boundary Conformance Profile for High-Risk AI Actions
4.4.1 Root-Policy Dominance. Provided that 𝑃 cannot modify 𝑃𝑒𝑟𝑚𝑖𝑡𝐾 , 𝑄 𝐾 , or the resolution semantics of root obligations:
where: 𝑉 𝑒𝑟𝑖 𝑓 𝑦𝐷𝑒𝑟𝑖𝑣𝑎𝑡𝑖𝑜𝑛(𝜋𝑎𝑙𝑙𝑜𝑤 , 𝐵, 𝐴𝐿𝐿𝑂𝑊 , 𝑂𝐾) = 𝑡𝑟𝑢𝑒.
𝐴𝑙𝑙𝑜𝑤𝜂 (𝐾, 𝑃) ⊆ 𝐴𝑙𝑙𝑜𝑤𝜂 (𝐾, ∅). This property is relative to one fixed root-policy version 𝐾. It does not claim that 𝐾 is correct, complete, or immutable across administrative changes. 4.4.2 Conjunctive Rule Addition. Let 𝑃 ′ = 𝑃 ∪ {𝑝}, where rule 𝑝 is composed conjunctively:
If CoreOK does not hold: ¬𝐶𝑜𝑟𝑒𝑂𝐾𝐾 (𝑃, 𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) Γ𝐾 (𝑃, 𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) = (𝐷𝐸𝑁𝑌, 𝐹𝑖𝑟𝑠𝑡𝐹𝑎𝑖𝑙𝑢𝑟𝑒 (𝐵), 𝜋𝑑𝑒𝑛𝑦 ) (E-Deny) with:
𝑃𝑒𝑟𝑚𝑖𝑡𝑃 ′ = 𝑃𝑒𝑟𝑚𝑖𝑡𝑃 ∧ 𝑃𝑒𝑟𝑚𝑖𝑡𝑝 𝑉 𝑒𝑟𝑖 𝑓 𝑦𝐷𝑒𝑟𝑖𝑣𝑎𝑡𝑖𝑜𝑛(𝜋𝑑𝑒𝑛𝑦 , 𝐵, 𝐷𝐸𝑁𝑌, 𝐹𝑖𝑟𝑠𝑡𝐹𝑎𝑖𝑙𝑢𝑟𝑒 (𝐵)) = 𝑡𝑟𝑢𝑒.
and:
The profile defines a deterministic priority relation over simultaneous failures and commits that relation through 𝑝𝑟𝑜 𝑓 𝑖𝑙𝑒𝑉 𝑒𝑟𝑠𝑖𝑜𝑛. For EBL-Core, let the ordered failure sequence be:
𝑄𝑃 ′ = 𝑄𝑃 ∪ 𝑄𝑝 . Then: 𝐴𝑙𝑙𝑜𝑤𝜂 (𝐾, 𝑃 ′ ) ⊆ 𝐴𝑙𝑙𝑜𝑤𝜂 (𝐾, 𝑃).
F (𝐵) = ⟨ (𝐼 𝑁 𝑃𝑈𝑇 _𝐼 𝑁𝑉 𝐴𝐿𝐼 𝐷, ¬𝑊 𝑒𝑙𝑙𝐹𝑜𝑟𝑚𝑒𝑑 (𝐵) ),
This property applies only to rule addition under the specified conjunction and obligation-union semantics. It does not apply to arbitrary replacement, deletion, reprioritization, or reinterpretation of policy rules. 4.4.3 Policy-Version Evolution. Define a separate compatibility relation:
(𝐼 𝑁𝑇 𝐸𝑁𝑇 _𝐵𝐼 𝑁 𝐷𝐼 𝑁 𝐺_𝐹𝐴𝐼 𝐿𝐸𝐷, ¬𝐵𝑜𝑢𝑛𝑑 (𝐼, 𝑥, 𝐶𝑡𝑥, 𝑡 ) ), (𝑅𝑂𝑂𝑇 _𝑃𝑂𝐿𝐼𝐶𝑌 _𝐷𝐸𝑁 𝑌 , ¬𝑃𝑒𝑟𝑚𝑖𝑡𝐾 (𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡 ) ), (𝑅𝑂𝑂𝑇 _𝐸𝑉 𝐼 𝐷𝐸𝑁𝐶𝐸_𝑈 𝑁 𝑆𝐴𝑇 𝐼𝑆𝐹 𝐼 𝐸𝐷, ¬𝐸𝑣𝑖𝑑𝑒𝑛𝑐𝑒𝑂𝐾𝐾 (𝐾, 𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡 ) ), (𝑂𝑃𝐸𝑅𝐴𝑇 𝐼𝑂𝑁 𝐴𝐿_𝑃𝑂𝐿𝐼𝐶𝑌 _𝐷𝐸𝑁 𝑌 , ¬𝑃𝑒𝑟𝑚𝑖𝑡𝑃 (𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡 ) ), (𝑂𝑃𝐸𝑅𝐴𝑇 𝐼𝑂𝑁 𝐴𝐿_𝐸𝑉 𝐼 𝐷𝐸𝑁𝐶𝐸_𝑈 𝑁 𝑆𝐴𝑇 𝐼𝑆𝐹 𝐼 𝐸𝐷, ¬𝐸𝑣𝑖𝑑𝑒𝑛𝑐𝑒𝑂𝐾𝑃 (𝑃, 𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡 ) ) ⟩.
𝐶𝑜𝑚𝑝𝑎𝑡𝐾 (𝑃𝑜𝑙𝑑 , 𝑃𝑛𝑒𝑤 )
(1)
only when an appropriate validation procedure establishes: ∀𝐼, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡 : 𝐴𝑙𝑙𝑜𝑤⟨𝐼 ,𝐸𝑣,𝐶𝑡𝑥,𝑡 ⟩ (𝐾, 𝑃𝑛𝑒𝑤 ) ⊆ 𝐴𝑙𝑙𝑜𝑤⟨𝐼 ,𝐸𝑣,𝐶𝑡𝑥,𝑡 ⟩ (𝐾, 𝑃𝑜𝑙𝑑 ).
Version order, naming, or the presence of additional rules does not establish this relation. Compat_K classifies the policy change as non-expanding under fixed 𝐾. It does not imply that every action previously allowed by 𝑃𝑜𝑙𝑑 remains allowed by 𝑃𝑛𝑒𝑤 , and it does not automatically preserve grants issued under 𝑃𝑜𝑙𝑑 . Baseline ERC reuse requires exact policy-version equality. A change to 𝐾 is outside this operational-policy relation and requires a new adjudication.
4.5
𝐹𝑖𝑟𝑠𝑡𝐹𝑎𝑖𝑙𝑢𝑟𝑒 (𝐵) is the reason in the least-indexed pair whose predicate is true. Predicates after the first structurally undefined predicate are not evaluated; INPUT_INVALID therefore dominates all semantic failures. Status selection within an individual obligation follows the separate total precedence declared by its evidenceresolution profile. Equation (1) fixes primary-reason selection without collapsing the full set of diagnostic failures that a derivation may record. ERC eligibility is: 𝐸𝑙𝑖𝑔𝑖𝑏𝑙𝑒𝐹𝑜𝑟 𝐸𝑅𝐶 (𝐵, 𝑑, 𝑟, 𝜋 ) ⇐⇒ 𝑉 𝑒𝑟𝑖 𝑓 𝑦𝐷𝑒𝑟𝑖𝑣𝑎𝑡𝑖𝑜𝑛 (𝜋, 𝐵, 𝑑, 𝑟 ) = 𝑡𝑟𝑢𝑒.
4.5.1 Determinism. For canonically equivalent bundles evaluated under the same semantic profile, conforming implementations must produce the same semantic decision and primary reason:
Adjudication Function
The positive predicate is: 𝐶𝑜𝑟𝑒𝑂𝐾𝐾 (𝑃, 𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡)
𝐶𝑎𝑛𝑜𝑛 𝑣 (𝐵 1 ) = 𝐶𝑎𝑛𝑜𝑛 𝑣 (𝐵 2 ) =⇒ 𝑑 1 = 𝑑 2 ∧ 𝑟 1 = 𝑟 2 .
⇐⇒ 𝑊 𝑒𝑙𝑙𝐹𝑜𝑟𝑚𝑒𝑑 (𝐵) Each supplied derivation must verify:
∧ 𝐵𝑜𝑢𝑛𝑑 (𝐼, 𝑥, 𝐶𝑡𝑥, 𝑡) ∧ 𝑃𝑒𝑟𝑚𝑖𝑡𝐾 (𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡)
𝑉 𝑒𝑟𝑖 𝑓 𝑦𝐷𝑒𝑟𝑖𝑣𝑎𝑡𝑖𝑜𝑛(𝜋𝑖 , 𝐵𝑖 , 𝑑𝑖 , 𝑟𝑖 ) = 𝑡𝑟𝑢𝑒.
∧ 𝑃𝑒𝑟𝑚𝑖𝑡𝑃 (𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡)
Different conforming implementations may use different valid derivation encodings. EBL-Core does not require:
∧ ∀𝑞 ∈ 𝑄 𝐾 : 𝑆𝑡𝑎𝑡𝑢𝑠 (𝑞, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) = 𝑉 𝐴𝐿𝐼𝐷 ∧ ∀𝑞 ∈ 𝑄 𝑃 : 𝑆𝑡𝑎𝑡𝑢𝑠 (𝑞, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) = 𝑉 𝐴𝐿𝐼𝐷. The positive rule is: 𝐶𝑜𝑟𝑒𝑂𝐾𝐾 (𝑃, 𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) Γ𝐾 (𝑃, 𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) = (𝐴𝐿𝐿𝑂𝑊 , 𝑂𝐾, 𝜋𝑎𝑙𝑙𝑜𝑤 )
𝑖𝑑 (𝜋 1 ) = 𝑖𝑑 (𝜋2 ). (E-Allow)
An individual ERC nevertheless commits to the particular derivation supplied with that ERC.
Wu et al.
4.5.2 Side-Effect Freedom, Input Closure, and Bounded Evaluation. Adjudication does not modify external state, policy state, evidence sources, grant state, or protected system state. Its semantic result depends only on 𝐵. A conforming evaluator does not consult an undeclared clock, network source, mutable service, randomness source, or hidden model inference. Each profile specifies an input fragment and resource-bound function: 𝑆𝑡𝑒𝑝𝑠 (Γ, 𝐵) ≤ 𝐵𝑜𝑢𝑛𝑑 𝑣 (|𝐵|). This is a conformance requirement, not a claim that a particular implementation has already been measured or verified against the bound.
4.6
Decision-Derivation Semantics
A decision derivation is a structured witness for one adjudication: 𝜋 = ⟨𝑒𝑛𝑐𝑜𝑑𝑖𝑛𝑔𝑉 𝑒𝑟𝑠𝑖𝑜𝑛, 𝑝𝑟𝑜 𝑓 𝑖𝑙𝑒𝑉 𝑒𝑟𝑠𝑖𝑜𝑛, 𝑖𝑛𝑝𝑢𝑡𝐶𝑜𝑚𝑚𝑖𝑡𝑚𝑒𝑛𝑡𝑠, 𝑝𝑜𝑙𝑖𝑐𝑦𝐶𝑜𝑚𝑚𝑖𝑡𝑚𝑒𝑛𝑡𝑠, 𝑟𝑜𝑜𝑡𝑂𝑏𝑙𝑖𝑔𝑎𝑡𝑖𝑜𝑛𝑠, 𝑜𝑝𝑒𝑟𝑎𝑡𝑖𝑜𝑛𝑎𝑙𝑂𝑏𝑙𝑖𝑔𝑎𝑡𝑖𝑜𝑛𝑠, 𝑒𝑣𝑖𝑑𝑒𝑛𝑐𝑒𝑆𝑡𝑎𝑡𝑢𝑠𝑒𝑠, 𝑖𝑛𝑓 𝑒𝑟𝑒𝑛𝑐𝑒𝑆𝑡𝑒𝑝𝑠, 𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛, 𝑟𝑒𝑎𝑠𝑜𝑛⟩. Define: 𝑉 𝑒𝑟𝑖 𝑓 𝑦𝐷𝑒𝑟𝑖𝑣𝑎𝑡𝑖𝑜𝑛(𝜋, 𝐵, 𝑑, 𝑟 ) = 𝑡𝑟𝑢𝑒 only if: 1. the derivation and 𝐵 identify the same supported profile version; 2. the derivation commits to every component of 𝐵; 3. the recorded root and operational policy versions match 𝐵; 4. the recorded obligation sets equal the obligation sets generated from 𝐵; 5. every evidence status follows from the committed evidence, context, time, and obligation semantics; 6. every derivation leaf corresponds to a committed input; 7. every inference step is admitted by the profile; 8. no required positive or negative premise has been omitted; 9. the terminal judgment is 𝑑 with primary reason 𝑟 ; and 10. the supplied derivation conforms to its declared encoding version. VerifyDerivation is profile-relative. It is not a universal proof system. An ERC additionally checks:
𝑑𝑚 = 𝑒𝑟𝑐.𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛,
𝑟𝑚 = 𝑒𝑟𝑐.𝑟𝑒𝑎𝑠𝑜𝑛,
and: 𝑉 𝑒𝑟𝑖 𝑓 𝑦𝐷𝑒𝑟𝑖𝑣𝑎𝑡𝑖𝑜𝑛(𝜋𝑚 , 𝐵, 𝑑𝑚 , 𝑟𝑚 ) = 𝑡𝑟𝑢𝑒. Different valid derivation encodings may therefore support the same replay result.
4.7
Invalidation, Grant State, and Atomic Redemption
Define the adjudication fingerprint: 𝐹 (𝐵) = 𝐶𝑜𝑚𝑚𝑖𝑡 (𝑝𝑟𝑜 𝑓 𝑖𝑙𝑒𝑉 𝑒𝑟𝑠𝑖𝑜𝑛, 𝑖𝑑 (𝐼 ), 𝑖𝑑 (𝑥), 𝑣𝑒𝑟𝑠𝑖𝑜𝑛(𝐾), 𝑣𝑒𝑟𝑠𝑖𝑜𝑛(𝑃), 𝑖𝑑 (𝑄 𝐾 ), 𝑖𝑑 (𝑄 𝑃 ), 𝑖𝑑 (𝐸𝑣), 𝑖𝑑 (𝐶𝑡𝑥), 𝑡). A baseline ERC becomes non-reusable if: • the candidate identity changes; • the root- or operational-policy version changes; • the committed evidence set changes; • a required evidence status is no longer VALID; • decision-relevant context changes; • intent binding no longer holds; • the validity interval expires; or • the supplied derivation no longer verifies against the original bundle. Invalidation means that the earlier result cannot be reused. It does not convert the earlier ALLOW into a current DENY; a current decision requires re-adjudication. Let the redemption-time input be 𝑅 = ⟨𝐾𝑟 , 𝑃𝑟 , 𝑥𝑟 , 𝐸𝑣𝑟 , 𝐶𝑡𝑥𝑟 , 𝑡𝑟 ⟩. For the baseline profile, current-condition validity is the following explicit conjunction: 𝐶𝑢𝑟𝑟𝑒𝑛𝑡𝐶𝑜𝑛𝑑𝑖𝑡𝑖𝑜𝑛𝑠𝐻𝑜𝑙𝑑 (𝑒𝑟𝑐, 𝐵, 𝑅) ⇐⇒ 𝑣𝑒𝑟𝑠𝑖𝑜𝑛(𝐾𝑟 ) = 𝑒𝑟𝑐.𝑟𝑜𝑜𝑡𝑃𝑜𝑙𝑖𝑐𝑦𝑉 𝑒𝑟𝑠𝑖𝑜𝑛 ∧ 𝑣𝑒𝑟𝑠𝑖𝑜𝑛(𝑃𝑟 ) = 𝑒𝑟𝑐.𝑜𝑝𝑒𝑟𝑎𝑡𝑖𝑜𝑛𝑎𝑙𝑃𝑜𝑙𝑖𝑐𝑦𝑉 𝑒𝑟𝑠𝑖𝑜𝑛 ∧ 𝑖𝑑 (𝐸𝑣𝑟 ) = 𝑒𝑟𝑐.𝑒𝑣𝑖𝑑𝑒𝑛𝑐𝑒𝐼𝑑 ∧ 𝑖𝑑 (𝐶𝑡𝑥𝑟 ) = 𝑒𝑟𝑐.𝑐𝑜𝑛𝑡𝑒𝑥𝑡𝐼𝑑 ∧ 𝐵𝑜𝑢𝑛𝑑 (𝐼, 𝑥𝑟 , 𝐶𝑡𝑥𝑟 , 𝑡𝑟 )
(2)
∧ 𝑃𝑒𝑟𝑚𝑖𝑡𝐾𝑟 (𝐼, 𝑥𝑟 , 𝐸𝑣𝑟 , 𝐶𝑡𝑥𝑟 , 𝑡𝑟 ) ∧ 𝑃𝑒𝑟𝑚𝑖𝑡𝑃𝑟 (𝐼, 𝑥𝑟 , 𝐸𝑣𝑟 , 𝐶𝑡𝑥𝑟 , 𝑡𝑟 ) ∧ ∀𝑞 ∈ 𝑄 𝐾 : 𝑆𝑡𝑎𝑡𝑢𝑠 (𝑞, 𝐸𝑣𝑟 , 𝐶𝑡𝑥𝑟 , 𝑡𝑟 ) = 𝑉 𝐴𝐿𝐼 𝐷
𝑖𝑑 (𝜋) = 𝑒𝑟𝑐.𝑑𝑒𝑟𝑖𝑣𝑎𝑡𝑖𝑜𝑛𝐼𝑑.
𝑅𝑒𝑝𝑙𝑎𝑦𝑚 (𝐵) = (𝑑𝑚 , 𝑟𝑚 , 𝜋𝑚 )
∧ ∀𝑞 ∈ 𝑄 𝑃 : 𝑆𝑡𝑎𝑡𝑢𝑠 (𝑞, 𝐸𝑣𝑟 , 𝐶𝑡𝑥𝑟 , 𝑡𝑟 ) = 𝑉 𝐴𝐿𝐼𝐷. The obligation identities and resolution versions are already committed by the verified ERC. An extension may add currentstate predicates only by naming and versioning them in the profile and committing their inputs in the ERC; undeclared resolver state is inadmissible. The grant-state transition relation is:
be replay by conforming implementation 𝑚. Replay is semantically consistent with an ERC when:
𝐼𝑆𝑆𝑈 𝐸𝐷 → {𝐶𝑂𝑁 𝑆𝑈 𝑀𝐸𝐷, 𝐸𝑋 𝑃𝐼𝑅𝐸𝐷, 𝑅𝐸𝑉 𝑂𝐾𝐸𝐷 }.
This equality binds the ERC to the particular supplied derivation. It does not require an independent evaluator to serialize its own derivation identically. Let:
From Intent to Execution Grant: An Execution-Boundary Conformance Profile for High-Risk AI Actions
No transition returns a terminal grant to ISSUED. A nonce contributes to ERC or grant identity. It does not establish this state transition. At-most-once redemption requires an authoritative grant-state transition or a mechanism with equivalent semantics. Revocation and expiry are explicit competing transitions: 𝑅𝑒𝑣𝑜𝑘𝑒
𝑔 : 𝐼𝑆𝑆𝑈 𝐸𝐷 −−−−−→ 𝑔 : 𝑅𝐸𝑉 𝑂𝐾𝐸𝐷, 𝐸𝑥𝑝𝑖𝑟𝑒
𝑔 : 𝐼𝑆𝑆𝑈 𝐸𝐷 −−−−−→ 𝑔 : 𝐸𝑋 𝑃𝐼𝑅𝐸𝐷. All transitions out of ISSUED share one authoritative linearization order. Thus, if Revoke or Expire linearizes before Redemption, R-Success is disabled; if R-Success linearizes first, the later lifecycle operation cannot replace CONSUMED. This supplies a determinate result even when requests overlap in real time [9]. The Redemption guard is defined, rather than left implementationspecific, by:
R-Success for candidate 𝑥𝑟 . Then 𝑖𝑑 (𝑥𝑟 ) = 𝑒𝑟𝑐.𝑐𝑎𝑛𝑑𝑖𝑑𝑎𝑡𝑒𝐼𝑑. Consequently, the declared Redemption Interface cannot use a grant issued for 𝑥 to redeem a decision-relevantly different candidate 𝑥 ′ . Proof sketch. Equation (3) is a premise of R-Success and contains the equality 𝑖𝑑 (𝑥𝑟 ) = 𝑒𝑟𝑐.𝑐𝑎𝑛𝑑𝑖𝑑𝑎𝑡𝑒𝐼𝑑. A mutation of any canonical decision-relevant candidate field changes 𝐶𝑎𝑛𝑜𝑛 𝑣 (𝑥𝑟 ) and hence its commitment, except with a collision excluded by the assumption. Removing the candidate-identity guard admits the recipient-substitution counterexample used in the conformance corpus. The result is scoped to the declared interface and says nothing about alternative effect-producing paths. □ Proposition 2 (Root-policy dominance). Fix a root-policy version 𝐾. If Operational Policy cannot modify 𝑃𝑒𝑟𝑚𝑖𝑡𝐾 , 𝑄 𝐾 , or rootobligation resolution semantics, and if direct predicates and obligations compose conjunctively, then
𝑅𝑒𝑑𝑒𝑒𝑚𝑂𝐾 (𝑔, 𝑒𝑟𝑐, 𝐵, 𝜋, 𝑅) ⇐⇒
𝐴𝑙𝑙𝑜𝑤𝜂 (𝐾, 𝑃) ⊆ 𝐴𝑙𝑙𝑜𝑤𝜂 (𝐾, ∅).
𝑉 𝑒𝑟𝑖 𝑓 𝑦𝐸𝑅𝐶 (𝑒𝑟𝑐, 𝐵, 𝜋) = 𝑉 𝐴𝐿𝐼𝐷 ∧ 𝑒𝑟𝑐.𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛 = 𝐴𝐿𝐿𝑂𝑊 ∧ 𝑠𝑡𝑎𝑡𝑒 (𝑔) = 𝐼𝑆𝑆𝑈 𝐸𝐷 ∧ 𝐺𝑟𝑎𝑛𝑡𝐵𝑜𝑢𝑛𝑑𝑇𝑜 (𝑔, 𝑒𝑟𝑐)
(3)
∧ 𝑖𝑑 (𝑥𝑟 ) = 𝑒𝑟𝑐.𝑐𝑎𝑛𝑑𝑖𝑑𝑎𝑡𝑒𝐼𝑑 ∧ 𝑆𝑐𝑜𝑝𝑒 (𝑔) ⊆ 𝑒𝑟𝑐.𝑎𝑢𝑡ℎ𝑜𝑟𝑖𝑡𝑦𝑆𝑐𝑜𝑝𝑒 ∧ 𝑡𝑟 ∈ 𝑒𝑟𝑐.𝑖𝑛𝑡𝑒𝑟𝑣𝑎𝑙 ∧ 𝐶𝑢𝑟𝑟𝑒𝑛𝑡𝐶𝑜𝑛𝑑𝑖𝑡𝑖𝑜𝑛𝑠𝐻𝑜𝑙𝑑 (𝑒𝑟𝑐, 𝐵, 𝑅). A successful protected transition has the form:
Proof sketch. Membership in 𝐴𝑙𝑙𝑜𝑤𝜂 (𝐾, 𝑃) requires both 𝑅𝑜𝑜𝑡𝑂𝐾𝐾 and 𝑂𝑝𝑒𝑟𝑎𝑡𝑖𝑜𝑛𝑎𝑙𝑂𝐾𝑃 . The empty Operational Policy replaces only the latter conjunct with 𝑡𝑟𝑢𝑒 and removes only 𝑄 𝑃 ; it leaves 𝑅𝑜𝑜𝑡𝑂𝐾𝐾 unchanged. Every member of the first set is therefore a member of the second. Permitting 𝑃 to delete or reinterpret a root obligation would invalidate the argument, which is why the non-weakening premise is explicit. The proposition does not establish that 𝐾 is substantively correct or prevent an authorized replacement of 𝐾. □ Proposition 3 (Evidence-obligation safety). If Γ𝐾 (𝑃, 𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) = (𝐴𝐿𝐿𝑂𝑊 , 𝑟, 𝜋),
𝑅𝑒𝑑𝑒𝑒𝑚𝑂𝐾 (𝑔, 𝑒𝑟𝑐, 𝐵, 𝜋, 𝑅)
𝑠𝑡𝑎𝑡𝑒 (𝑔) = 𝐼𝑆𝑆𝑈 𝐸𝐷
. 𝑅𝑒𝑑𝑒𝑒𝑚 (𝑔,𝑥𝑟 ) ⟨𝑔 : 𝐼𝑆𝑆𝑈 𝐸𝐷, 𝑠⟩ −−−−−−−−−−−→ ⟨𝑔 : 𝐶𝑂𝑁 𝑆𝑈 𝑀𝐸𝐷, Δ(𝑠, 𝑥𝑟 )⟩ (R-Success) The validation predicates, grant consumption, and protected effect must share one logical linearization point with respect to decision-relevant state. A conforming realization may use an atomic transaction, version-conditional commit, transactional state transition, or equivalent mechanism. A validation step followed by an interleavable state change and later effect is not a conforming realization of R-Success. If validation fails, if the grant is not ISSUED, or if linearization cannot be established: 𝑅𝑒𝑑𝑒𝑒𝑚(𝑔, . . .) = 𝐷𝐸𝑁𝑌 .
4.8
Conditional Security Propositions
The following propositions are preservation results over the EBLCore rules. Several are direct consequences of explicit guards; this is intentional because the profile is meant to make those guards testable. Each result states the assumptions on which it depends and the mutation that would falsify the conclusion if the corresponding guard were omitted. Proposition 1 (Exact action binding). Assume collision resistance for 𝐶𝑜𝑚𝑚𝑖𝑡 𝑣 , a verified ERC, and a successful application of
then ∀𝑞 ∈ 𝑄 𝐾 ∪ 𝑄 𝑃 : 𝑆𝑡𝑎𝑡𝑢𝑠 (𝑞, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡) = 𝑉 𝐴𝐿𝐼 𝐷. Proof sketch. The sole positive rule, E-Allow, requires 𝐶𝑜𝑟𝑒𝑂𝐾𝐾 . Its final two conjuncts require VALID for every member of 𝑄 𝐾 and 𝑄 𝑃 . Replacing any required status by UNKNOWN, MISSING, EXPIRED, or CONFLICT falsifies 𝐶𝑜𝑟𝑒𝑂𝐾𝐾 and selects E-Deny under the precedence in Equation (1). The result concerns obligation resolution, not the external truth of an evidence assertion. □ Proposition 4 (Semantic replay consistency). Assume input closure, deterministic canonicalization, deterministic evidence classification, and the fixed failure precedence in Equation (1). For closed bundles under the same profile, 𝐶𝑎𝑛𝑜𝑛 𝑣 (𝐵 1 ) = 𝐶𝑎𝑛𝑜𝑛 𝑣 (𝐵 2 ) =⇒ 𝑑 1 = 𝑑 2 ∧ 𝑟 1 = 𝑟 2 . Each accepted derivation must independently satisfy 𝑉 𝑒𝑟𝑖 𝑓 𝑦𝐷𝑒𝑟𝑖𝑣𝑎𝑡𝑖𝑜𝑛(𝜋𝑖 , 𝐵𝑖 , 𝑑𝑖 , 𝑟𝑖 ) = 𝑡𝑟𝑢𝑒. Serialized derivation equality is not required. Proof sketch. Canonical equality gives identical values for every declared input to the predicates and status functions. Input closure excludes an undeclared clock, resolver, randomness source, or mutable process value. The same predicates therefore fail or succeed, and the fixed total precedence selects the same primary reason. Different encodings may record different valid inference
Wu et al.
structures, so the conclusion is semantic rather than byte-level equality. A hidden clock or implementation-dependent iteration order provides a counterexample if either assumption is removed. □ Proposition 5 (Single-use grant consumption). Assume one authoritative, linearizable grant-state object and terminal states CONSUMED, EXPIRED, and REVOKED. At most one concurrent Redemption of the same grant can apply R-Success and produce the protected effect. Proof sketch. Linearizability totally orders competing state transitions from ISSUED [9]. The first successful Redemption changes the state to CONSUMED; every other Redemption is ordered after that transition and fails the 𝑠𝑡𝑎𝑡𝑒 (𝑔) = 𝐼𝑆𝑆𝑈 𝐸𝐷 premise. If revocation or expiry is first, no Redemption succeeds. A nonce alone would not prove the result because two consumers could accept the same nonce without a shared authoritative transition. □ Proposition 6 (Conditional interface enforcement). Let 𝑃𝑟𝑜𝑡𝑒𝑐𝑡𝑒𝑑𝐸𝑥𝑒𝑐𝑢𝑡𝑒 (𝑥) denote a protected transition through the declared interface. Assume: every such transition requires successful Redemption; the Effector applies only the redeemed candidate; Grant Issuance requires a verified ALLOW ERC; R-Success checks Equation (3); validation, consumption, and effect are linearized; grants cannot be forged or broadened within the model; and participating roles satisfy their declared trust assumptions. Then 𝑃𝑟𝑜𝑡𝑒𝑐𝑡𝑒𝑑𝐸𝑥𝑒𝑐𝑢𝑡𝑒 (𝑥) =⇒ ∃𝐵, 𝜋, 𝑒𝑟𝑐, 𝑔 : 𝑒𝑟𝑐.𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛 = 𝐴𝐿𝐿𝑂𝑊 , 𝑖𝑑 (𝑥) = 𝑒𝑟𝑐.𝑐𝑎𝑛𝑑𝑖𝑑𝑎𝑡𝑒𝐼𝑑, 𝑉 𝑒𝑟𝑖 𝑓 𝑦𝐷𝑒𝑟𝑖𝑣𝑎𝑡𝑖𝑜𝑛(𝜋, 𝐵, 𝐴𝐿𝐿𝑂𝑊 , 𝑒𝑟𝑐.𝑟𝑒𝑎𝑠𝑜𝑛) = 𝑡𝑟𝑢𝑒, 𝑠𝑡𝑎𝑡𝑒 (𝑔) : 𝐼𝑆𝑆𝑈 𝐸𝐷 → 𝐶𝑂𝑁 𝑆𝑈 𝑀𝐸𝐷. Proof sketch. By the complete-mediation assumption for the declared interface, 𝑃𝑟𝑜𝑡𝑒𝑐𝑡𝑒𝑑𝐸𝑥𝑒𝑐𝑢𝑡𝑒 (𝑥) has a successful Redemption witness. The only successful rule is R-Success; expanding its 𝑅𝑒𝑑𝑒𝑒𝑚𝑂𝐾 premise with Equation (3) yields the ERC decision, candidate equality, verified derivation, and state transition in the conclusion. Removing complete mediation admits an alternative-path counterexample, while removing Effector fidelity permits execution of a candidate other than the committed one. Hence the proposition is interface-local and conditional; it does not establish deploymentwide non-bypassability, human-intent correctness, evidence truth, root-policy correctness, or correct external outcomes. □
EBL-Core Conformance Profile and Integration Model 5.1 Conformance Model Overview
7. Grant Issuer; and 8. Effector and Redemption Interface. The principal path is: Candidate Materialization | Adjudication | ERC Generation and Verification | Grant Issuance: state = ISSUED | Linearized Redemption and Consumption | Protected Effect or Denial The Candidate Materializer produces one canonical action containing every field required by the applicable candidate profile. A schema cannot guarantee coverage of unknown real-world effects; candidate-profile completeness and Effector fidelity remain explicit assumptions. The Adjudicator produces a deterministic semantic decision and reason together with a verifiable decision derivation. Different implementations may encode valid derivations differently. The ERC Generator produces a decision-binding releasecondition object. ERC generation does not release execution authority. The ERC Verifier checks the ERC against the original adjudication bundle and supplied derivation. Current-state redemption compatibility is evaluated separately by the Redemption Interface. The Grant Issuer releases authority for the exact candidate and initializes the grant in the ISSUED state. The Redemption Interface verifies current conditions and performs a linearized transition that consumes the grant and releases the protected effect. Whether all effect-producing paths traverse this interface remains a deployment property.
5.2
EBL-Core Input Contract
The Adjudicator consumes: 𝐵 = ⟨𝑝𝑟𝑜 𝑓 𝑖𝑙𝑒𝑉 𝑒𝑟𝑠𝑖𝑜𝑛, 𝐾, 𝑃, 𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡⟩. A conforming candidate 𝑥 denotes exactly one action. It must be fully materialized, schema-valid, deterministically canonicalizable, and complete with respect to all decision-relevant parameters. The policy inputs separately identify:
5
An EBL-Core implementation assigns the following logical roles: 1. Intent Provider; 2. Candidate Materializer; 3. Evidence Resolver; 4. Adjudicator; 5. ERC Generator; 6. ERC Verifier;
𝑄 𝐾 = 𝑂𝑏𝑙𝑖𝑔𝑎𝑡𝑖𝑜𝑛𝑠𝐾 (𝐾, 𝐼, 𝑥, 𝐶𝑡𝑥) and: 𝑄 𝑃 = 𝑂𝑏𝑙𝑖𝑔𝑎𝑡𝑖𝑜𝑛𝑠𝑃 (𝑃, 𝐼, 𝑥, 𝐶𝑡𝑥). The adapter must preserve the origin and semantics of each obligation. Operational-policy processing cannot suppress or reinterpret root-policy obligations. The evidence set 𝐸𝑣 must contain the complete materialized evidence input used to classify 𝑄 𝐾 ∪ 𝑄 𝑃 . Undeclared resolver state cannot affect adjudication.
From Intent to Execution Grant: An Execution-Boundary Conformance Profile for High-Risk AI Actions
The context 𝐶𝑡𝑥 must contain the complete decision-relevant contextual projection. Time 𝑡 remains an explicit input. Input closure requires the result to depend only on 𝐵 and the referenced profile semantics. External observations may occur before adjudication, but their decision-relevant results must be materialized in 𝐸𝑣 or 𝐶𝑡𝑥.
5.3
Adjudicator Conformance Requirements
5.4
ERC Generation, Grant Issuance, and Redemption
Let: 𝑅 = ⟨𝐾𝑟 , 𝑃𝑟 , 𝑥𝑟 , 𝐸𝑣𝑟 , 𝐶𝑡𝑥𝑟 , 𝑡𝑟 ⟩ denote the current redemption inputs. The abstract interfaces are:
5.3.1 Deterministic Semantic Evaluation. For canonically equivalent bundles:
𝐴𝑑 𝑗𝑢𝑑𝑖𝑐𝑎𝑡𝑒 (𝐵) → (𝑑, 𝑟, 𝜋), 𝐺𝑒𝑛𝑒𝑟𝑎𝑡𝑒𝐸𝑅𝐶 (𝐵, 𝑑, 𝑟, 𝜋, 𝑖𝑠𝑠𝑢𝑒𝑟, 𝑛𝑜𝑛𝑐𝑒, 𝑖𝑛𝑡𝑒𝑟𝑣𝑎𝑙) → 𝑒𝑟𝑐,
𝐶𝑎𝑛𝑜𝑛 𝑣 (𝐵 1 ) = 𝐶𝑎𝑛𝑜𝑛 𝑣 (𝐵 2 ), conforming evaluators must produce: 𝑑1 = 𝑑2
and
𝑉 𝑒𝑟𝑖 𝑓 𝑦𝐸𝑅𝐶 (𝑒𝑟𝑐, 𝐵, 𝜋) → {𝑉 𝐴𝐿𝐼𝐷, 𝐼 𝑁𝑉 𝐴𝐿𝐼𝐷 },
𝑟1 = 𝑟2 .
Each derivation must satisfy:
𝐼𝑠𝑠𝑢𝑒𝐺𝑟𝑎𝑛𝑡 (𝑒𝑟𝑐, 𝐵, 𝜋) → 𝑔 | ⊥, and: 𝑅𝑒𝑑𝑒𝑒𝑚(𝑔, 𝑒𝑟𝑐, 𝐵, 𝜋, 𝑅) → {𝐸𝑋 𝐸𝐶𝑈𝑇 𝐸, 𝐷𝐸𝑁𝑌 }.
𝑉 𝑒𝑟𝑖 𝑓 𝑦𝐷𝑒𝑟𝑖𝑣𝑎𝑡𝑖𝑜𝑛(𝜋𝑖 , 𝐵𝑖 , 𝑑𝑖 , 𝑟𝑖 ) = 𝑡𝑟𝑢𝑒. Conformance does not require: 𝑖𝑑 (𝜋 1 ) = 𝑖𝑑 (𝜋2 ). The profile must nevertheless define deterministic semantics for rule resolution, failure priority, evidence-status classification, and unordered inputs. An implementation-specific iteration order cannot alter 𝑑 or 𝑟 . 5.3.2 Side-Effect-Free and Bounded Evaluation. Adjudication must not modify external state, policies, evidence sources, grant state, redemption state, or the protected system. Each profile defines:
5.4.1
ERC Generation. The ERC Generator must bind: • the complete input-bundle commitment; • intent and exact-candidate identities; • actor and authority scope; • root- and operational-policy versions; • 𝑄 𝐾 and 𝑄 𝑃 ; • evidence and context commitments; • adjudication time and validity interval; • decision and reason; • the supplied derivation commitment; • profile and schema versions; • issuer identity; and • a nonce. For an ALLOW ERC:
𝑆𝑡𝑒𝑝𝑠 (Γ, 𝐵) ≤ 𝐵𝑜𝑢𝑛𝑑𝑃𝑟𝑜 𝑓 𝑖𝑙𝑒 (|𝐵|). The present specification defines this obligation without claiming that a particular implementation has already been measured or verified against it.
𝑉 𝑒𝑟𝑖 𝑓 𝑦𝐷𝑒𝑟𝑖𝑣𝑎𝑡𝑖𝑜𝑛(𝜋, 𝐵, 𝐴𝐿𝐿𝑂𝑊 , 𝑟 ) = 𝑡𝑟𝑢𝑒. A DENY ERC may preserve a refusal for verification or diagnosis, but:
5.3.3 Input Validation and Failure Classification. Before positive adjudication, the Adjudicator validates: • profile and schema versions; • canonical representability; • intent and candidate structure; • exact candidate completeness; • policy identities; • separate root and operational obligation sets; and • evidence-obligation structure. Malformed, incomplete, unsupported, or unresolved evaluation cannot produce ALLOW. 5.3.4 No Implicit Repair. Obtaining new evidence, modifying a candidate, replacing a policy, resolving a conflict, or filling a missing parameter creates a new input bundle and requires a new adjudication.
𝑒𝑟𝑐.𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛 = 𝐷𝐸𝑁𝑌 =⇒ 𝐼𝑠𝑠𝑢𝑒𝐺𝑟𝑎𝑛𝑡 (𝑒𝑟𝑐, 𝐵, 𝜋) = ⊥. The nonce distinguishes the ERC instance. It does not implement grant consumption. 5.4.2
ERC Verification. 𝑉 𝑒𝑟𝑖 𝑓 𝑦𝐸𝑅𝐶 (𝑒𝑟𝑐, 𝐵, 𝜋) = 𝑉 𝐴𝐿𝐼 𝐷 only if: • the ERC is well formed; • profile and schema versions are recognized; • all object commitments match 𝐵; • 𝑄 𝐾 and 𝑄 𝑃 are correctly generated and separately identified; • the candidate denotes exactly one complete action; • the issuer is authorized for the recorded scope; • the supplied derivation commitment matches the ERC’s derivationId field; and • the supplied derivation verifies for 𝐵, 𝑒𝑟𝑐.𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛, and 𝑒𝑟𝑐.𝑟𝑒𝑎𝑠𝑜𝑛.
Wu et al.
ERC verification establishes consistency with the original adjudication. It does not establish that current redemption conditions remain valid. 5.4.3
Grant Issuance. A grant may be issued only if:
𝑒𝑟𝑐.𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛 = 𝐴𝐿𝐿𝑂𝑊 ∧ 𝑉 𝑒𝑟𝑖 𝑓 𝑦𝐸𝑅𝐶 (𝑒𝑟𝑐, 𝐵, 𝜋) = 𝑉 𝐴𝐿𝐼𝐷. Issuance creates 𝑔 such that:
linearized from ISSUED determines the terminal state: revocation or expiry first forces Redemption to deny; Redemption first produces CONSUMED, after which revocation or expiry cannot overwrite the result. The EBL-Core baseline is single-candidate and single-use. Bounded candidate sets and multi-use grants require an extension profile.
5.5
𝐺𝑟𝑎𝑛𝑡𝐵𝑜𝑢𝑛𝑑𝑇𝑜 (𝑔, 𝑒𝑟𝑐) = 𝑡𝑟𝑢𝑒, 𝐶𝑎𝑛𝑑𝑖𝑑𝑎𝑡𝑒𝑂 𝑓 (𝑔) = 𝑒𝑟𝑐.𝑐𝑎𝑛𝑑𝑖𝑑𝑎𝑡𝑒𝐼𝑑, 𝑆𝑐𝑜𝑝𝑒 (𝑔) ⊆ 𝑒𝑟𝑐.𝑎𝑢𝑡ℎ𝑜𝑟𝑖𝑡𝑦𝑆𝑐𝑜𝑝𝑒, and: 𝑠𝑡𝑎𝑡𝑒 (𝑔) = 𝐼𝑆𝑆𝑈 𝐸𝐷. The representation of 𝑔 is an implementation choice. An ERC may be embedded in the same credential that represents 𝑔, but the contract and authority-bearing roles remain semantically distinct. 5.4.4 Redemption Verification. Before the protected effect, the Redemption Interface verifies: 𝑉 𝑒𝑟𝑖 𝑓 𝑦𝐸𝑅𝐶 (𝑒𝑟𝑐, 𝐵, 𝜋) = 𝑉 𝐴𝐿𝐼𝐷, 𝐺𝑟𝑎𝑛𝑡𝐵𝑜𝑢𝑛𝑑𝑇𝑜 (𝑔, 𝑒𝑟𝑐), 𝑠𝑡𝑎𝑡𝑒 (𝑔) = 𝐼𝑆𝑆𝑈 𝐸𝐷, 𝑖𝑑 (𝑥𝑟 ) = 𝑒𝑟𝑐.𝑐𝑎𝑛𝑑𝑖𝑑𝑎𝑡𝑒𝐼𝑑, 𝑣𝑒𝑟𝑠𝑖𝑜𝑛(𝐾𝑟 ) = 𝑒𝑟𝑐.𝑟𝑜𝑜𝑡𝑃𝑜𝑙𝑖𝑐𝑦𝑉 𝑒𝑟𝑠𝑖𝑜𝑛, 𝑣𝑒𝑟𝑠𝑖𝑜𝑛(𝑃𝑟 ) = 𝑒𝑟𝑐.𝑜𝑝𝑒𝑟𝑎𝑡𝑖𝑜𝑛𝑎𝑙𝑃𝑜𝑙𝑖𝑐𝑦𝑉 𝑒𝑟𝑠𝑖𝑜𝑛, 𝑡𝑟 ∈ 𝑒𝑟𝑐.𝑣𝑎𝑙𝑖𝑑𝑖𝑡𝑦𝐼𝑛𝑡𝑒𝑟𝑣𝑎𝑙, 𝐶𝑢𝑟𝑟𝑒𝑛𝑡𝐶𝑜𝑛𝑑𝑖𝑡𝑖𝑜𝑛𝑠𝐻𝑜𝑙𝑑 (𝑒𝑟𝑐, 𝐵, 𝑅). For the baseline profile, CurrentConditionsHold expands to the conjunction in Equation (2): exact policy-version equality, equality of committed evidence and context identities, continued intent binding, both policy predicates, and VALID status for every committed obligation. An adapter cannot place an undeclared network lookup, clock, resolver, or policy decision inside this predicate. Extension conditions must be named and versioned by the profile and bound by the ERC. If any condition is false or unresolved, redemption returns DENY. For a successful redemption, validation, the transition 𝐼𝑆𝑆𝑈 𝐸𝐷 → 𝐶𝑂𝑁 𝑆𝑈 𝑀𝐸𝐷, and the protected effect must be linearized. A conforming implementation may realize this requirement through an atomic transaction, version-conditional commit, transactional state transition, or an equivalent mechanism. EBL-Core does not prescribe which mechanism is used. A grant in CONSUMED, EXPIRED, or REVOKED cannot be redeemed. The nonce assists with identity and correlation, but the authoritative grant-state transition supplies replay prevention. Redemption, revocation, and expiry must operate on the same authoritative lifecycle state. When they overlap, the first transition
Worked Example: A Single-Use Transfer Grant
Consider an authenticated treasury request to transfer at most 10,000 USDC from account treasury-01 to the pre-approved recipient beneficiary-alice on mainnet. The Intent Authority emits a structured intent 𝐼𝑇 valid over [1700000000, 1700001000]. The Candidate Materializer resolves the request to exactly one candidate 𝑥𝑇 : transfer 7,500 USDC to that recipient, with a maximum fee of 25 units and authority scope transfer:treasury-01. No recipient, amount, network, or fee remains unresolved. The bundle is well formed, intent binding and both policy predicates hold, and every evidence obligation resolves to VALID. Hence no predicate in the EBL-Core failure sequence is true, and adjudication produces Γ𝐾3 (𝑃17, 𝐼𝑇 , 𝑥𝑇 , 𝐸𝑣𝑇 , 𝐶𝑡𝑥𝑇 , 𝑡) = (𝐴𝐿𝐿𝑂𝑊 , 𝑂𝐾, 𝜋𝑇 ). The supplied derivation 𝜋𝑇 records the input commitments, the separate sets 𝑄 𝐾 = {𝑞 1, 𝑞 2 } and 𝑄 𝑃 = {𝑞 3 }, the three VALID classifications, and the applied E-Allow rule. ERC Generation then creates 𝑒𝑟𝑐𝑇 containing the commitments to 𝐼𝑇 , 𝑥𝑇 , 𝐾3 , 𝑃17 , 𝑄 𝐾 , 𝑄 𝑃 , 𝐸𝑣𝑇 , 𝐶𝑡𝑥𝑇 , 𝑡, 𝜋𝑇 , the effective interval, issuer, and nonce. Verification of 𝑒𝑟𝑐𝑇 does not itself release authority. Separate Grant Issuance creates 𝑔𝑇 in ISSUED, bound to 𝑒𝑟𝑐𝑇 and the candidate commitment 𝑖𝑑 (𝑥𝑇 ). At Redemption, the interface receives the same candidate, policy versions, evidence and context commitments, and a current time inside the effective interval. Equations (2) and (3) hold. A successful linearized transition applies the in-scope effect once and changes 𝑔𝑇 from ISSUED to CONSUMED. Three perturbations expose the bindings. First, changing the recipient to beneficiary-bob changes 𝑖𝑑 (𝑥𝑇 ), so the existing ERC and grant fail exact-candidate validation. Second, redeeming after the approval evidence or effective ERC interval expires makes the relevant obligation non-VALID and disables R-Success. Third, if 32 Redemption requests race on 𝑔𝑇 , the authoritative state object orders them: at most one can observe and consume ISSUED; the rest observe CONSUMED and deny. Section 6.2 reports executable checks of these cases.
5.6
Interoperability with Existing Systems
A capability system may represent 𝑔, but EBL-Core does not redefine delegation or credential transport. If the capability cannot bind the candidate identity, grant state, or redemption conditions, an additional conforming verifier is required. Cross-system replay requires the same semantic decision and reason under equivalent input bundles. Independent implementations may emit different valid derivation encodings, provided that each satisfies:
From Intent to Execution Grant: An Execution-Boundary Conformance Profile for High-Risk AI Actions
Object
Materialized value
Decision-relevant role
Intent 𝐼𝑇
Named actor, source account, asset, recipient set, 10,000-unit maximum, network, scope, and validity window 7,500 USDC; beneficiary-alice; mainnet; maximum fee 25 Amount at most 10,000; USDC and mainnet permitted; account enabled and funded Amount at most 9,000
Defines immutable constraints and permitted refinement for one transfer candidate.
Candidate 𝑥𝑇 Root Policy 𝐾3 Operational Policy 𝑃 17 Evidence 𝐸𝑣𝑇
Allowlist attestation, ledger snapshot, and approval record, each bound to 𝑥𝑇 and current at 𝑡 = 1700000100 Account enabled, balance 10,000, state version ledger-state-42
Context 𝐶𝑡𝑥𝑇
Supplies the exact payload committed by adjudication, ERC Generation, Grant Issuance, and Redemption. Generates 𝑞 1 = recipient allowlisting and 𝑞 2 = sufficient-balance obligations. Generates 𝑞 3 = approval-quorum obligation without changing 𝑞 1 or 𝑞 2 . Resolves 𝑆𝑡𝑎𝑡𝑢𝑠 (𝑞𝑖 , 𝐸𝑣𝑇 , 𝐶𝑡𝑥𝑇 , 𝑡 ) = 𝑉 𝐴𝐿𝐼 𝐷 for 𝑖 ∈ {1, 2, 3}.
Supplies the explicit state projection used by both policy predicates.
Table 2: Complete materialized inputs for the financial-transfer trace. Values are illustrative units and identifiers; they do not describe a production payment deployment.
Existing mechanism
Possible EBL-Core role
Adapter obligation
Cedar, Rego, or XACML
Root or operational policy evaluation
Capability or credential system Provenance or evidence system Agent runtime
Execution-grant representation
Preserve separate root and operational predicates and obligations; expose exact policies, inputs, and results. Bind authority to the exact candidate and ERC, expose grant state, and prevent broader interpretation. Identify assertion, source, scope, freshness, and the root or operational obligation to which the item applies. Produce one complete canonical candidate with no post-adjudication parameter resolution. Verify current conditions and linearize validation, single-use consumption, and the protected transition.
Reference monitor or enforcement point
Evidence production Candidate materialization Redemption boundary
5.7.3 𝑉 𝑒𝑟𝑖 𝑓 𝑦𝐷𝑒𝑟𝑖𝑣𝑎𝑡𝑖𝑜𝑛(𝜋, 𝐵, 𝑑, 𝑟 ) = 𝑡𝑟𝑢𝑒.
• generation and verification of a complete ERC; • exact-candidate grant binding; • initialization of grant state as ISSUED; • validity and current-condition checks; • single-use ISSUED-to-CONSUMED semantics; • rejection of terminal grant states; and • linearized validation, consumption, and protected transition at the declared interface.
Interoperability therefore concerns semantic equivalence and verification at the ERC interface, not byte-identical derivation output or shared internal code.
5.7
Conformance Levels
5.7.1 Level 0: Decision-Compatible. A Level 0 implementation provides an ALLOW or DENY decision, stable primary reason, identified profile version, and fail-closed handling of malformed or unavailable evaluation. It does not provide full execution-release conformance. 5.7.2
Level 1: Action-Bound Adjudication. Level 1 adds: • one canonical candidate identity; • a canonical intent identity; • explicit intent-to-candidate binding; • separate root and operational obligations; • committed policy and input versions; • deterministic semantic decisions and reasons; and • a decision derivation satisfying the profile verification relation. Level 1 does not establish that execution authority is bound to the decision.
Level 2: Release-Contract Conformance. Level 2 adds:
Level 2 is the minimum level for claiming EBL-Core executionrelease conformance. The claim remains scoped to the declared interface and does not establish the absence of alternative effectproducing paths. 5.7.4
Level 3: Independently Replayable Boundary. Level 3 adds: • an independently specified ERC verifier; • complete decision-derivation verification or semantic replay; • a published conformance corpus; • negative, mutation, policy-composition, and concurrentredemption tests; • cross-runtime or cross-implementation evaluation; and • documented equality of semantic decisions and reasons.
Wu et al.
Level 3 does not require byte-identical derivation serialization. It also does not establish evidence truth, correct human intent, root-policy correctness, or deployment-wide non-bypassability.
6
Evaluation and Validation Strategy
Evaluation of EBL-Core requires separating three distinct questions: whether the profile defines precise and testable semantics, whether implementations realize those semantics correctly and efficiently, and whether a particular deployment satisfies the assumptions under which an execution boundary is meaningful. These questions require different forms of evidence. Conformance tests can validate the semantic profile without establishing deployment security, while implementation benchmarks can characterize operational cost without proving complete mediation. This preprint reports a bounded executable validation using the accompanying minimal reference artifact. The artifact instantiates one financial-transfer profile, a reference adjudicator, a separately implemented verifier and Semantic Replay path, canonical schemas, mutation vectors, and an in-memory linearizable grant store. Broader cross-domain evaluation, independently developed implementations, production benchmarks, and deployment experience remain future work.
6.1
Evaluation Goals
The evaluation is organized around four research questions. Q1: Can EBL-Core precisely represent execution-release obligations for high-risk AI actions? This question concerns semantic coverage. An evaluation should determine whether EBL-Core can represent the intent, candidateaction, policy, evidence, context, temporal, and redemption constraints required by representative execution scenarios. A scenario should be considered covered only when its decision-relevant obligations are represented through typed profile objects or explicitly defined extension points. Encoding an obligation solely as uninterpreted free text does not establish semantic coverage. Q2: Can independent implementations produce equivalent decisions from the same semantic inputs? Given the same profile version and canonical input bundle, conforming adjudicators should produce the same decision and reason code. Their Decision Derivations need not be structurally or byteidentical. Each derivation must independently verify against the same inputs, decision, reason-code precedence, and profile rules. Equality of serialized derivations or derivation commitments is required only when a particular test vector supplies that representation as an explicit input, not as a general consequence of determinism. Q3: Does the Execution Release Contract capture obligations that are not otherwise standardized as one object by existing authorization and agent-control mechanisms? This question concerns the residual abstraction addressed by EBL-Core. The evaluation should not ask whether another mechanism is computationally capable of encoding an EBL-Core condition. A sufficiently general policy language can encode many such conditions. Instead, it should determine whether each condition is: 1. native to the mechanism’s documented abstraction; 2. expressible through an explicit adaptation;
3. delegated to an external component; or 4. not represented by the evaluated integration. The relevant result is therefore an obligation mapping, not a ranking of systems. Q4: Can EBL-Core identify execution-boundary and grantlifecycle failures? The evaluation should test candidate, policy, evidence, context, time, derivation, ERC, and grant mutations. It should also test the lifecycle states ISSUED, CONSUMED, EXPIRED, and REVOKED, concurrent Redemption attempts, and the requirement that at most one successful Redemption linearize with the protected effect. These questions evaluate EBL-Core as a semantic conformance profile. They do not measure whether an AI system is aligned, whether its proposed actions are desirable in general, or whether every path to an external effect is mediated.
6.2
Preliminary Reference Artifact
The source package includes an executable artifact written against Python 3.13.4 using only the standard library. It provides two machine-readable schemas, profile-specific deterministic canonicalization and SHA-256 commitments, a reference adjudicator, ERC Generation and Grant Issuance, and an in-memory grant store whose lock is the logical linearization point for the protected test effect. A separate verifier recomputes structural validity, obligation statuses, decision and primary reason, derivation commitments, ERC bindings, and Semantic Replay without calling the adjudicator. The two paths share the declared canonicalization and commitment primitives, so they are not claimed as independently developed implementations. The implementation, schemas, test vectors, retained result, and reproduction instructions are available under anc/ in the arXiv source package. The corpus fixes one financial-transfer bundle and applies positive, negative, boundary, ordering, and adversarial mutations. Table 3 reports the retained run included with the source package. Every static vector checks the expected decision and primary reason, Decision-Derivation Verification, and Semantic Replay. Lifecycle checks cover mutation of a derivation and ERC, denial of Grant Issuance from a DENY ERC, candidate and policy-version changes, terminal states, and duplicate Redemption. During development, the corpus exposed a disagreement over whether an empty target was a structural error or an intent-binding failure; aligning both paths with the declared schema removed the disagreement. This is evidence that reason-code precedence and independent recomputation are testable rather than merely descriptive. The final retained run passed all reported checks. The artifact does not constitute mechanized verification, a production payment implementation, or evidence of complete mediation, and its local timing output is explicitly non-normative.
6.3
Semantic Conformance Evaluation
Let a test input be the closed semantic bundle 𝐵 𝑣 = ⟨𝑣, 𝐾, 𝑃, 𝐼, 𝑥, 𝐸𝑣, 𝐶𝑡𝑥, 𝑡⟩, where 𝑥 is one canonical, fully materialized candidate and 𝑣 is the EBL-Core version. An adjudicator evaluates the bundle as
From Intent to Execution Grant: An Execution-Boundary Conformance Profile for High-Risk AI Actions
Execution Grant
Grant Issuer verified ALLOW
Execution Release Contract (ERC)
Effector verification
commitment
Agent Runtime
decision
Decision Derivation
Redemption Boundary
candidate produces
Intent Authority
policies
Policy Engine
Execution systems
intent
evidence
EBL-Core Adjudication EBL-Core semantic layer
Evidence System
Participating systems EBL-Core does not replace these systems. It defines the semantic contract between them.
Figure 2: EBL-Core as an interoperability contract. Existing agent, intent, policy, evidence, grant, redemption, and effector components retain their own abstractions. EBL-Core specifies the semantic bindings exchanged among them; it does not replace the participating systems. 6.3.1
Input Closure. For
𝐴(𝐵 𝑣 ) = ⟨𝑑, 𝑟, 𝜋⟩. 𝐴(𝐵 𝑣 ) = ⟨𝑑, 𝑟, 𝜋⟩
A conforming verifier checks: and 𝑉 𝑒𝑟𝑖 𝑓 𝑦𝐷𝑒𝑟𝑖𝑣𝑎𝑡𝑖𝑜𝑛(𝐵 𝑣 , 𝑑, 𝑟, 𝜋) = 𝑡𝑟𝑢𝑒. A conformance corpus should contain valid, invalid, boundary, and malformed bundles together with expected decisions, reason codes, derivation-verification conditions, ERC Generation outcomes, Grant Issuance outcomes, and Redemption outcomes.
𝐴(𝐵 𝑣′ ) = ⟨𝑑 ′, 𝑟 ′, 𝜋 ′ ⟩, input closure and determinism require: 𝐶𝑎𝑛𝑜𝑛 𝑣 (𝐵 𝑣 ) = 𝐶𝑎𝑛𝑜𝑛 𝑣 (𝐵 𝑣′ ) =⇒ 𝑑 = 𝑑 ′ ∧ 𝑟 = 𝑟 ′ .
Wu et al.
Validation component
Workload
Observed result
Static conformance corpus
34 canonical, malformed, policy, intent, and evidence-state vectors
Lifecycle and mutation checks
15 ERC, derivation, issuance, binding, expiry, revocation, and consumption checks 100 trials, each with 32 requests for one ISSUED grant (3,200 attempts) 100 two-party races over one authoritative grant state
34/34 matched decision, reason, derivation-verification, and replay oracles. 15/15 matched the specified outcome.
Concurrent Redemption Revoke–Redeem race
Exactly one successful Redemption and one protected test effect per trial. 100/100 ended in one valid terminal outcome with no effect after revocation.
Table 3: Preliminary executable validation for the included financial-transfer profile. Results establish behavior only for the artifact, environment, and test oracles described here.
They do not require 𝜋 = 𝜋 ′ . Instead, both supplied derivations must satisfy: 𝑉 𝑒𝑟𝑖 𝑓 𝑦𝐷𝑒𝑟𝑖𝑣𝑎𝑡𝑖𝑜𝑛(𝐵 𝑣 , 𝑑, 𝑟, 𝜋) = 𝑡𝑟𝑢𝑒 and 𝑉 𝑒𝑟𝑖 𝑓 𝑦𝐷𝑒𝑟𝑖𝑣𝑎𝑡𝑖𝑜𝑛(𝐵 𝑣′ , 𝑑 ′, 𝑟 ′, 𝜋 ′ ) = 𝑡𝑟𝑢𝑒. A conforming adjudicator must not obtain decision-relevant information from undeclared clocks, mutable process state, network lookups, or implementation-local defaults. Such information must first be materialized in the closed bundle. Cross-implementation comparison should include: • decision equality; • reason-code equality under the specified precedence rules; • acceptance of the same canonical inputs; • rejection of the same malformed inputs; • successful verification of every accepted Decision Derivation; and • compatible ERC verification and lifecycle outcomes. The comparison must not require byte-identical Decision Derivations. 6.3.2 Intent-binding tests. Intent-binding vectors should include both permitted refinements and prohibited expansions. Valid cases should cover: • specialization of parameters within an authorized range; • selection of exactly one resource from a finite set explicitly encoded in the trusted intent, followed by materialization of that selected resource as the single canonical candidate; • reduction of an amount, duration, or effect scope; • selection of an explicitly permitted target; and • materialization of implementation details that do not alter the authorized effect. Invalid cases should cover: • substitution of a different recipient or target; • expansion of the affected resource set; • privilege escalation; • increase of financial, temporal, or physical effect; • substitution of an approval issued for another intent; • use of an approver outside the required authority scope; and
• reinterpretation of an ambiguous intent in a more permissive direction. A decision for one member of an intent-authorized set does not authorize an unspecified member at Redemption. Any mutation that changes the canonical candidate after ERC Generation requires a new adjudication. 6.3.3 Evidence-State Tests. For each obligation in 𝑄 𝐾 ∪ 𝑄 𝑃 , the corpus should exercise:
{VALID, UNKNOWN, MISSING, EXPIRED, CONFLICT}. Only VALID may discharge a positive obligation. UNKNOWN, MISSING, EXPIRED, and CONFLICT must not produce ALLOW for the candidate under adjudication. If a system wishes to propose a different reduced-risk or recovery operation, it must materialize that operation as a new canonical candidate and adjudicate it under the applicable policies and obligations. The corpus should additionally test: • evidence with the wrong type; • evidence supplied by an inadmissible provider; • evidence bound to another intent or candidate; • evidence at both sides of its validity boundary; • conflicting records from multiple providers; • equivalent evidence inputs in different representational orders; • undeclared evidence-resolver state; and • evidence that expires between adjudication and Redemption. These tests evaluate obligation resolution and binding. They do not establish that an evidence provider’s assertion is true. 6.3.4 Policy-Composition Tests. Policy evaluation should test three distinct properties. First, root-policy dominance requires that Operational Policy neither alter the Root Policy predicate nor remove, weaken, rename, or reinterpret 𝑄 𝐾 . An Operational Policy permission cannot override a Root Policy denial. Second, conjunctive rule addition should be tested by adding an Operational Policy restriction and confirming that the admitted candidate set does not expand. The resulting operational obligations must be added through 𝑄 𝑃 , without modifying 𝑄 𝐾 .
From Intent to Execution Grant: An Execution-Boundary Conformance Profile for High-Risk AI Actions
Third, policy-version evolution should be tested through the separately defined compatibility relation 𝐶𝑜𝑚𝑝𝑎𝑡𝐾 (𝑃𝑜𝑙𝑑 , 𝑃𝑛𝑒𝑤 ). Version order, naming, or the presence of additional rules does not establish compatibility. Even when a change is shown to be nonexpanding under fixed 𝐾, compatibility does not automatically preserve an existing grant. Baseline ERC and grant reuse requires exact policy-version equality. A Root Policy change requires new adjudication. The corpus should therefore include: • an Operational Policy that attempts to permit a Root Policy denial; • deletion or reinterpretation of an obligation in 𝑄 𝐾 ; • addition of an operational restriction and corresponding 𝑄𝑃 ; • an Operational Policy update that expands the permitted set; • a non-expanding update satisfying the accepted compatibility procedure; • an exact policy-version mismatch at ERC verification or Redemption; • an attempted reuse of a grant after a compatible Operational Policy update; • a Root Policy version change; and • policies exceeding the profile’s declared structural or evaluation bounds. Unsupported or out-of-bounds policies must be rejected explicitly rather than evaluated through implementation-dependent behavior.
6.4
Adversarial Mutation Evaluation
Adversarial mutation testing begins with a valid trace:
𝜏 = ⟨𝐵, 𝑑, 𝑟, 𝜋, 𝑒𝑟𝑐, 𝑔, 𝑠𝑡𝑎𝑡𝑒 (𝑔)⟩, where 𝐵 contains one canonical candidate, the ERC verifies, and 𝑔 is in the ISSUED state. A mutation changes one decision-relevant component while holding the others constant. The test oracle then evaluates the mutation at adjudication, ERC verification, Grant Issuance, or Redemption, according to when it occurs. The baseline profile permits one successful Redemption for a grant instance. The mutation corpus must not use a reusable or bounded-use grant as its baseline. A second Redemption attempt returns DENY, including when the attempts overlap in time. The principal metrics are: • agreement with the expected decision or lifecycle outcome; • reason-code correctness; • detection stage; • whether re-adjudication is required; • false acceptance of a decision-relevant mutation; • false rejection of representations declared canonically equivalent; and • the number of successful effects produced by concurrent attempts against one grant.
6.5
Baseline Abstraction Comparison
Table 1 provides the completed qualitative mapping for six close baselines. It uses the same native, adapted, external, and unestablished categories proposed by the evaluation design and gives each baseline credit for its documented primary abstraction. The result supports a limited positioning claim: the mandatory EBL-Core contract is not native as a whole to any compared abstraction. It does not show that those mechanisms are unable to express the conditions, nor does it establish that an EBL-Core implementation is more secure or efficient. The current mapping is literature-based rather than adapterbased. A stronger evaluation requires concrete Cedar, Rego, capability, and agent-runtime adapters applied to the same conformance traces. Such work should record which guarantees are inherited from the substrate and which are supplied by wrapper code, then test cross-implementation ERC and Redemption outcomes. The included artifact does not yet perform this adapter comparison.
6.6
Scenario-Based Evaluation
Section 5.5 and the accompanying corpus instantiate one complete financial-operation trace. Extending the same evaluation to infrastructure, deployment, disclosure, and physical-actuation profiles remains future work. Each additional scenario should provide: 1. a structured intent; 2. one canonical, fully materialized candidate action; 3. versioned Root and Operational Policies; 4. separately identified 𝑄 𝐾 and 𝑄 𝑃 ; 5. complete typed evidence, explicit context, and explicit time; 6. an expected decision, reason code, and verifiable Decision Derivation; 7. the expected ERC Generation outcome; 8. Grant Issuance and Redemption outcomes for verified ALLOW cases; and 9. adjudication-time, ERC-time, and Redemption-time mutations. The broader corpus is intended to contain the following scenarios. Each future scenario should include at least one permitted trace, denials for all relevant non-VALID obligation states, a Root Policy denial, an Operational Policy restriction, mutations after ERC Generation, and—where a grant is issued—lifecycle and concurrency tests after Grant Issuance. Ambiguities that cannot be represented without application-specific semantics should be recorded as profile gaps or extension requirements rather than resolved through unstated evaluator behavior. Scenario coverage would show that the same conformance abstraction applies across several effect domains. It would not establish that EBL-Core captures every domain-specific safety property or guarantees a safe real-world outcome.
6.7
Performance-Evaluation Scope
Performance is a property of an implementation rather than the semantic definition. The included artifact can emit indicative local timings, but the retained validation result and the claims in this paper do not depend on them. A standard-library Python model, one profile, and an in-memory store do not provide a meaningful
Wu et al.
Mutation class
Example
Required response
Candidate mutation
A transfer to Alice is changed to a transfer to Bob.
Evidence mutation Policy mutation
Evidence is replaced, expires, or is rebound after adjudication. A Root or Operational Policy version changes.
Reject the existing decision, ERC, and grant binding; require new adjudication. Reject the existing commitment or require new adjudication.
Obligation mutation
𝑄 𝐾 is removed or reinterpreted, or 𝑄 𝑃 changes.
Context mutation
A balance, permission, device state, environment, or risk classification changes. A step, premise, rule identifier, or conclusion in 𝜋 changes.
Derivation mutation ERC substitution Grant-state mutation Concurrent Redemption
An ERC is presented with a different candidate, bundle, issuer, or grant. A CONSUMED, EXPIRED, or REVOKED grant is presented as usable. Two requests redeem the same ISSUED grant concurrently.
Reject on baseline version mismatch; 𝐶𝑜𝑚𝑝𝑎𝑡𝐾 does not automatically preserve the grant. Reject; obligation identity and resolution semantics are decision-relevant. Deny when the committed version or current-state predicate no longer holds. Reject unless the resulting Decision Derivation independently verifies. Reject the inconsistent binding chain. Deny; terminal states cannot return to ISSUED.
Check-effect race
Decision-relevant state changes between validation and effect.
At most one request may complete the linearized ISSUED-to-CONSUMED transition and protected effect. Deny unless validation, state transition, and effect can be linearized.
Scenario
Candidate-action binding
Representative obligations and failure probes
Financial operation
Exact source account, asset, amount, recipient, network, and transaction parameters
Infrastructure change
Exact plan or configuration digest, target resources, environment, and intended transition
Software deployment
Exact artifact digest, service, release configuration, and destination environment
Data disclosure
Exact data fields, recipient, channel, purpose, and disclosure operation
Physical actuation
Exact command, device, parameters, duration, and actuation interface
Approval authority and validity, balance evidence, amount limits, recipient substitution, fee or network changes, and duplicate redemption Change window, operator scope, pre-state commitment, rollback readiness, target expansion, and production-state drift Artifact provenance, approval scope, environment constraints, canary or rollback conditions, artifact substitution, and approval expiry Recipient authority, data classification, scope limitation, context-dependent restrictions, field expansion, and channel substitution Device state, safety envelope, operator authority, stale sensor evidence, parameter expansion, and delayed redemption
production-performance baseline. Operational measurements for production-oriented implementations should therefore be reported separately from semantic conformance results. The evaluation should vary policy size, the number of obligations in 𝑄 𝐾 and 𝑄 𝑃 , evidence-set size, candidate complexity, context size, and Decision Derivation depth. It should separately measure canonicalization, adjudication, derivation construction, ERC Generation, cryptographic operations, Decision-Derivation Verification, Grant Issuance, and Redemption. Such an evaluation should include: • adjudication latency distributions; • serialized ERC and Decision Derivation sizes; • Decision-Derivation Verification latency; • Semantic Replay cost; • Grant Issuance and Redemption latency; • peak and steady-state memory use; • scaling with policy rules and Evidence Obligations; and
• observed and analytically derived worst-case evaluation steps. Decision-Derivation Verification checks whether a supplied derivation supports the committed result under the applicable rules. Semantic Replay reconstructs the decision from the committed semantic inputs. These operations should be measured independently. External evidence acquisition should be excluded from adjudication latency unless it is explicitly part of the implementation under test. Performance comparisons should also match semantic work: an EBL-Core path that generates and verifies an ERC should not be compared directly with a baseline invocation that returns only a Boolean decision. No universal latency or throughput threshold follows from EBLCore. Acceptable operational bounds depend on the Effector domain, while termination and profile-defined evaluation limits remain conformance requirements.
From Intent to Execution Grant: An Execution-Boundary Conformance Profile for High-Risk AI Actions
6.8
Artifact Status and Roadmap
The current package completes a bounded subset of the artifact plan: machine-readable schemas, profile-specific canonicalization and commitments, one deterministic reference adjudicator, a separate verifier and Semantic Replay path, a mutation corpus, and lifecycle and concurrency tests for one financial-transfer profile. It is intended as an executable specification and test oracle, not as a production security component. Because the adjudicator and verifier share canonicalization and commitment primitives and were developed in the same artifact, the package does not claim implementation independence. The next validation stages are independently developed adjudicators and verifiers, additional domain profiles, cross-implementation vectors, and adapters for representative authorization engines, agent runtimes, proof systems, and capability mechanisms. Each adapter should identify which required semantic properties are native, adapted, external, or unestablished. Performance characterization, mechanized correspondence between the formal rules and executable model, and production deployment remain separate stages requiring stronger evidence, Effector integration, authority analysis, and bypass evaluation.
6.9
Limitations
The proposed evaluation cannot establish the following properties: • that a natural-language instruction was translated into the correct trusted intent; • that an evidence provider’s assertion is true; • that every execution path in a deployment passes through the designated boundary; • that the root policy is complete or substantively correct; • that arbitrary deployments provide complete mediation; • that issuer keys, policy authorities, or evidence providers are operationally uncompromised; or • that an authorized command produces the intended physical or external outcome. Mutation testing can show that the specified boundary rejects tested classes of changed inputs. It cannot establish the absence of hidden Effectors, side channels, unmodeled state, or alternative authority paths. Decision-Derivation Verification and Semantic Replay can establish how a decision follows from committed inputs under the profile semantics; neither establishes that those inputs accurately represent the external world. The evidence required for each claim category must therefore remain explicit: Under these limitations, EBL-Core remains testable as a conformance profile. Its semantic properties can be evaluated through canonical inputs, decision and reason-code agreement, binding checks, Decision-Derivation Verification, lifecycle tests, and Semantic Replay. Implementation claims require executable artifacts and measurements, while deployment-security claims remain conditional on explicit authority, trust, Effector-fidelity, and mediation assumptions.
7
Discussion
EBL-Core defines a conformance profile connecting adjudication to the release and Redemption of action-scoped execution authority.
Its contribution is narrower than a complete authorization architecture or AI safety system. This section clarifies the distinct semantic roles in that profile and the deployment assumptions under which they are meaningful.
7.1
EBL-Core Is Complementary to Authorization, Not a Replacement
Authorization mechanisms can evaluate both broad permission classes and highly specific structured requests. EBL-Core does not distinguish itself by assuming that authorization is limited to coarsegrained decisions. Instead, it asks whether an integration preserves a prescribed release-and-redemption contract for one canonical candidate. The execution-boundary question is: What minimum semantic release-and-redemption contract must hold before one canonical, fully materialized AI-generated candidate may receive actionscoped execution authority? Cedar, OPA/Rego, XACML, capability systems, and other mechanisms may supply policy evaluation or authority-management substrates. An EBL-Core integration may invoke them during adjudication and incorporate their results into a Decision Derivation. The residual contract jointly binds the established intent, canonical candidate, Root and Operational Policy versions, 𝑄 𝐾 , 𝑄 𝑃 , evidence, context, time, decision, and Decision Derivation. It then distinguishes ERC Generation, Grant Issuance, and Redemption. EBL-Core should consequently be evaluated by whether implementations preserve these bindings and lifecycle roles, not by whether it replaces the expressiveness of existing authorization systems.
7.2
ERC, Execution Grant, and Redemption Are Distinct Semantic Roles
An Execution Release Contract is a decision-binding releasecondition object. It commits to an adjudication result and the conditions under which that result may support the release and Redemption of authority. It is not inherently authority-bearing. An Execution Grant represents the action-scoped execution authority released by a Grant Issuer from a verified ALLOW ERC. Under the baseline profile, it is bound to one canonical candidate, begins in ISSUED, and can support at most one successful Redemption. Redemption is the governed operation that verifies the ERC, Decision Derivation, candidate binding, current conditions, authority scope, validity interval, and grant state. Successful Redemption linearizes validation, the protected effect, and the transition from ISSUED to CONSUMED. A deployment may encode an ERC and an Execution Grant in the same transport envelope or cryptographic credential. A conforming implementation must nevertheless preserve their distinct semantic roles: the ERC records release conditions, the grant represents released authority, and Redemption governs its exercise. An ALLOW ERC asserts that the committed candidate satisfied the profile’s adjudication conditions. The ERC permits an independent verifier to check that assertion; it does not itself establish that Grant Issuance occurred. Possession of either an ERC or grant also
Wu et al.
Claim category
Appropriate validation evidence
What the evidence does not establish
Semantic conformance
Formal definitions, canonical vectors, differential evaluation, and derivation verification Mutation tests, performance measurements, resource bounds, and verifier independence Architecture review, effector integration, authority configuration, key management, and bypass analysis
Truth of inputs or complete mediation
Claim area
EBL-Core defines
EBL-Core does not establish
Intent binding
A relation between a trusted intent object and one canonical candidate Commitments binding adjudication, ERC, grant, and Redemption to the same candidate Obligation-relative states, bindings, freshness, and conflict handling Root-policy dominance, 𝑄 𝐾 /𝑄 𝑃 separation, conjunctive addition, and version rules Deterministic decision and reason-code semantics with Decision-Derivation Verification A decision-binding release-condition object Grant Issuance from a verified ALLOW ERC Single-use grant states and linearized validation, consumption, and protected effect A basis for relating release decisions to separately collected evidence Semantic properties required of conforming implementations under stated assumptions A constrained interface between proposed actions and execution authority
Correct understanding of natural-language or human intent
Implementation behavior Deployment security
Candidate identity Evidence Policy Decision ERC Authority release Redemption Outcome Security AI safety
Correctness of policies or external providers Universal safety outside the evaluated deployment
That the candidate is beneficial, complete, or error-free External truth, completeness, or provider honesty Policy correctness or secure Root Policy administration Correctness of unmodeled inputs or trusted authorities An inherently authority-bearing token or proof of execution A new general-purpose capability primitive Universal mediation or faithful execution by every Effector Proof that an external effect occurred or had the intended result Deployment security without authority, key, Effector, and bypass analysis General alignment, safe planning, or universal prevention of harmful actions
Table 4: Summary of EBL-Core claim boundaries. The profile specifies conditional semantic properties, while deployment and external-world claims require additional evidence.
does not establish successful Redemption, faithful execution, or an external outcome. Those claims require separate runtime and evidentiary support.
7.3
Intent Limitations
EBL-Core does not solve natural-language intent understanding. Its trusted semantic boundary begins after an Intent Authority has produced a structured intent object. The Intent Authority may obtain that object from a human instruction, workflow definition, approved plan, organizational process, or another trusted source. Determining whether this translation accurately captures a person’s actual intention is outside the EBL-Core adjudication model. Under EBL-Core semantics, a candidate accepted for Redemption must have the same canonical identity as the candidate committed by the verified ERC and Execution Grant. If the Effector faithfully realizes that candidate and the protected effect is reachable only through the governed interface, the resulting operation corresponds to the committed candidate. Effector fidelity and exclusive mediation are deployment assumptions. The corresponding semantic statement is:
If Redemption succeeds, the candidate accepted by the Redemption Interface is bound to the trusted intent object under the specified Bound relation. This does not establish that the intent object correctly represents a human’s actual intention or that the Effector produced the intended external outcome. For example, an intent object may correctly bind a payment to a named recipient while still containing a recipient selected through an erroneous upstream interpretation. EBL-Core can detect later substitution of that recipient, but it cannot determine that the original selection was mistaken unless such information is supplied through policy, evidence, or a corrected intent object. This distinction is important in AI-agent safety analysis. Intent binding constrains execution relative to a trusted representation; it does not establish the semantic correctness of that representation.
7.4
Evidence Limitations
EBL-Core specifies evidence identity, type, source admissibility, binding, freshness, validity intervals, conflict handling, and obligation resolution. It distinguishes VALID, UNKNOWN, MISSING, EXPIRED,
From Intent to Execution Grant: An Execution-Boundary Conformance Profile for High-Risk AI Actions
and CONFLICT, and prohibits a non-VALID state from discharging a positive obligation in 𝑄 𝐾 ∪ 𝑄 𝑃 . These semantics do not establish evidence truth. EBL-Core cannot determine that a provider is honest, a sensor is accurate, an approval was informed, or every relevant fact was observed. Such claims require provider trust, measurement integrity, authority analysis, and domain-specific validation. Execution-lineage, provenance, and outcome-verification systems address the complementary question of what evidence supports claims about an execution and its result. EBL-Core instead classifies supplied evidence against declared obligations before authority release. A conforming implementation may consume compatible provenance or attestation records, but VALID means only that a record discharges a specified obligation under the declared resolution semantics.
7.5
Deployment Assumptions and Complete Mediation
A semantic requirement and a deployment property must be distinguished. The relevant semantic requirement is: A conforming redemption requires a valid execution grant whose bindings and redemption conditions hold. The corresponding deployment property is: Every path capable of producing the protected external effect requires such a grant. EBL-Core specifies the former. Establishing the latter requires analysis of the deployed architecture. A conforming adjudicator and verifier do not prevent an agent from reaching an unmediated administrative interface, invoking an alternative tool, using an independently held credential, or communicating with a component that does not enforce the grant. Nor does the profile prove that all signing keys are protected or that every Intent Authority, Policy Authority, Evidence Provider, Grant Issuer, and Effector behaves correctly. Complete mediation therefore depends on the placement and authority of the execution boundary. A deployment must identify all components capable of producing the protected effect, restrict alternative authority paths, and ensure that effectors validate grants before acting. Hardware-backed boundaries or isolated execution environments may strengthen these assumptions, but they do not follow from the EBL-Core semantics alone. Claims about an EBL-Core deployment must consequently state: • which effects are considered protected; • which effectors can produce those effects; • where grants are validated; • which components and keys are trusted; • which alternative authority paths have been excluded; and • which failures remain outside the model. Global non-bypassability is not a claim of this work.
7.6
Adjacent Analytical Boundaries
EBL-Core does not determine which components, credentials, administrators, or coalitions can reach a protected effect through
ordinary, recovery, update, or alternative paths. That is an authoritytopology and bypass-analysis problem. The Execution Grant is a semantic object in the declared release lifecycle; its presence does not prove that the deployed architecture makes the grant causally necessary. Nor does EBL-Core establish execution lineage or terminal outcomes. Provenance and outcome-verification mechanisms may supply evidence consumed by adjudication or retained after Redemption, but their production, completeness, and truth properties require separate analysis. Conversely, those mechanisms do not determine whether a candidate satisfied the release contract at decision time. The profile is self-contained at these interfaces: it defines the authority scope, evidence obligations, candidate, policies, ERC, grant, and Redemption predicates needed for its own conformance claims. Authority-topology and execution-lineage analyses can strengthen deployment evidence without becoming prerequisites for the core semantics.
7.7
Research Implications
If the execution-release abstraction proves useful across implementations, future work can extend the included schemas, adjudicator, verifier, and corpus into interoperable ERC encodings and adapters for established policy and capability systems. Independently developed implementations would permit stronger differential tests than the two code paths in the current artifact. Mechanized semantics could examine determinism, root-policy dominance, evidence-state treatment, intent refinement, version compatibility, and lifecycle preservation. Domain profiles for infrastructure, disclosure, deployment, and physical actuation could refine evidence obligations and reason codes without weakening the mandatory bindings. Runtime or hardware-backed integration may strengthen key protection, mediation, and Effector assumptions; those mechanisms alter deployment assurance rather than the semantic contract.
8
Conclusion
AI agents increasingly move from generating information to proposing actions that can modify infrastructure, deploy software, transfer assets, disclose information, or actuate physical systems. Authorization systems, policy engines, runtime monitors, provenance mechanisms, and agent guardrails provide important foundations for governing such actions. The interfaces among these mechanisms, however, do not necessarily impose the same semantic conditions on the final transition from one candidate action to execution authority. This paper defines EBL-Core, an execution-boundary conformance profile that binds a trusted intent object, one canonical and fully materialized candidate, versioned Root and Operational Policies, 𝑄 𝐾 and 𝑄 𝑃 , typed evidence, decision-relevant context, explicit time, and a verifiable Decision Derivation through an Execution Release Contract. The ERC is a decision-binding release-condition object rather than inherently authority-bearing. A verified ALLOW ERC may support separate Grant Issuance, while Redemption governs whether the resulting action-scoped authority can be exercised.
Wu et al.
EBL-Core defines semantic properties required of conforming implementations, including candidate binding, root-policy dominance, Evidence Obligation handling, deterministic adjudication, Decision-Derivation Verification, and single-use linearized Redemption. These properties do not establish correct humanintent interpretation, evidence truth, universal mediation, global non-bypassability, faithful Effector behavior, or correct external outcomes. Such claims remain conditional on the deployment architecture and stated trust assumptions. Future work can extend the included executable specification with independently developed adjudicators and verifiers, ERC interoperability experiments, broader conformance suites, integration adapters, and additional domain-specific profiles. These artifacts may provide a foundation for evaluating execution-release semantics across heterogeneous AI-agent systems. The paper defines a semantic contract for when and why an AI-generated action may receive execution authority under explicit assumptions.
References [1] James P. Anderson. 1972. Computer Security Technology Planning Study. Technical Report ESD-TR-73-51. Electronic Systems Division, Air Force Systems Command. [2] Lujo Bauer, Michael A. Schneider, and Edward W. Felten. 2001. A Proof-Carrying Authorization System. Technical Report TR-638-01. Department of Computer Science, Princeton University. https://www.cs.princeton.edu/research/techreps/ 638 [3] Arnar Birgisson, Joe Gibbs Politz, Úlfar Erlingsson, Ankur Taly, Michael Vrable, and Mark Lentczner. 2014. Macaroons: Cookies with Contextual Caveats for Decentralized Authorization in the Cloud. In Proceedings of the Network and Distributed System Security Symposium. Internet Society, San Diego, CA, USA, 15 pages. doi:10.14722/ndss.2014.23265 [4] Henk Birkholz, Dave Thaler, Michael Richardson, Ned Smith, and Wei Pan. 2023. Remote ATtestation ProcedureS (RATS) Architecture. RFC 9334. Internet Engineering Task Force. doi:10.17487/RFC9334 [5] Joseph W. Cutler, Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, Eleftherios Ioannidis, John Kastner, Anwar Mamat, Darin McAdams, Matt McCutchen, Neha Rungta, Emina Torlak, and Andrew Wells. 2024. Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization (Extended Version). arXiv:2403.04651 [cs.CR] doi:10.48550/arXiv. 2403.04651 [6] Jack B. Dennis and Earl C. Van Horn. 1966. Programming Semantics for Multiprogrammed Computations. Commun. ACM 9, 3 (1966), 143–155. doi:10.1145/ 365230.365252 [7] Marcelo Fernandez. 2026. Atomic Decision Boundaries: A Structural Requirement for Guaranteeing Execution-Time Admissibility in Autonomous Systems. arXiv:2604.17511 [cs.LO] doi:10.48550/arXiv.2604.17511 [8] Deepak Garg and Frank Pfenning. 2010. A Proof-Carrying File System. In 2010 IEEE Symposium on Security and Privacy. IEEE, Oakland, CA, USA, 349–364. doi:10.1109/SP.2010.28
[9] Maurice P. Herlihy and Jeannette M. Wing. 1990. Linearizability: A Correctness Condition for Concurrent Objects. ACM Transactions on Programming Languages and Systems 12, 3 (1990), 463–492. doi:10.1145/78969.78972 [10] Kerianne Hobbs, Mark Mote, Matthew Abate, Samuel Coogan, and Eric Feron. 2023. Run Time Assurance for Safety-Critical Systems: An Introduction to Safety Filtering Approaches for Complex Control Systems. IEEE Control Systems Magazine 43, 2 (April 2023), 28–65. doi:10.1109/MCS.2023.3234380 Preprint: arXiv:2110.03506. [11] Vincent C. Hu, David Ferraiolo, D. Richard Kuhn, Adam Schnitzer, Kenneth Sandlin, Robert Miller, and Karen Scarfone. 2014. Guide to Attribute Based Access Control (ABAC) Definition and Considerations. Technical Report NIST Special Publication 800-162. National Institute of Standards and Technology. doi:10.6028/NIST.SP.800-162 Updated February 2019. [12] Yanming Liu, Xinyue Peng, Jiannan Cao, Xinyi Wang, Songhang Deng, Jintao Chen, Jianwei Yin, and Xuhong Zhang. 2026. ToolGate: Contract-Grounded and Verified Tool Execution for LLMs. arXiv:2601.04688 [cs.CL] doi:10.48550/arXiv. 2601.04688 [13] OASIS XACML Technical Committee. 2013. eXtensible Access Control Markup Language (XACML) Version 3.0. OASIS Standard. OASIS. https://docs.oasisopen.org/xacml/3.0/xacml-3.0-core-spec-os-en.html [14] Open Policy Agent Authors. 2026. Open Policy Agent: Policy Language Documentation. https://www.openpolicyagent.org/docs/policy-language. Accessed 2026-09-10. [15] Nils Palumbo, Sarthak Choudhary, Jihye Choi, Guy Amir, Prasad Chalasani, and Somesh Jha. 2026. Formal Policy Enforcement for Real-World Agentic Systems. arXiv:2602.16708 [cs.CR] doi:10.48550/arXiv.2602.16708 [16] Jaehong Park and Ravi Sandhu. 2004. The UCONABC Usage Control Model. ACM Transactions on Information and System Security 7, 1 (2004), 128–174. doi:10. 1145/984334.984339 [17] Jose German Rivera, Alejandro Andres Danylyszyn, Charles B. Weinstock, Lui R. Sha, and Michael J. Gagliardi. 1996. An Architectural Description of the Simplex Architecture. Technical Report CMU/SEI-96-TR-006. Software Engineering Institute, Carnegie Mellon University. https://www.sei.cmu.edu/library/an-architecturaldescription-of-the-simplex-architecture/ [18] Anders Rundgren, Bradley Jordan, and Samuel Erdtman. 2020. JSON Canonicalization Scheme (JCS). RFC 8785. Internet Engineering Task Force. doi:10.17487/ RFC8785 [19] Jerome H. Saltzer and Michael D. Schroeder. 1975. The Protection of Information in Computer Systems. Proc. IEEE 63, 9 (1975), 1278–1308. doi:10.1109/PROC.1975. 9939 [20] Fred B. Schneider. 2000. Enforceable Security Policies. ACM Transactions on Information and System Security 3, 1 (2000), 30–50. doi:10.1145/353323.353382 [21] Tianneng Shi, Jingxuan He, Zhun Wang, Hongwei Li, Linyu Wu, Wenbo Guo, and Dawn Song. 2025. Progent: Securing AI Agents with Privilege Control. arXiv:2504.11703 [cs.CR] doi:10.48550/arXiv.2504.11703 [22] W3C Provenance Working Group. 2013. PROV-DM: The PROV Data Model. W3C Recommendation. World Wide Web Consortium. https://www.w3.org/TR/provdm/ [23] Haoyu Wang, Christopher M. Poskitt, and Jun Sun. 2025. AgentSpec: Customizable Runtime Enforcement for Safe and Reliable LLM Agents. arXiv:2503.18666 [cs.AI] doi:10.48550/arXiv.2503.18666 [24] Zexun Wang. 2026. Proof-Carrying Agent Actions: Model-Agnostic Runtime Governance for Heterogeneous Agent Systems. arXiv:2606.04104 [cs.SE] doi:10. 48550/arXiv.2606.04104 [25] Genliang Zhu and Chu Wang. 2026. Intent-Governed Tool Authorization for AI Agents. arXiv:2606.22916 [cs.AI] doi:10.48550/arXiv.2606.22916