Evidence and replay

audit-export produces one complete tenant prefix and its referenced immutable policy bundles. replay consumes only those files, verifies the chain and bindings, and reconstructs chronological decisions with separate in-memory ledgers. An ELIGIBLE result is an explanation, never executable authority.

Export and trust

Set DATABASE_URL to the restricted gateway connection in the private operator environment. Store a current tenant ADMIN credential in a private text file; never pass it as a command-line argument. The destination parent must already exist, and both output files must be new.

uv run execbound audit-export --tenant <tenant-UUID> --credential-file local-data/admin.token --output local-data/history.json

The default companion checkpoint is history.head.json; --checkpoint selects a different new file. --database <name> reads a restored copy on the same server instead, so a restore is checked without anyone building a second connection string with its password; the runtime role, forced RLS, check_runtime and the ADMIN credential check apply unchanged, and the output is the same either way. Export reads a coherent read-only repeatable-read snapshot and checks current ADMIN authority again in separate transactions immediately before publishing each file. It does not append an export audit event or contact a provider.

Retain the checkpoint independently. A head distributed alongside its own export establishes internal consistency only: replacement of both files by a privileged writer is outside that guarantee. Publication links the checkpoint first and the export last; a machine crash can leave an orphan checkpoint. Existing files are never overwritten on retry.

Replay and comparison

These commands also work with the database and providers stopped. They do not load .env or runtime configuration, authenticate live credentials, resolve current context, activate policy, or consume real approvals and budgets.

uv run execbound replay --input local-data/history.json --trusted-head local-data/history.head.json --output local-data/baseline
uv run execbound replay --input local-data/history.json --trusted-head local-data/history.head.json --candidate local-data/candidate.json --output local-data/comparison

Each output is a new directory containing deterministic report.json and report.md. Inputs are strict JSON: no duplicate keys, floating numbers, unknown versions, foreign references or silently truncated histories. V1 bounds the export to 64 MiB, 10,000 events and 256 referenced bundles; candidate files are bounded to 1 MiB. Oversized, corrupt or secret-bearing history is rejected without exposing raw input or SQL diagnostics. Use a new destination for each run. For a pre-activation view without files, execbound bundle-preview runs the same export, verification and candidate comparison in memory as a current ADMIN and prints the changed decisions.

Future execution events capture normalized policy inputs, historical identity/approval bindings and actual usage/start/finish times. Audit sequence orders events; semantic time determines freshness and rolling windows. Confirmed units count in (usage_time - window, usage_time]; unresolved reservations remain counted until exact evidence settles them. Approved operations count toward total ceilings and do not count toward autonomous ceilings. New rules, runs, inverse operations or changed policy cannot erase retained impact. Approval captures carry required_approvers and every counted approver; a VERIFIED capture with fewer distinct approvers than required, a repeated principal or a denial is INSUFFICIENT_QUORUM and makes the history incomplete, and approval.decision_recorded marks a partial approval as a consequential decision. Observed decisions are ordinary captures with mode: OBSERVE: the execution ends OBSERVED with outcome OBSERVED, replay counts its OBSERVED impact only for observe-mode evaluations (the projection the gateway used), a candidate bundle re-evaluates it like any enforced decision, and an observed execution that shows an approval, reservation, claim or dispatch, or an OBSERVED transition without an observe-mode capture, is OBSERVED_WITH_EFFECT and makes the history incomplete. tenant.mode_changed is informational.

Limit scopes (design) are reconstructed from captures alone. Every unit the ledger reserves, observes or holds uncertain carries the account and scalar facts of its capture's frozen plan and the memberships of its captured agent identity, and usage filters each rule's units by scope exactly as the store does: any listed action, the asking principal, the rule's account, the selector over the unit's retained facts, or the rule's group in the unit's retained membership. Captures written since this unit record the agent's memberships as identity.groups, an empty list when the agent belongs to no group, so replay can tell "none" from "unrecorded"; a capture without the key predates recorded membership and is evaluated as a member of nothing, which is what the kernel did, so baseline decisions still match. UNKNOWN_GROUP_MEMBERSHIP is a candidate-only uncertainty: a candidate rule with a group scope marks a decision UNRESOLVED when the decision's own capture lacks groups (its applicability is unknown) or when a unit that would otherwise have counted by state and window lacks them (the count is only a lower bound). A unit with unknown membership never counts toward a group scope, so the uncertainty is expressed by the marker and never by possible room in the budget, and a denial at the lower bound still stands. Offline candidate validation checks every action a rule lists against the catalog and every selector against the contracts of the candidate's mappings; group and account existence cannot be checked offline, so a candidate group rule for a group no capture recorded applies to nobody. group.created, group.assigned and group.revoked are informational.

The baseline re-evaluates recorded decisions from immutable facts and reconstructs retained outcomes. Legacy events without required inputs or semantic times are incomplete. Mutable current inventory, approval rows and stored counters never fill historical gaps. Unknown consequential semantics and invalid chronology propagate uncertainty rather than making later decisions appear eligible.

Emergency stop periods are reconstructed from matching tenant.stop_activated and tenant.stop_released events (a stop still active at the head is an open period) and listed in both reports. An admission, approval decision or dispatch commitment recorded inside a period, by chain order or by semantic time, is reported as DECISION_DURING_STOP and makes the history incomplete, because the gateway could not have produced it. An activation while a stop is open or a release without a matching activation is unsupported history. Candidate comparison ignores stops: a stop is not policy.

Each decision row carries the frozen arguments when they are non-empty, omitted otherwise, and report.md renders them as an Arguments: line, so a decision that turns on an option is explainable from the report. Verification rebuilds the attempted provider command with those arguments, so an export containing argument-bearing actions verifies against its recorded command digests. Offline replay cannot rebuild the catalog's OperationSpecs, because an export carries no mapping rows: simulate therefore validates a candidate bundle without them, and the action-context check holds only because a compatible candidate must keep the original, store-validated Cedar schema and mappings.

Candidate comparisons initially allow policy and limit changes with the captured operation mappings, accounts and context contracts. Newly required approval or an action that was never observed produces UNRESOLVED; a changed plan cannot reuse an old approval, so a candidate quorum change is a policy change and recorded approvers never satisfy a changed requirement by assumption; the bundle preview reports the candidate's effective requirement per changed decision. Possible impact and same-target dependencies propagate forward. A denial that remains true despite uncertainty can still be reported as DENY.

An unchanged observed action can be projected only under the report's explicit FIXED_HISTORY_PROJECTION provenance. This is not evidence about alternate external reality. No assumed-success or assumed-approval mode exists. Reports keep recorded and hypothetical outcomes distinct and expose dependency IDs and possible counts.

Terminal evidence retains the gateway's recorded proof and exact command/digest bindings. Offline verification does not independently reauthenticate the provider HMAC, because signing keys are deliberately excluded. Neither public replay routes nor real vendor integrations are included.

Externally executed operations

A settled checkpoint carries a settlement tier, and the tier is what chooses which envelope the retained record is parsed as — before either is parsed. The transition payload names it beside the evidence rather than inside it, because those bytes are validated as a TerminalEvidence and that model admits no extra field; the executions.result column carries it inside the evidence object as well, so an export is self-describing. At tier ATTESTED the authenticated record is parsed as the external executor's SignedOutcome; a settlement naming no tier is parsed as a provider's SignedJournal. Neither stands in for the other, so a mislabelled settlement is a refused export and never evidence read as the wrong kind. An executor's record binds no execution and no tenant of its own — what ties it to a row is the operation identifier the transition names and the record repeats, which is unique per tenant — and its Ed25519 signature is not rechecked here for the same reason the journal's MAC is not: verifying it needs a public key from executor_keys that no export carries.

An assertion is validated rather than stepped over. It is retained under its own key, never as evidence, so reading it cannot promote it; replay binds it to the operation, the account and both hashes and refuses two shapes no settlement writes: a settlement at tier ASSERTED whose outcome is FAILED_NOT_EXECUTED, which would be a history claiming the executor's bare word refunded a reservation, and a settled state that is not the outcome the assertion itself names — or anything but INDETERMINATE where no tier is named. So the two states a settled assertion may hold are EXECUTED and FAILED_EFFECT_UNKNOWN, and no assertion reaching a settlement can name STALE_AUTHORIZATION, because the pairing table forbids the one reason that would have mapped it there. The new refusal codes are INVALID_SETTLEMENT_TIER, INVALID_ASSERTED_OUTCOME and INVALID_ASSERTED_SETTLEMENT, and both kinds of evidence on one transition is INVALID_TERMINAL_EVIDENCE. MISSING_TERMINAL_EVIDENCE now fires for a terminal transition carrying neither kind, so a settled assertion is not reported as a settlement whose evidence went missing.

An attested checkpoint's provenance is RECORDED_EXECUTOR_EVIDENCE, kept apart from the RECORDED_GATEWAY_EVIDENCE a provider journal gets: a journal is the gateway's record of what a provider's own API answered, made by a different party from the one whose budget is at stake, while an executor's record is an authenticated statement about an action ExecBound never dispatched and says only who spoke. A decision row names its settlement_tier when it has one, serialized only when set so every report of operations ExecBound dispatched is byte-identical, and the rendering names the tier with what it rests on. A report that names a tier carries a fourth limitation line: executor attestation is gateway-recorded provenance, no executor public keys are loaded, and an asserted outcome was never verified. The offline ledger settles an asserted execution as executed, matching the impact the kernel confirmed, and settles an asserted FAILED_EFFECT_UNKNOWN the same way for the same reason: that settlement reads the outcome, and the one outcome it reconstructs a non-execution from is FAILED_NOT_EXECUTED. It models no canonical claim at all, so the claim an assertion leaves held is not something replay reasons about, and the live and replayed pictures of an asserted settlement differ in exactly that place.

A corrected row replays through a second settlement, and the ledger has one method for it. A transition out of FAILED_EFFECT_UNKNOWN is the administrator's correction, and the simulator chooses on the payload's own from_state: Ledger.correct admits CONFIRMED → NONEXECUTION once and refuses everything else, including a second call, while Ledger.settle stays exactly as narrow as it was. Widening settle instead would let any exported history claim a refund, which is the one thing an offline consumer must not be able to invent. Without the method, a tenant that corrected one row would get a report saying it could not reconstruct that window's ledger — INVALID_IMPACT_HISTORY and INCOMPLETE_HISTORY — rather than a refused export. The corrected row's exported settlement_tier and terminal time are the correction's, not the statement's, in both of the directions the correction admits. execution.checkpoint_granted, execution.outcome_reported, execution.claim_released, execution.control_point_contradiction and the four executor_key.* kinds are informational. An event kind the informational set does not name makes a tenant's export UNSUPPORTED with UNKNOWN_EVENT_SEMANTICS permanently, because audit events are append-only, which is why a new kind joins that set in the same change that first appends one.

One thing the history cannot answer. A second, differently signed attested record that restates a settlement's own tier, outcome and reason is verified, found to move nothing, and answered as a no-op: nothing is retained and nothing is appended, and the settlement's retained proof digest stays the first record's. So a tenant cannot afterwards see that two of its registered keys attested one settlement. No budget, claim or execution state moves, so this is a limit on what the chain can be asked and never a settlement that went unrecorded; the qualifying signer is any holder of a key the tenant registered, which may be the administrator's settlement key and not only the executor's.

The security event export (execbound export-events, see Operations) sends destinations exactly the sanitized event representation this export produces, in sequence order and never more; it reads the chain and never writes it.

See the validation instructions for reproducible two-provider examples and the evidence package.