Proof-Carrying Agent Runtime: A Bounded Architecture and Specification

An agent can explain why a refund is appropriate and still refund the wrong account. A reviewer can approve the correct account, then an executor can submit different arguments. A complete transcript can preserve both mistakes without preventing either.

The useful ambition behind a proof-carrying agent runtime is to make each external effect depend on independently checkable authorization evidence, bound to the operation actually dispatched.

The word proof requires discipline. This article proposes a bounded architecture and a formal specification sketch. It does not present a mechanically verified runtime, a new ContextOS wire schema, or evidence of production deployment. Its examples are constructed. Research and primary documentation were checked on September 6, 2026.

What the research supports

In George Necula’s original work, proof-carrying code supplies a proof that a program satisfies a consumer’s safety policy; a checker validates that proof before admitting the code. That is a stronger claim than attaching a signature, rationale, or audit log. The relevant inheritance is the separation between an untrusted producer and a smaller trusted checker. See Necula and Lee’s original technical report.

Fred Schneider’s Enforceable Security Policies establishes limits on execution monitoring. A monitor can prevent specified bad execution prefixes, but that does not establish eventual success or every information-flow property. For an agent gateway, “never dispatch an unauthorized refund” is a tractable target; “always resolve the customer’s problem” is a different obligation.

CaMeL provides a concrete agent-system precedent: separate control and data flows, track capabilities, and enforce policies in an interpreter around the model. Its results and guarantees depend on its threat model. The paper also discusses non-goals, utility costs, and side channels. It does not establish that arbitrary natural-language judgments can be proved correct.

These sources motivate the design below. They do not validate this proposed design.

Define the claim before the artifact

Three artifacts are often collapsed into “proof”:

This proposal uses authorization receipts for general workflows. A deployment may attach machine-checkable proofs for a restricted policy language, but should identify the proposition, logic, checker version, and assumptions separately.

The target claim is:

Every mediated external dispatch was authorized for its exact principal, tenant, operation, arguments, resource version, and validity interval at its dispatch boundary.

This does not claim that evidence is objectively true, a model is honest, or a supplier will honor a request. Those are separate questions with separate observations.

The trust boundary

Treat the planner, retrieved text, memory content, and model-generated receipts as untrusted. They may propose actions or supply candidate evidence. They cannot declare themselves authorized.

The trusted computing base includes the identity verifier, policy checker, canonical serializer, approval verifier, durable reservation ledger, credential boundary, and adapter implementation. The gateway owns credentials; the planner has no alternate route to the same effect. A browser session or shell with equivalent credentials would enlarge this boundary and must be mediated too.

Untrusted proposals and evidence
              |
              v
  resolve identity and object versions
              |
              v
  deterministic obligation checker
              |
      deny / pause / receipt
              |
              v
  atomic reservation + durable outbox
              |
              v
  credential-owning adapter -> supplier
              |
              v
  reconcile result -> verify postcondition

This is compatible with ContextOS’s existing governance boundary and execution contracts. It does not replace native ActionRisk with a numerical trust score. The compatibility ApprovalMode vocabulary remains read_only, local_write, network, delegated, and destructive.

A minimal transition system

Let runtime state be S = (P, I, V, A, B, L, O): policy snapshot, identity and delegation snapshot, resource versions, approvals, budget reservations, operation ledger, and durable outbox.

Let an action proposal a name a principal, tenant, capability, target, typed arguments, and semantic operation ID. Let e be the evidence snapshot. Let t be an explicit clock observation supplied by the trusted runtime. The checker is a deterministic function of these inputs:

check(S, a, e, t) -> deny(reasons) | pause(obligations) | eligible(receipt)
 
eligible = schema_valid
       AND identity_valid
       AND delegation_contains_action
       AND tenant_and_resource_match
       AND capability_and_native_risk_allowed
       AND evidence_requirements_satisfied
       AND required_approval_matches
       AND validity_window_open
       AND budget_reservable

Every predicate needs executable semantics. “Evidence sufficient” cannot mean that a model says it is sufficient. For a refund, it could mean an authenticated order lookup resolves one canonical order, ownership matches, the refundable balance is observed at a named version, and no required conflict remains unresolved.

Human judgment can satisfy a policy-selected approval obligation. The receipt establishes that an authorized principal approved the frozen decision basis; it does not convert that person’s judgment into a theorem.

The following states belong to this article’s model, not to a new canonical enum:

An unknown operation retains its reservation until reconciliation. An expired, undispatched operation can release its reservation. A dispatched operation cannot be erased merely because its receipt subsequently expires.

Bind the receipt to the effect

A useful receipt binds more than a tool name. Its conceptual payload includes the action digest, evidence digest, policy and checker versions, principal and delegation identifiers, tenant, resource version, approval reference, expiry, operation ID, and budget reservation reference.

This is a proposed application artifact, not an importable ContextOS type:

action_digest = HASH(
  domain_separator,
  canonical(principal, tenant, capability, target,
            typed_arguments, resource_version, operation_id)
)

Canonicalization must be fully specified. RFC 8785 defines a JSON canonicalization scheme, including recursive property ordering and serialization constraints. A top-level key sort is insufficient. Currency must also have an application-level representation, such as integer minor units plus currency code; a serializer does not decide monetary semantics.

The adapter rederives the digest from its actual dispatch payload. It rejects altered arguments and cross-tenant receipt reuse. Store sensitive evidence behind access-controlled references rather than making a signed receipt a new data leak. A signature authenticates its issuer and payload; its authority still depends on the issuer’s configured role.

The race a diagram can hide

Suppose two workers each observe a refundable balance of 10,000 minor units and independently authorize refunds of 7,000. Each local predicate succeeds. The aggregate effect is invalid.

The proposed remedy is an atomic conditional transition that reserves the shared refundable amount against the observed order version. Only one worker can reserve 7,000 from that version. The losing worker must reload and re-evaluate. The same transaction creates the durable operation entry and outbox record, so a crash cannot leave an unrecorded dispatch intent.

This only controls state the runtime owns. If another channel can change the supplier’s balance, use a provider-side conditional operation or authoritative supplier limit. A local lock cannot freeze an airline, payment processor, or another application.

Likewise, local receipt consumption cannot guarantee one external effect after a timeout. The provider may have committed before the connection failed. AWS’s idempotent API guidance explains why retries need a stable expression of caller intent and a service contract. When that contract is unavailable, reconciliation or operator intervention is part of correctness.

A conditional safety argument

Define invariant J: every operation in the dispatch log has a matching eligible receipt, valid reservation, and authorized dispatch event for the exact bound action.

Assume the initial state satisfies J; all effects pass through the gateway; cryptographic and identity checks behave as specified; the checker correctly implements the predicates; and durable transitions are atomic and version-checked. Further assume the adapter preserves the bound action and the dispatch-time revocation rule has a defined ordering point.

The induction is small: transitions that do not dispatch preserve J; the dispatch transition can append only a matching receipt-backed event, so it preserves J as well. Therefore every reachable dispatch-log state satisfies J under those assumptions.

This is a proof sketch about a transition model. It is not a proof of the implementation or of supplier behavior. Extending the claim to external effects requires adapter refinement and provider semantics. Immediate revocation across an in-flight network request is not guaranteed by checking a token a few milliseconds earlier; the system must define whether dispatch or provider acceptance is its authorization boundary.

Tests that could falsify an implementation

The acceptance suite should attempt failures at the boundary, with a supplier stub that records actual effects:

• Change one nested argument after approval; expect denial and zero dispatches.
• Replay a receipt under another tenant; expect denial and zero dispatches.
• Race two reservations against one resource version; expect at most the permitted aggregate reservation.
• Crash after provider commit but before receipt storage; expect reconciliation without a new semantic operation.
• Revoke delegation while an operation is queued; expect the documented dispatch-time rule to apply.
• Alter a policy snapshot or remove evidence; expect verification failure, not a substituted default.
• Fail the checker or ledger; expect no effect to bypass the missing control.

A later formal artifact should model these interleavings, check the invariant, and test implementation traces against the model. No such model-checking result is claimed here. Measure false denials, stale approvals, verification overhead, unknown-outcome age, and task completion alongside violations. A gateway that blocks everything is safe in a narrow sense and useless in practice.

The architecture earns the name by making its claim small enough to check, its assumptions explicit enough to challenge, and its failures observable enough to repair.

What to read next

• Proof-carrying context covers the evidence view before action admission.
• Agent Harness Benchmark: an experimental protocol explains how to test the surrounding controls.
• The agentic travel commerce reference architecture applies these boundaries to bookings and recovery.