AGL behavioral contracts and enforcing runtime

Status: proposal, not an implemented language version

Baseline: AGL 0.6, repository revision 78dd552

1. Purpose and decision

Extend AGL's existing data types, effects, idempotency contracts, and durable execution with resource-scoped authority and checked action protocols. Expose the same contracts through a Rust framework API so applications can construct checked workflows without writing AGL source.

The proposed guarantee is:

Every dispatched action has validated arguments, sufficient current authority, permitted effects, and a valid protocol transition. An approval-protected action is bound to an authentic approval of that exact action. These properties hold for developer-authored workflows and model-proposed actions at the mediated execution boundary.

This guarantee assumes correctly implemented trusted adapters and an enforcing host. It does not prove that model output is true, that tools meet their business specifications, that external systems provide exactly-once execution, or that a workflow eventually completes.

The review decision is whether to adopt the contract model and staged delivery below. This document does not reserve a new language version, change AGL 0.6, or declare any proposed syntax supported. All new syntax and API sketches are illustrative; a versioned normative specification must accompany implementation.

2. Existing behavior and the gap

AGL already implements a substantial part of this design. The proposal builds on these mechanisms rather than replacing them.

In particular, DeploymentPolicy::validate_program currently uses has_approval to detect whether an external-write pipeline contains an approval statement somewhere in its control flow. That structural summary does not establish that a successful approval precedes each write, that rejection prevents the write, or that the decision covers its arguments. Existing approval values are ordinary booleans, not evidence of authorization.

The current tool registry validates declared arguments and results. Its optional Invocation carries task identity and cancellation, but not a resource-specific grant or an approval permit. The registered tool handler receives JSON arguments. The new dispatcher must close this context gap for protected operations.

Native Rust remains trusted in-process. URL/path argument checks are policy helpers, not confinement of arbitrary Rust code or all network/file accesses.

3. Scope

The first release covers:

• Typed, immutable action proposals and exact-action approvals.
• Authority grants scoped to principal, operation, and resource.
• Finite resource protocols with opaque handles and affine consumption.
• A shared contract representation and dispatcher for AGL and Rust embedding.
• Durable operation identity, atomic claims, and explicit uncertain outcomes.
• Static diagnostics and runtime denials with an auditable reason.

Full session types, general dependent types, arbitrary refinement proofs, automatic inference of native code effects, and model-internal reasoning verification are outside this release. Evidence protocols are a follow-on use case of the same primitive, not an initial claim of semantic truth verification.

4. Contract model

4.1 Distinct concepts

Existing agent requires continues to express model/provider features such as reasoning and tool_calling. A new authority requirement must not overload this field. Likewise, application-defined effect names do not themselves grant access.

4.2 Tool and task contracts

The shared intermediate representation contains:

OperationContract {
  qualified_name, contract_version, implementation_fingerprint,
  input_type, output_type,
  authority_requirements,
  possible_effects,
  protocol_preconditions,
  protocol_outcomes,
  approval_requirement,
  idempotency_contract,
  scheduling_contract
}

Authority requirements select resources from validated arguments or opaque handles. Protocol outcomes describe success, definite failure, and uncertain completion separately. Effect sets describe possible execution, including error paths and compensation. Financial operations may add an application effect such as financial_write, but must also retain external_write.

Contracts are trusted declarations about host implementations. Registration must match source/module contract fingerprints before execution. A handler with a different contract cannot silently replace a checked implementation.

4.3 Authority grants

A grant contains a trusted issuer, subject principal, allowed operations, resource scope, validity interval, and revocation identity. Possessing a type named EmailSend is insufficient to send from every mailbox.

Only an authenticated host authorization service may issue grants. The model may request authority but cannot create it. Delegation may narrow scope and expiry; it may never increase either. Static checking verifies required grant kinds and scope relationships where known. Dispatch checks concrete arguments, identity, expiry, revocation, and deployment restrictions.

Effective authority is the intersection of source requirements, granted scope, and deployment policy. A tool omitted from an agent's tool set remains unavailable even when the host has registered it. A model naming another declared tool must receive a denial at dispatch, not just an omission from its advertised schema.

Read grants may be shared when their contracts permit it. One-shot approvals and exclusive state transitions are affine: they may be consumed at most once.

5. Resources and protocol typing

5.1 State belongs to a resource

Represent protocol state as Resource[R, S], where R names a resource kind and S a declared finite state. This is proposed notation, not current TypeExpr syntax. An email draft and a report may have independent states within the same workflow; one global Agent<State> would conflate those lifecycles.

A handle identifies a resource ID, immutable revision, payload digest, protocol definition, and state. Constructors are inaccessible to ordinary AGL expressions, model output, and unprivileged host clients. Nominal typing alone does not make a value unforgeable; runtime handle lookup and protected issuance are required.

The initial email protocol is:

Draft --propose--> Proposed --human approval--> Authorized
                         |                         |
                         +--human denial--> Denied  +--dispatch claim--> Dispatching
                                                                        |
                                              +-------------------------+------------------+
                                              |                         |                  |
                                           Sent                 FailedNoEffect          Unknown

Unknown means the dispatcher cannot establish whether the external action took effect. Reconciliation may establish Sent or FailedNoEffect. It must not silently return the resource to a reusable authorized state.

A proposal snapshots all effect-relevant arguments. Editing a draft creates a new revision and requires a new proposal and approval. Editing cannot mutate an already authorized snapshot in place.

5.2 Static judgment

Use an explicit output environment to capture consumption and state changes:

Γ ; Δ ; C ⊢ e : τ ! ε ▷ Δ'

• Γ contains ordinary reusable values.
• Δ contains owned resource handles and affine permits.
• C contains available authority requirements/grants.
• τ is the result type and ε the upper bound on possible effects.
• Δ' contains resources available after evaluation.

For a declared operation the checker requires compatible inputs, sufficient authority kinds, permitted effects, and matching input states. Consumed bindings leave Δ; returned handles enter Δ' according to the selected outcome.

At a conditional or match join, a resource is available only when every reachable predecessor preserves the same ownership and compatible state. Differing states require an explicit tagged outcome and exhaustive match; an ordinary boolean cannot narrow a resource to Authorized.

A loop must preserve its resource invariant at the back edge. A permit consumed by the body cannot reappear on a later iteration. The first implementation may reject loops carrying changing protocol states rather than infer complex invariants.

Entering try/catch cannot resurrect consumed handles. Dispatch failures expose typed outcomes that say whether the action was definitely unperformed or may have occurred. A fallback value cannot stand in for a permit or proof handle.

5.3 Dynamic choices

Static inference includes every tool an agent may select, as AGL 0.4 already does. Giving a researcher a write tool therefore adds its effects even if the prompt says not to use it. The effect ceiling must be satisfied without predicting which tool the model chooses.

The runtime can reduce the advertised tool set according to the current resource states, but advertising is a usability feature. The dispatcher independently validates every proposal against current state and authority. Invalid proposals produce structured feedback; they do not execute.

6. Exact-action approval

6.1 Proposed interface

The following is a semantic sketch, not accepted AGL syntax:

proposal = propose send_email(email_revision)
decision = request_approval(proposal, role = operator, expires = 3600)

match decision {
  Granted { permit } => dispatch(proposal, permit)
  Denied { reason }  => return Rejected(reason)
}

propose is deterministic and performs no external write. request_approval contributes human; dispatch contributes the tool's effects. Only the trusted approval resolver may produce Granted. A model returning JSON with that tag does not mint a permit.

A permit authorizes one logical operation. It binds:

• Authenticated approver, requesting principal, execution ID, and grant scope.
• Qualified operation and contract/implementation fingerprints.
• Canonical validated arguments, resource IDs and revisions, and their digest.
• Destination, account/tenant, and other effect-relevant deployment configuration.
• Policy fingerprint, issuance time, expiry, and logical operation ID.

The approval UI must present the same snapshot that dispatch will execute. Defaults must be expanded before approval; the dispatcher must not silently add or change recipients, amounts, destinations, or other effect-relevant arguments.

6.2 Canonicalization and authenticity

Canonicalization is versioned: recursively sorted object keys, preserved array order, explicit type tags, finite numeric values with one defined encoding, and materialized defaults. The MVP may restrict proposed payloads to supported schema types until this encoding has conformance fixtures. Hash the encoded snapshot with a standard cryptographic digest; a hash identifies content, not its approver.

The local implementation uses opaque IDs resolved through the trusted store. Externally submitted decisions must be authenticated and checked against a pending server-issued request and approver role. Raw client booleans, a model's message history, or user-supplied JSON cannot be accepted as authentic permits. Portable signed permits are deferred; signing-key management is not required for the local MVP.

6.3 Consumption and rejection

Permit claim, resource revision/state check, and transition to Dispatching must be one atomic durable transaction. A second claim must fail, including claims from a second process. Copying a serialized permit ID does not copy authority.

Rejection, expiry, revocation, or fingerprint mismatch prevents a new dispatch. An already dispatched action cannot be undone by revocation. Recovering its outcome remains legal; a further external attempt requires current authorization under the retry contract. The MVP stops and requests renewed approval when a permit expires or authority is revoked before such an attempt.

Legacy approve ... remains a Bool under its existing language versions. It does not become a permit by implicit conversion.

7. Enforcing dispatcher

All protected task calls and tool calls, including nested calls inside model adapters and native contextual handlers, must pass through one dispatcher.

AGL source / Rust workflow builder
            |
       checked contract IR
            |
      model action proposal
            |
      enforcing dispatcher
            |
        trusted handler

Before starting a new logical operation, the dispatcher must:

1. Resolve its qualified contract and verify registration fingerprints.
2. Validate arguments and resolve opaque handles through trusted lookup.
3. Check the agent tool set, concrete authority scope, and deployment restrictions.
4. Check effect ceilings and protocol preconditions.
5. Validate any approval against the exact canonical proposal.
6. Reserve scheduling/budget capacity and recheck authorization after waiting.
7. Atomically claim permits/resource revisions and persist an operation intent.
8. Invoke the handler with stable operation identity and cancellation context.
9. Validate and persist the outcome and resulting protocol state before releasing reusable handles to the caller.

Scheduling capacity reserved before a failed claim must be released; attempted work already charged under budget semantics is not refunded merely because a result is unsuccessful. Failure to persist an intent prevents dispatch. Failure to persist a result after an external effect produces an uncertain outcome.

The handler receives the authorized snapshot and contextual execution services. Protected handlers must not be callable through the legacy unrestricted registry entry point. Native hosts that deliberately bypass this boundary fall outside the guarantee. Untrusted extension confinement requires a separate sandbox design.

The initial condition on runtime traces is a safety property: every dispatch has a preceding valid claim, and every committed state transition follows its contract. Neither property establishes liveness or task utility.

8. Durability, retries, and uncertain outcomes

Each logical tool operation has its own persisted ID beneath its parent task invocation. Retries reuse that ID, proposal snapshot, and destination idempotency key. A parent task ID alone is insufficient when a model invokes a tool several times or changes its decisions after restart.

Persist each tool intent and outcome before allowing the adapter to continue. Persist the adapter continuation/tool-call transcript needed to match pending operations on resume. Recovery must not ask the model to regenerate an unfinished action and assume it will produce the same arguments. A changed action requires a new proposal; a new write requires its own authorization.

The operation record has the following lifecycle:

Pending -> Claimed -> Completed
                  -> FailedNoEffect
                  -> Unknown -> ReconciledCompleted | ReconciledNoEffect

Claimed is persisted before I/O. A crash while claimed is treated as Unknown until receiver lookup, authoritative handler evidence, or another declared reconciliation mechanism establishes an outcome. Even invalid response JSON can follow a successful external write and must not be classified as no effect.

Automatic retry is permitted only when:

• The failure selector permits it and budgets/deadlines allow it.
• The existing idempotency contract allows the same logical operation to repeat.
• Required authority and approval remain valid for the next attempt.
• An uncertain write is safely deduplicated by the destination or first reconciled.

Payment/email APIs are not assumed to support idempotency. Without a receiver contract or authoritative reconciliation, an uncertain non-idempotent operation requires human resolution and receives no blind retry.

The dispatcher guarantees at most one initial claim per permit. It cannot guarantee exactly-once external effects across an I/O/commit boundary without cooperation from the destination. An idempotency key is a host/receiver promise, not a proof established by its String type.

The existing append/load EventStore API cannot by itself express an atomic cross-process claim. Introduce a separate transactional OperationStore contract for proposal snapshots, decisions, permit claims, resource revisions, and tool outcomes. SQLite is the first implementation. Claim and intent must commit together; audit events are committed in the same transaction or an atomic outbox. Trace appends alone must not be used as a mutual-exclusion primitive.

Replay substitutes completed operations without contacting providers or tools. Recovery checks source, deployment, policy, protocol, canonicalization, and contract fingerprints. Revocation prevents new attempts, not reading a historical receipt. Retention must preserve pending intents and consumed-permit tombstones for the lifetime of any credential/reference that could otherwise be replayed.

9. Parallel execution and resources

Existing effect unions remain conservative. Disjoint effect names do not prove that operations are independent, and shared effect names do not prohibit parallel reads.

• Parallel branches receive disjoint owned handles/one-shot permits. Shared read access requires an explicit shareable grant and resource contract.
• Runtime compare-and-swap on resource revision prevents concurrent transitions even when distinct permits accidentally name the same resource revision.
• A permit cannot be captured by both branches or duplicated by parallel map.
• The MVP forbids protected external writes inside race: cancelling a losing branch cannot retract an effect it already performed. Read/model races retain their existing cancellation semantics.
• Admission reserves tool calls, retries, and concurrency before work starts. Nested scopes must also respect enclosing ceilings; a child cannot evade its parent's budget by creating another pipeline scope.
• Token/cost usage reported after execution remains accounting rather than a strict predictive bound. Hard limits require declared upper-bound reservation and a provider interface capable of honoring the corresponding limit.

Cancellation before claim prevents dispatch. Cancellation after an effect starts may produce Unknown; it does not release the consumed permit for another action.

10. Framework API and implementation boundaries

The production implementation remains Rust. Reuse AGL's existing parser, checker, runtime, adapters, and embedding API; do not create a second execution engine.

The proposed public API has these responsibilities:

ContractRegistry: register versioned trusted operation contracts
WorkflowBuilder: construct the same IR as the AGL frontend
check_workflow: Workflow -> CheckedWorkflow | Diagnostics
Dispatcher: execute only checked operations or validated model proposals
ApprovalResolver: authenticate decisions for persisted pending proposals
OperationStore: atomically claim and advance protected operations/resources

CheckedWorkflow, permits, and state handles have private constructors. Rust typestate wrappers can improve developer ergonomics, but runtime checks remain authoritative for JSON boundaries, revocation, persistent state, and model choices. A compiler certificate is not authorization to execute with arbitrary deployment bindings.

Module interfaces include authority requirements, protocols, affine ownership, effects, approval requirements, and outcome/idempotency contracts in their fingerprints. Adding authority/effects, strengthening preconditions, or changing states/approval bindings is an exported compatibility change. Resume compatibility is stricter than source API compatibility because old approvals must bind the same executable contract.

Version the changed extension contracts; do not add mandatory behavior to API version 1 while claiming unchanged compatibility. Legacy handlers remain usable for legacy workflows. They cannot register as protected operations until they provide the new context and contracts. No new dependency is approved by this document; any implementation requiring one follows repository approval rules.

11. Observable evidence obligations

After the email MVP, express evidence gathering using the same resource model:

Question<Unresearched>
  -> Evidence<Collected>
  -> Evidence<CheckedAgainstPolicy>
  -> Report<Reviewed>
  -> Publication

Evidence receipts record source identity, retrieved content digest, retrieval time, and the question/revision they concern. A trusted validator issues an attestation identifying its policy/version, inspected evidence, report digest, and result. Merely running search does not establish that sources support a particular answer. Publication must bind the attestation to the exact report.

The checker proves required receipts/attestations are present and correctly bound. The assurance about relevance, corroboration, or truth is only as strong as the validator. An LLM-based validator yields a recorded judgment, not a mathematical proof. Do not expose a misleading universal Verified state.

12. Diagnostics and audit

Allocate stable diagnostic codes during implementation for missing authority, invalid protocol state, consumed permit use, incompatible branch ownership, unbound approval, unsafe retry, and unsupported protected race. Static diagnostics include source spans, required/actual state, and a concrete remediation.

Runtime denials distinguish schema errors, authorization denial, expired/revoked approval, proposal mismatch, stale revision, claimed permit, persistence failure, and uncertain completion. Policy denial must not be reported as an ordinary network error or treated as retryable.

Audit records contain execution/task/tool operation IDs, principal, contract and policy fingerprints, resource revision, proposal digest, decision actor/time, claim, attempt, outcome, and reconciliation. Redact secrets before persistence. Store payload snapshots through protected storage references; audit traces must not contain bearer grants or permit secrets. Digests of low-entropy sensitive fields are not automatically anonymous.

13. Delivery and acceptance

Stage 1: contracts and exact-action email approval

Implement shared contracts, checked dispatch, opaque proposals/permits, a trusted approval resolver, and the transactional local operation store. Demonstrate with deterministic Rust handlers and a fake email destination; live email is unnecessary.

Acceptance scenarios:

Tests must include real SQLite concurrency/atomicity checks and fault injection at the claim, external-call, and completion boundaries. Counting mock calls only within one process is insufficient evidence for cross-process claims.

Stage 2: AGL protocol and ownership checking

Choose the surface grammar, add a versioned normative specification, and implement AST/parser/formatter/checker/runtime support together. Add module-interface compatibility rules, source-span diagnostics, migration guidance, and positive and negative conformance fixtures for branching, loops, catch/fallback, parallel capture, stale handles, and forged host/model values.

Stage 3: evidence and bounded delegation

Add evidence attestations and attenuated delegation using the same dispatcher and opaque resource primitives. Measure usability and rejected valid workflows before adding general session types, refinements, or symbolic resource arithmetic.

For every stage, retain existing versioned conformance/regression behavior, run the repository checks, document guarantee assumptions, and exercise mock CLI and embedding paths without credentials. No stage is complete on parser support alone.

14. Alternatives and open decisions

Resolve before implementation:

1. Select protocol/authority syntax without overloading provider requires.
2. Specify canonical payload encoding and choose the digest implementation.
3. Define authenticated approver integration and the local operator identity model.
4. Decide the new extension API version and protected-operation migration path.
5. Specify reconciliation contracts for the first real destination after the mock MVP. Its idempotency guarantees determine achievable retry behavior.

The initial recommendation is a finite protocol checker plus exact-action permits and runtime enforcement. Keep the calculus small until the email and evidence examples establish where richer typing is necessary.

15. Related work

These references establish overlapping mechanisms, not equivalence to this spec or an independent assessment of implementation quality.

• Effect AI toolkits: typed tool contracts and required handler services; useful framework composition ideas.
• Pydantic AI deferred tools: explicit approval/deferred execution and discussion of client authorization boundaries.
• LangGraph interrupts: persisted human interaction and replay/idempotency responsibilities.
• Guardians: structured-plan verification using taint analysis, security automata, and SMT conditions.
• AgentSpec: a runtime policy DSL with triggers, predicates, and enforcement actions.
• Agent-C: temporal action constraints enforced with SMT checking and constrained generation.
• Language-Based Agent Control: typed agent-generated programs with capability, provenance, and information-flow policies.
• Temporal activity semantics: destination idempotency and the distinction between durable completion records and repeated external execution.