Effect Transaction Protocol

Core 0.1 · Implementer draft

Bind authorization to one action and one observed state.

ETP defines records and executor rules for external actions proposed by untrusted agents. The executor validates the chain and consumes a single-use grant before dispatch. A receipt then records the observed outcome.

Read Core 0.1 View the repository

Model output does not create execution authority.

Execution order

The executor rechecks authority immediately before claim.

The executor checks record bindings, time, audience, current state, and effect-profile rules. It claims the grant before it calls the target.

  1. 01 / Validate

    Verify the exact chain

    Match the task commitment, proposal, decision, grant, executor audience, and admitted evidence.

  2. 02 / Claim

    Consume one grant

    Move the grant from unused to consumed with one atomic lifecycle-store operation.

  3. 03 / Dispatch

    Call the declared target

    Use the operation, target, arguments, and state condition bound into the proposal.

  4. 04 / Observe

    Record the outcome

    Issue a receipt. If the result is unknown, append reconciliation evidence without restoring the grant.

Agent runtime Proposes an external action
ETP evaluator and executor Decide, validate, claim, dispatch, observe
External target API, cluster, repository, or service

Responsibility boundary

The protocol is one part of the control plane.

ETP fixes record shape and execution order. Each deployment still chooses its policy, evidence, adapters, trust roots, and operating controls.

ETP specifies

  • Versioned records with strict schemas and cryptographic bindings.
  • An authorization decision bound to one proposal and its admitted evidence.
  • An audience-bound, time-limited grant with one lifecycle-store claim.
  • Receipts and append-only reconciliation for known and unknown outcomes.
  • Effect-profile rules for currentness, dispatch, observation, and retry handling.

A deployment supplies

  • Policy evaluators and the evidence used to reach a decision.
  • Target adapters, credentials, and target-side conditional operations or fencing.
  • A lifecycle store with the consistency properties required by the profile.
  • Signers, verifier trust roots, key rotation, and operational access controls.
  • Monitoring, incident response, recovery, and production assurance.

Repository contents

Core 0.1 can be inspected and exercised.

The repository contains the draft specification, strict schemas, reference software, conformance data, and bounded formal models.

  • Schemas and profiles

    Nine strict Core schemas define record shape. Reference profiles specify conditional HTTP requests and Kubernetes JSON Patch.

    Open schemas

  • Reference software

    Five Rust crates cover Core verification, the authority profile, a SQLite lifecycle store, executor composition, and the CLI. The TypeScript package provides structural verification without runtime dependencies.

    Review status

  • Outcome handling

    A receipt separates a known failure from an unknown result. An unknown result keeps the grant consumed and requires reconciliation before another attempt.

    Read the rules

  • Formal artifacts

    The repository contains Lean declarations for selected lifecycle invariants and a bounded TLA+ model. The stated proof boundaries remain part of each result.

    Inspect Lean

Repository evidence

Counts are tied to checked-in source sets.

evidence-summary.json records these counts and the hashes of the inputs used to derive them.

77 Core conformance cases Binding, canonicalization, chain, claim, currentness, issuance, receipt, reconciliation, time, and transport cases.
50 Effect-profile vectors 4 positive and 46 adversarial vectors across the checked-in HTTP and Kubernetes profiles.
23 Lean theorem declarations Selected lifecycle invariants. This is not a model-to-code refinement proof.
65,232 Distinct TLA+ states Complete bounded search for the checked-in configuration. This is not an unbounded liveness proof.

Machine-readable source: evidence-summary.json

Status / Implementer draft

Core 0.1 defines a testable protocol surface.

The checked-in tests cover this repository’s implementations and models. They do not establish production fitness, interoperability with an independent implementation, prompt-injection immunity, regulatory compliance, or external assurance.

Start with the specification, then review the threat model and implementation status.