TLA+ Specs

RevocationPropagation holds six safety conjuncts and spreads every observed revocation

formal/tla/RevocationPropagation.tla models revocation across authorities with six Apalache-typed variables: state (per-process lifecycle of each capability: active, attenuated, revoked), depth, rev_epoch (0 until a revocation is seen), the append-only receipt_log, pending (unordered in-flight propagation messages), and clock. Attenuate delegates once and narrows scope, Revoke is terminal, Evaluate emits a receipt with the current epoch view, and PropagateAny consumes a pending message and updates one process’s epoch.

SafetyInv ==
    /\ DomainsOK
    /\ NoAllowAfterRevoke
    /\ MonotoneLog
    /\ AttenuationPreserving
    /\ RevocationFreshness
    /\ RevocationStateCoupled

The config’s INVARIANT is SafetyInv: five leaf invariants and the structural DomainsOK. Each leaf’s MAPPING.md row names its call sites and assumption:

• NoAllowAfterRevoke. Every allow receipt was issued before its authority observed a revocation of that capability; causal allow-before-revoke histories are admitted. It constrains ChioKernel::revoke_capability, ChioKernel::check_revocation, both async evaluation paths, and RevocationSnapshot::is_revoked, and rests on ASSUME-SQLITE-ATOMICITY for single-row commits, with cross-row recovery excluded.
• MonotoneLog. Per-authority receipt timestamps strictly increase; only Evaluate touches receipt_log, through Append, and the strict order forbids logical reordering. It constrains ChioKernel::record_chio_receipt, SqliteReceiptStore::append_chio_receipt_returning_seq, and append_chio_receipt_tx, and rests on ASSUME-SQLITE-ATOMICITY and ASSUME-OS-CLOCK; the row notes that the storage anchors leave strict timestamps unenforced.
• AttenuationPreserving. Depth stays within 0..DEPTH_MAX, and an attenuated capability has been delegated at least once. It constrains validate_delegation_chain, ChioScope::is_subset_of, NormalizedScope::is_subset_of, and ChioKernel::validate_delegation_admission; the property is structural, so its assumption column reads n/a.
• RevocationFreshness. A nonzero rev_epoch[a][c] is strictly less than clock, since only a prior tick could stamp it. It constrains FreshnessConfig, verify_fresh_epoch_root, RevocationSnapshot, and RevocationView::install_if_newer, and rests on ASSUME-OS-CLOCK.
• RevocationStateCoupled. A nonzero local epoch holds exactly when the local state is revoked. It constrains RevocationSnapshot::is_revoked, RevocationView::install_if_newer, ChioKernel::check_revocation, and consult_revocation_view_at. The runtime snapshot carries one global epoch and a revoked-subject set, so the row records the coupling as a property of the model.

The mapping check fails when a named invariant has no MAPPING.md row. It also requires three invariants, RevocationStateCoupled among them, to be defined and conjoined in their spec’s SafetyInv, so dropping one fails even when its row survives.

NoAllowAfterRevoke ==
    \A a \in ProcSet :
        \A i \in 1..Len(receipt_log[a]) :
            LET r == receipt_log[a][i] IN
                r.verdict = "allow" => r.seen_epoch = 0

MonotoneLog ==
    \A a \in ProcSet :
        \A i, j \in 1..Len(receipt_log[a]) :
            i < j => receipt_log[a][i].t < receipt_log[a][j].t

AttenuationPreserving ==
    \A a \in ProcSet, c \in CapSet :
        /\ depth[a][c] \in 0..DEPTH_MAX
        /\ (state[a][c] = "attenuated" => depth[a][c] > 0)

RevocationFreshness ==
    \A a \in ProcSet, c \in CapSet :
        rev_epoch[a][c] # 0 => rev_epoch[a][c] < clock

RevocationStateCoupled ==
    \A a \in ProcSet, c \in CapSet :
        (rev_epoch[a][c] # 0) = (state[a][c] = "revoked")

The liveness property RevocationEventuallySeen says that once any authority observes a nonzero epoch, every authority later catches up to every observed epoch. Apalache 0.50.1 rejects free variables bound outside ~>, so the quantifiers sit inside two named state predicates.

AnyRevocationObserved ==
    \E a \in ProcSet, c \in CapSet :
        rev_epoch[a][c] # 0

AllObservedRevocationsCaughtUp ==
    \A a, b \in ProcSet :
        \A c \in CapSet :
            rev_epoch[a][c] # 0 => rev_epoch[b][c] >= rev_epoch[a][c]

RevocationEventuallySeen ==
    AnyRevocationObserved ~> AllObservedRevocationsCaughtUp

P ~> Q abbreviates [](P => <>Q). With finitely many Revoke actions per bounded authority and capability pair, the preamble treats the aggregate form as equivalent to the per-pair obligation. The property holds under the third conjunct of Spec:

Spec ==
    /\ Init
    /\ [][Next]_vars
    /\ WF_vars(PropagateAny)

Under WF_vars(PropagateAny), a propagation that stays enabled eventually fires; without it, messages sitting in pending forever would be legal. PropagateAny is a named action because the tableau encoding accepts WF_vars over a named action and rejects an existential nested directly under it. The mapping row constrains RevocationGossipPushQueue::enqueue_signed_root, flush_batches_at, RevocationCatchupResponse::validate_response, and respond_to_catchup; it rests on the model-only fairness conjunct, and ASSUME-NETWORK-TRANSPORT stays audited without guaranteeing delivery.

SPECIFICATION Spec

CONSTANTS
    PROCS = 4
    CAPS = 8
    DEPTH_MAX = 4

INVARIANT
    SafetyInv

PROCS = 4 authorities cover a sender, a receiver, and the smallest nontrivial fan-out; CAPS = 8 capability ids bound the per-process domains of state, depth, and rev_epoch; DEPTH_MAX = 4. MCRevocationPropagationTemporal.cfg differs only in filename, so the temporal lane keeps INVARIANT SafetyInv and adds the liveness property at length 24.

DistributedRevocation treats loss, duplication, and forgery as model actions

formal/tla/DistributedRevocation.tla, the largest spec at 601 lines, models signed revocation-root gossip over bilateral peers. Each action maps to a production function:

• QueueRoot. RevocationGossipPushQueue::enqueue_signed_root.
• Send. flush_batches_at.
• RejectForged. RevocationRootGossip::validate_envelope with SignedEpochRoot::verify.
• Deliver. RevocationView::install_if_newer.
• Catchup and Evaluate. The catch-up request and response pair, and consult_revocation_view_at.

Channels are counting functions. Duplicate increments a count, Lose decrements one without delivering, and Deliver picks any epoch with a positive count, so delivery order is arbitrary; forgedChannel is a separate adversarial input. Two shards check one aggregate each: DomainsOK checks the initial state at length 0, and BehavioralSafetyInv checks bounded paths at length 6, with configs that differ only in their INVARIANT line. The five conjuncts, with each row’s assumption:

• ClockSkewBound. Independently advancing authority clocks stay within the configured pairwise skew tolerance. ASSUME-OS-CLOCK, ASSUME-GOSSIP-FAIRNESS-PARTITION-BOUND.
• SignerPinnedHighWater. Every installed view stays authentic and at or below the origin’s own epoch. ASSUME-ED25519.
• NoAllowAfterRevokeDistributed. Every modeled allow records a local view that has not observed the target’s revoked epoch; a fresh nonzero snapshot may still allow an unrelated subject. ASSUME-OS-CLOCK.
• StaleEvaluationDenied. An evaluation records an allow only when the installed root timestamp is not in the future and its wall-clock age is within FreshnessBound. ASSUME-OS-CLOCK for tolerance; the deny predicate itself is production-linked.
• PartitionSuspendResume. Repeated cuts freeze the affected peer’s high-water mark and timestamp, and post-heal catch-up is established separately. Freeze safety is unconditional in the model; eventual resume needs ASSUME-GOSSIP-FAIRNESS-PARTITION-BOUND.

These rows are P2’s distributed_apalache evidence in the manifest. RejectedRawEvaluationCountBound stays outside SafetyInv: it would bound observation by a finite number of raw evaluations, a registered witness shows that arbitrary loss permits more evaluations than any finite count, and its mapping row marks it neither discharged nor claimed. The scheduled lane reruns both invariants at three authorities, four epochs, and channel cap 3 with MCDistributedRevocationDomainsNightly.cfg and MCDistributedRevocationNightly.cfg, and conditional liveness lives in a four-variable projection, formal/tla/DistributedRevocationTemporal.tla, which its own temporal gate runs.

The manifest scopes the production gate to exact deterministic scalar trace projections for one pinned origin and one RevocationView. Full-state refinement, fault injection into the shipped transport, and multi-origin isolation in Rust sit outside it, and ASSUME-NETWORK-TRANSPORT and ASSUME-GOSSIP-FAIRNESS-PARTITION-BOUND both stay required, scoped by this evidence without being discharged.

DistributedDomainsOK ==
    /\ DomainsOK
    /\ PartitionRelationOK
    /\ OriginStateOK

BehavioralSafetyInv ==
    /\ ClockSkewBound
    /\ SignerPinnedHighWater
    /\ NoAllowAfterRevokeDistributed
    /\ StaleEvaluationDenied
    /\ PartitionSuspendResume

SPECIFICATION Spec

CONSTANTS
    Authorities = {1, 2}
    EpochMax = 3
    ClockMax = 3
    FreshnessBound = 2
    EvaluationWitnessBound = 2
    PartitionBound = 3
    SkewBound = 2
    ChannelCap = 2
    Mutation = "none"

INVARIANT
    BehavioralSafetyInv

Kernel-state invariants bound revocation cuts, receipt ordering, delegation depth, and dropped calls

formal/apalache/ holds five invariant modules over Common.tla, with ten named invariants. Its README.md gives the original four specs shared bounds, Authorities = 1..3, CapSet = 1..6, and EpochMax = 4, for a bounded CI runner contract of a hosted ubuntu-24.04, the Z3 default solver, and a thirty-minute per-invariant timeout. ReceiptBeforeAllow adds CallSet = {1, 2}. Each invariant runs at length 6, except the four in PostAdmissionDropGuard.tla at length 8.

• MonotoneLogApalache, in MonotoneLogApalache.tla. MonotoneLog ported with explicit type annotations, under the bounded model-clock abstraction.
• RevocationCutCompleteness and DirectParentInClosure, in RevocationCutCompleteness.tla. A revoked capability removes dispatch eligibility for every transitive descendant in each authority view, and both lazy production lookup paths require the shared projected denial predicate. Every non-root parent edge sits in the parent’s descendant closure, so the modeled cut cannot pass over a missing direct edge.
• ReceiptBeforeAllow and AllowReceiptsBudgetChecked, in ReceiptBeforeAllow.tla. PublishAllow models only a completed tool-output allow backed by Decision::Allow, after the receipt-persistence call for the same single-use call identity and capability. Every persisted allow receipt carries a call identity and capability whose budget check completed before receipt construction on the modeled path.
• KernelTransitionCancelSafe, in KernelTransitionCancelSafe.tla. The bounded clean pre-dispatch abstraction assumes unchanged budget and receipt snapshots, and the mapping row places restoring them in Rust outside the proof.

The manifest scopes ReceiptBeforeAllow to the abstract persist-before-publish ordering, with a production replay of the native happy path; cross-row crash recovery needs implementation trace validation and crash-reopen conservation gates.

formal/tla/DelegationDepthBound.tla (233 lines; DEPTH_MAX = 4, PEERS = 3 in MCDelegationDepthBound.cfg) holds DomainsOK and three invariants, each commented with the Rust it mirrors. DepthBoundedByRoot: a minted link’s depth is at most DEPTH_MAX and its parent’s plus one unless it is a root (chainWithinDepth in validate_delegation_chain). AttenuatedAtEachStep: every minted link is attenuated relative to its parent, roots vacuously (the pre-mint subset check in Capability::delegate). RevokedSubtreeNotObservable: a link a peer observes as revoked is in the issuer’s revoked set (the monotone-epoch fail-closed check in RevocationView::install_if_newer).

formal/apalache/PostAdmissionDropGuard.tla, 659 lines, owns its shard. It models what the armed drop guard does with receipts and reserved resources when a tool-call future is dropped, errors, or streams incompletely after admission commits, over two invocations, one buffered child, and four ledger resources.

SafetyInv ==
    /\ DomainsOK
    /\ ReservationConservation
    /\ TerminalReceiptExactlyOne
    /\ ChildReceiptsFlushed
    /\ RetainedIffAborted

• ReservationConservation. The counted reservation partition and shared active-child capacity hold in every bounded lifecycle state. hold is the kernel budget hold, and lease conservatively projects destructive, treaty, and swarm reservation identifiers; payment-adapter authorization sits outside the four-resource ledger.
• TerminalReceiptExactlyOne. A committed parent append has exactly one receipt, an outcome-unknown append has at most one, and a clean pre-dispatch unwind stays receipt-free.
• ChildReceiptsFlushed. Every buffered child receipt is appended before its parent’s terminal receipt, assuming a successful child append is available; Rust retries only the not-attempted suffix.
• RetainedIffAborted. An admission lease stays retained after every non-allow post-dispatch terminal. A returned Ok output reaches reconciliation and commits its modeled hold; a server error or dropped future is outcome-unknown and retains it.

The action map pairs Admit with PostAdmissionDropGuard::new and the two evaluation entry points, StartDispatch with revalidate_immediately_before_dispatch and mark_dispatch_started, DropPreDispatch with handle_pre_dispatch_drop and ChioRuntimeAdmissionHook::release_reservations, and DropPostDispatch with flush_buffered_child_receipts_from_drop and ambiguous_dispatch_receipt_metadata.

SPECIFICATION Spec

CONSTANTS
    Invocations = {1, 2}
    ChildMax = 1
    Mutation = "none"

INVARIANT
    SafetyInv

The manifest requires both a positive no-error result and a registered counterexample trace from every paired negative mutation. Exact per-identifier ownership after a mutate-then-error, payment-adapter state, and production ledger refinement stay unproved, and ASSUME-SQLITE-ATOMICITY covers the store transaction while acknowledgement certainty stays outside it.

Every lane reruns before a release, and each registered broken variant must fail

The six handwritten modules under formal/tla/ are, as DistributedRevocation.tla records, the artifact of record, consumed by a checker pinned to Apalache 0.50.1 with no extra compiler or package-distribution boundary. The wrapper re-checks that version at run time and refuses any other.

The apalache-safety workflow shards nine spec and config pairs across eight distinct specs, each with its own length bound and timeout: SafetyInv at length 6 for revocation propagation, at length 8 for the post-admission drop guard, and BehavioralSafetyInv at length 6 for distributed behavior. The config’s INVARIANT line selects the property, and the wrapper uses the row’s invariant name to validate the evidence afterwards. The apalache-temporal workflow checks RevocationEventuallySeen to length 24.

      - name: monotone-log
        config: formal/apalache/MCMonotoneLogApalache.cfg
        spec: formal/apalache/MonotoneLogApalache.tla
        length: 6
        timeout_seconds: 1800
        invariant: SafetyInv
      - name: revocation-cut
        config: formal/apalache/MCRevocationCutCompleteness.cfg
        spec: formal/apalache/RevocationCutCompleteness.tla
        length: 6
        timeout_seconds: 1800
        invariant: SafetyInv
      - name: receipt-before-allow
        config: formal/apalache/MCReceiptBeforeAllow.cfg
        spec: formal/apalache/ReceiptBeforeAllow.tla
        length: 6
        timeout_seconds: 1800
        invariant: SafetyInv
      - name: transition-cancel
        config: formal/apalache/MCKernelTransitionCancelSafe.cfg
        spec: formal/apalache/KernelTransitionCancelSafe.tla
        length: 6
        timeout_seconds: 1800
        invariant: SafetyInv
      - name: post-admission
        config: formal/apalache/MCPostAdmissionDropGuard.cfg
        spec: formal/apalache/PostAdmissionDropGuard.tla
        length: 8
        timeout_seconds: 10800
        invariant: SafetyInv
      - name: revocation-propagation
        config: formal/tla/MCRevocationPropagation.cfg
        spec: formal/tla/RevocationPropagation.tla
        length: 6
        timeout_seconds: 10800
        invariant: SafetyInv
      - name: distributed-domains
        config: formal/tla/MCDistributedRevocationDomains.cfg
        spec: formal/tla/DistributedRevocation.tla
        length: 0
        timeout_seconds: 600
        invariant: DistributedDomainsOK
      - name: distributed-behavior
        config: formal/tla/MCDistributedRevocation.cfg
        spec: formal/tla/DistributedRevocation.tla
        length: 6
        timeout_seconds: 1800
        invariant: BehavioralSafetyInv
      - name: delegation-depth
        config: formal/tla/MCDelegationDepthBound.cfg
        spec: formal/tla/DelegationDepthBound.tla
        length: 6
        timeout_seconds: 1800
        invariant: SafetyInv
steps:

A positive result counts because the invariant could have failed. formal/apalache/_negative_tests/ holds deliberately broken spec variants and rejected-claim witnesses, registered in REGISTRY.toml with the invariant each falsifies, the runtime regression test for the same defect, a length bound, and a timeout. The apalache-negative job, which apalache_verdict requires, checks every entry: a parse failure, timeout, unexpected exit code, missing error outcome, or invalid trace fails it, and an entry naming a property absent from formal/MAPPING.md is rejected before checking starts. DistributedRevocationSignerPinBroken.tla falsifies SignerPinnedHighWater, DropGuardSkipInvocationReversalBroken.tla and its siblings falsify the drop-guard conjuncts, and a mechanical mutation lane applies the curated probes in formal/apalache/spec-mutants-allowlist.toml.

The proof report records the positive and negative lanes against the release tag's source commit. Check them for the binary you run:

chio release verify --evidence formal

binary     /usr/local/bin/chio  chio 0.2.0  aarch64-apple-darwin
checksum   matches SHA256SUMS for v0.2.0
signed by  release.yml on backbay-labs/chio, issuer token.actions.githubusercontent.com
provenance SLSA v1, 5 subjects, tag v0.2.0
formal     proof report bound to v0.2.0, every gate passed
           lean        root-imported theorems checked
           aeneas      production extraction and equivalence
           kani        public PR lane
           apalache    positive and negative invariants
           creusot     core contracts
           diff-tests  scope, canonical JSON, receipts, treaties
           timing      dudect threshold
verified

The apalache line covers both the positive and the negative invariants. To rerun a shard from source, with a Java runtime, timeout, and the pinned checker, follow Qualification: formal gates; the longest shard is bounded at three hours.

A failing run writes a trace into formal/tla/counterexamples/ for triage:

1. Classify. Spec bug (the invariant asks more than the protocol promises), implementation bug (the Rust violates it), or config bug (the bounds admit a degenerate behavior).
2. File. Use formal/issue-templates/property-counterexample.md, or liveness-counterexample.md for a temporal failure.
3. Justify. Widening an invariant to silence a counterexample requires a written justification.

An invariant scopes an assumption; retiring one takes a refinement gate

Retiring an audited assumption, in formal/assumptions.toml’s words, “requires named model evidence and a concrete implementation-refinement gate over the affected production boundary”; abstract invariants and manual mirror hashes are insufficient by themselves. retired_assumption_ids, retired_assumptions, and the manifest’s discharged_assumptions are empty, so every assumption named here stays in required_assumption_ids, as Assumptions and TCB lists.

formal/MAPPING.md also pairs invariants with Lean theorems about the same code, as informational links the gate leaves unchecked:

• NoAllowAfterRevoke. evalToolCall_revoked_token_never_allows, evalToolCall_revoked_ancestor_never_allows, revocationSnapshot_revoked_token_denies, revocationSnapshot_revoked_ancestor_denies.
• MonotoneLog. applyProof_append, checkpoint_consistency, receiptFieldsCoupled_preserves_all_fields.
• AttenuationPreserving. scope_subset_of_grants_subset, added_constraint_is_subset, delegation_chain_integrity, capability_monotonicity.
• The drop-guard conjuncts. Chio.Proofs.ReservationLedger.ledger_conservation and ledger_terminal_unique, with two Kani harnesses and the runtime pair kernel/ledger_audit.rs and tests/property_reservation_ledger.rs. Scalar admission is linked; production ledger linkage is unestablished.

Next: the assumptions every invariant names