TLA+ Specs

A TLA+ module describes a system as a state machine plus a temporal formula constraining its behaviors. Chio keeps six handwritten modules under formal/tla/ and five Apalache invariant modules over a shared Common.tla under formal/apalache/. Each one names the Rust functions it abstracts, and formal/MAPPING.md carries a row per invariant recording the call sites it constrains and the assumption it rests on.

The checker

Every lane on this page runs Apalache, a symbolic model checker that translates the spec to SMT and asks the solver rather than enumerating reachable states. Its tableau encoding (PDR-017) is what makes the bounded liveness lane possible, and its restrictions are visible in the spec text: two of the shapes below exist because Apalache rejects the more natural form.

The specs are handwritten, and DistributedRevocation.tla:51-53 gives the reason in the spec itself: handwritten TLA+ is the artifact of record and the repository-pinned checker consumes it directly, avoiding an additional compiler and package-distribution boundary. The pin is 0.50.1, set by tools/install-apalache.sh:14 and re-checked at run time by scripts/check-apalache-positive.sh:97-101, which exits rather than run against any other version.

The pull-request safety lane

The apalache-safety workflow shards nine spec and config pairs across eight distinct specs. Both distributed shards run the same spec under different configs and different invariants. Each shard carries its own computation-length bound and its own timeout:

      - 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:

Each shard runs scripts/check-apalache-positive.sh with the matrix row's invariant, length, timeout, and config. The invariant name is not passed to Apalache on the command line; the config's INVARIANT line selects it, and the wrapper uses the name to validate the run's evidence afterwards.

Two more jobs run outside the pull-request lane. A scheduled job re-runs both distributed invariants at wider constants, and apalache-temporal runs the two liveness properties.

RevocationPropagation

formal/tla/RevocationPropagation.tla models how revocations propagate across authorities. Its six state variables are declared with Apalache type annotations at RevocationPropagation.tla:129-141: state (per-process, per-capability lifecycle), depth (delegation depth), rev_epoch (per-process revocation epoch, where 0 means not yet seen revoked), receipt_log (append-only per process), pending (the unordered set of in-flight propagation messages), and clock.

Lifecycle states are active, attenuated, and revoked. The next-state relation at RevocationPropagation.tla:260-264 has four shapes: Attenuate (delegate once, narrowing scope), Revoke (terminal), Evaluate (emit a receipt with the current epoch view), and PropagateAny (consume a pending message and update one process's epoch).

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

The third conjunct WF_vars(PropagateAny) is weak fairness on the named action PropagateAny: in any behavior where it stays continuously enabled (a pending propagation message exists for some recipient), the action eventually fires. Without that conjunct an infinite stutter where messages sit in pending forever would be a legal behavior and RevocationEventuallySeen would not hold. The spec preamble at RevocationPropagation.tla:266-287 records why weak fairness is sufficient here and strong fairness is not required.

The Rust mapping, from formal/MAPPING.md:53-58:

• state, depth → crates/core/chio-core-types/src/capability/scope.rs and crates/core/chio-core-types/src/capability/attenuation.rs
• rev_epoch → crates/kernel/chio-kernel-core/src/revocation_view.rs (RevocationSnapshot, RevocationView::install_if_newer)
• receipt_log → crates/platform/chio-store-sqlite/src/receipt_store.rs (append_chio_receipt_tx)
• clock → the injected clock behind ASSUME-OS-CLOCK

Safety invariants

The spec defines five named leaf safety invariants plus the structural DomainsOK. The aggregate SafetyInv is what the cfg file points INVARIANT at:

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

Read the body, not the comment above it. The block comment at RevocationPropagation.tla:357-362 describes the aggregate as three named safety invariants plus RevocationFreshness and DomainsOK, which is five. The definition beneath it conjoins six. The sixth, RevocationStateCoupled, is the one the comment omits.

scripts/check-mapping.sh enforces two separate things about this list. Every named invariant defined in the spec must have a row in formal/MAPPING.md (check-mapping.sh:128-163), and three invariants named at check-mapping.sh:39-43, one of them RevocationStateCoupled, must both be defined and appear as a conjunct of their spec's SafetyInv. Deleting a definition or dropping it from the conjunction fails the gate even if the mapping row survives.

NoAllowAfterRevoke

Every allow receipt was issued at a time when the issuing authority had not yet observed any revocation for that capability. Causal allow-before-revoke histories are admitted; allows after the issuer's local revoke-view are forbidden.

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

The mapping row constrains ChioKernel::revoke_capability, ChioKernel::check_revocation, both async evaluation paths, and RevocationSnapshot::is_revoked. Its assumption column reads ASSUME-SQLITE-ATOMICITY for single-row commits, and states in the same sentence that cross-row recovery is excluded. The invariant scopes that assumption; it does not remove it.

MonotoneLog

Per-authority receipt-log timestamps are strictly increasing. The append-only structure is enforced by each Evaluate using Append and no other action touching receipt_log; the strict order additionally forbids logical reordering inside the sequence.

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

Mapping: ChioKernel::record_chio_receipt, SqliteReceiptStore::append_chio_receipt_returning_seq, and append_chio_receipt_tx. The row names both ASSUME-SQLITE-ATOMICITY and ASSUME-OS-CLOCK, and adds that the storage anchors do not enforce strict timestamps.

AttenuationPreserving

Depth stays bounded by DEPTH_MAX; any capability in the attenuated state has been delegated at least once.

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

Mapping: validate_delegation_chain, ChioScope::is_subset_of, NormalizedScope::is_subset_of, and ChioKernel::validate_delegation_admission. This is the one row whose assumption column reads n/a: it is structural, bounded by DEPTH_MAX.

RevocationFreshness

Each recorded local revocation epoch is strictly less than the current clock: a non-zero rev_epoch[a][c] could only have been stamped by an earlier tick, so an observed revocation epoch never exceeds any clock value the model's actions could have produced.

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

Mapping: FreshnessConfig, verify_fresh_epoch_root, RevocationSnapshot, and RevocationView::install_if_newer. The row names ASSUME-OS-CLOCK as the assumption the property rests on.

RevocationStateCoupled

In the bounded model, a capability has a non-zero locally observed revocation epoch exactly when its local lifecycle state is revoked. The equality runs both ways, so neither variable can drift ahead of the other.

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

Mapping: RevocationSnapshot::is_revoked, RevocationView::install_if_newer, ChioKernel::check_revocation, and consult_revocation_view_at. The row records the abstraction gap in its own words: the runtime snapshot carries one global epoch and a revoked-subject set rather than a per-subject lifecycle state, so the coupling is a property of the model rather than a claim about the snapshot type.

Liveness: RevocationEventuallySeen

If any authority observes a non-zero local revocation epoch, the model eventually reaches a state where every authority has caught up to every observed epoch. The quantifiers sit inside two named state predicates rather than outside the leads-to operator, because Apalache 0.50.1 rejects free variables bound outside ~>, so the property itself must carry no temporal-bound variables:

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

The leads-to operator ~> is shorthand for [](P => <>Q): once any revocation has been observed, some later state satisfies the global catch-up predicate. The model admits only finitely many Revoke actions per bounded authority and capability pair, which is why the spec preamble at RevocationPropagation.tla:394-398 treats the aggregate form as equivalent to the per-pair obligation.

The property is gated on WF_vars(PropagateAny) declared in Spec. The named-action form is required because Apalache's tableau encoding supports WF_vars(<named action>) but rejects an existential nested directly under WF_vars; the spec introduces PropagateAny as the named-action workaround.

Mapping: RevocationGossipPushQueue::enqueue_signed_root, flush_batches_at, RevocationCatchupResponse::validate_response, and respond_to_catchup. The row records that the property rests on the model-only fairness conjunct and that ASSUME-NETWORK-TRANSPORT remains audited and does not guarantee delivery.

Model configuration

The pull-request config is nine lines:

SPECIFICATION Spec

CONSTANTS
    PROCS = 4
    CAPS = 8
    DEPTH_MAX = 4

INVARIANT
    SafetyInv

The liveness lane uses a second config with the same constants:

SPECIFICATION Spec

CONSTANTS
    PROCS = 4
    CAPS = 8
    DEPTH_MAX = 4

INVARIANT
    SafetyInv

The two configs differ only in filename. The temporal run keeps the INVARIANT SafetyInv line and adds --temporal RevocationEventuallySeen at --length 24 with a 3600-second timeout, per .github/workflows/apalache-temporal.yml:54-63. Depth, not width, is what the liveness lane buys.

DistributedRevocation

formal/tla/DistributedRevocation.tla is the largest spec in the tree at 601 lines. It models signed revocation-root gossip over bilateral peers, and its action map at DistributedRevocation.tla:5-15 names the production function behind each action: QueueRoot for RevocationGossipPushQueue::enqueue_signed_root, Send for flush_batches_at, RejectForged for RevocationRootGossip::validate_envelope with SignedEpochRoot::verify, Deliver for RevocationView::install_if_newer, Catchup for the catch-up request and response pair, and Evaluate for consult_revocation_view_at.

Loss, duplication, reordering, and forged frames are actions in the model rather than assumptions excluded from it. Channels are counting functions: Duplicate increments a count, Lose decrements one without delivering, and Deliver may pick any epoch with a positive count, so delivery order is arbitrary. forgedChannel is a separate adversarial input.

The spec carries two aggregate invariants and the two safety shards check one each. The first checks the concrete initial state:

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

The second is the bounded path check:

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

The two shards differ only in their config's INVARIANT line and in the computation length the workflow passes. The behavioral config runs at length 6; the domains config runs at length 0, because it checks the shape of the initial state rather than a path through it.

SPECIFICATION Spec

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

INVARIANT
    BehavioralSafetyInv

The rows above are formal/MAPPING.md:82-85 and :87. This lane is P2's distributed_apalache evidence in the manifest property matrix at formal/proof-manifest.toml:162.

The invariant kept out of SafetyInv

RejectedRawEvaluationCountBound is defined at DistributedRevocation.tla:597-599 and deliberately excluded from the aggregate. It would say observation occurs within a finite number of raw evaluations, and the spec preamble at DistributedRevocation.tla:43-45 records that a registered witness demonstrates arbitrary loss permits more evaluations than any finite count before observation. Its mapping row says the same thing in the assumption column: explicitly not discharged or claimed, with a registered claim-witness counterexample. No production rate limiter exists.

The scheduled lane re-runs both invariants at three authorities and four epochs with a channel cap of 3, using MCDistributedRevocationDomainsNightly.cfg and MCDistributedRevocationNightly.cfg at .github/workflows/apalache-safety.yml:234-249. Conditional liveness lives in a separate four-variable projection, formal/tla/DistributedRevocationTemporal.tla, run by scripts/check-distributed-revocation-temporal.sh.

PostAdmissionDropGuard

formal/apalache/PostAdmissionDropGuard.tla is 659 lines and owns its own shard at computation length 8 with a 10800-second timeout. It models the lifecycle of an armed post-admission drop guard: what happens to receipts and reserved resources when a tool-call future is dropped, errors, or streams incompletely after admission has already committed.

Its action map at PostAdmissionDropGuard.tla:5-34 pairs each modeled action with the Rust it abstracts: 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.

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

Those rows are formal/MAPPING.md:191-194. The config is three constants:

SPECIFICATION Spec

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

INVARIANT
    SafetyInv

The manifest scopes this evidence at formal/proof-manifest.toml:241: the lifecycle is model-checked at two invocations and one buffered child per invocation, and the evidence requires both a positive no-error result and every paired negative mutation producing a registered counterexample trace. The mapping rows add the concrete boundaries: 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 rather than acknowledgement certainty.

DelegationDepthBound

formal/tla/DelegationDepthBound.tla is a 233-line spec that bounds delegation depth across peer authorities. Its config formal/tla/MCDelegationDepthBound.cfg pins DEPTH_MAX = 4 and PEERS = 3. Three named safety invariants sit under its own SafetyInv at DelegationDepthBound.tla:227-231, alongside DomainsOK. Each one carries a block comment naming the Rust it mirrors, quoted below from DelegationDepthBound.tla:188-217:

• DepthBoundedByRoot · every minted delegation link sits at depth at most DEPTH_MAX, and its depth equals its parent's depth plus one unless it is a root. Mirrors validate_delegation_chain's chainWithinDepth check.
• AttenuatedAtEachStep · every minted link marks itself attenuated relative to its parent; roots are vacuously attenuated. Mirrors Capability::delegate's pre-mint scope-subset check.
• RevokedSubtreeNotObservable · every link a peer has observed as revoked is in the issuing authority's revoked set, so no peer can observe a revocation that has not been issued. Mirrors RevocationView::install_if_newer's monotone-epoch fail-closed check.

The kernel-state subset

formal/apalache/ holds five invariant modules extending a shared Common.tla. Between them they carry ten named invariants, listed at formal/MAPPING.md:185-194. The directory's own README.md:10-18 gives the shared reference bounds for what it calls the original four specs: Authorities = 1..3, CapSet = 1..6, EpochMax = 4, mirroring a bounded CI runner contract of a hosted ubuntu-24.04, the Z3 default solver, and a thirty-minute per-invariant timeout. Those four run at length 6; ReceiptBeforeAllow adds CallSet = {1, 2}. README.md:20-26 then gives PostAdmissionDropGuard a purpose-built state space instead: two invocations, one buffered child, four ledger resources, and a positive bound of 8.

formal/proof-manifest.toml:245 scopes the ReceiptBeforeAllow result in the manifest's own words: it proves the abstract persist-before-publish ordering and its production replay exercises the native happy path, and it does not discharge concrete cross-row crash recovery, which remains excluded until implementation trace validation and crash-reopen conservation gates establish refinement.

formal/apalache/CONTRACTOR-SIGNOFF.md records that this subset is an internal, self-authored verification record. Its header states that no third-party vendor has reviewed, run, or countersigned the results, and that every result in it is the maintainers' own claim rather than independently verified evidence.

Negative calibration

A positive result only means something if the invariant could have failed. formal/apalache/_negative_tests/ holds deliberately broken spec variants and explicit rejected-claim witnesses, registered in REGISTRY.toml with the exact invariant each one falsifies, the runtime regression test for the same defect, a length bound, and a timeout.

The apalache-negative job runs scripts/check-apalache-negative.sh over that registry at .github/workflows/apalache-safety.yml:308-344, and apalache_verdict lists it among the jobs it requires. A parse failure, timeout, unexpected exit code, missing error outcome, or invalid trace fails the job rather than passing as a caught defect. Registry entries naming a property absent from formal/MAPPING.md are rejected before model checking starts.

The registry entries cover both lanes this page describes: DistributedRevocationSignerPinBroken.tla falsifies SignerPinnedHighWater, and DropGuardSkipInvocationReversalBroken.tla and its siblings falsify the drop-guard conjuncts. A separate mechanical mutation lane applies the curated probes registered in formal/apalache/spec-mutants-allowlist.toml.

Counterexamples

A failing run writes a trace into formal/tla/counterexamples/. Triage path:

• Classify: spec bug (the invariant says something the protocol is not supposed to satisfy), implementation bug (the Rust code violates the invariant), or config bug (the cfg bounds let a degenerate behavior through).
• File via formal/issue-templates/property-counterexample.md, or liveness-counterexample.md for a temporal failure.
• Counterexamples are not silenced by widening the invariant without a written justification.

Lean cross-reference

The TLA+ invariants and the Lean theorems prove related properties about the same code at different levels of detail. formal/MAPPING.md:90-111 marks these informational; the gate does not enforce them.

• 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.
• formal/MAPPING.md:123-131 joins the PostAdmissionDropGuard conjuncts to 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 not established.

Reproduce

Every lane goes through one wrapper, so a local run is the same command CI runs with the matrix row substituted. The wrapper needs a Java runtime, the timeout command, and Apalache 0.50.1 on PATH; it exits 2 rather than running against any other Apalache version.

./tools/install-apalache.sh
export PATH="$HOME/.local/bin:$PATH"

# revocation-propagation shard
./scripts/check-apalache-positive.sh \
  --invariant SafetyInv \
  --length 6 \
  --timeout-seconds 10800 \
  --config formal/tla/MCRevocationPropagation.cfg \
  formal/tla/RevocationPropagation.tla

# post-admission shard
./scripts/check-apalache-positive.sh \
  --invariant SafetyInv \
  --length 8 \
  --timeout-seconds 10800 \
  --config formal/apalache/MCPostAdmissionDropGuard.cfg \
  formal/apalache/PostAdmissionDropGuard.tla

# distributed-behavior shard
./scripts/check-apalache-positive.sh \
  --invariant BehavioralSafetyInv \
  --length 6 \
  --timeout-seconds 1800 \
  --config formal/tla/MCDistributedRevocation.cfg \
  formal/tla/DistributedRevocation.tla

The liveness lane swaps --invariant for --temporal:

./scripts/check-apalache-positive.sh \
  --temporal RevocationEventuallySeen \
  --length 24 \
  --timeout-seconds 3600 \
  --config formal/tla/MCRevocationPropagationTemporal.cfg \
  formal/tla/RevocationPropagation.tla

The mapping gate needs no toolchain at all and is the cheapest way to check that a new invariant is wired correctly: ./scripts/check-mapping.sh. These commands are transcribed from .github/workflows/apalache-safety.yml:120-199 and .github/workflows/apalache-temporal.yml:54-63; no captured output accompanies them here because the runs need a pinned Apalache install and the longest shard is bounded at three hours.

Next

• Assumptions and TCB · the registry every invariant on this page names, and what retiring an entry would take.
• Theorem Inventory · the Lean theorems mapped to these invariants.
• Bilateral Federation · the protocol interface the propagation and gossip specs model.