TLA+ Specs

What TLA+ Does

A TLA+ module describes a system as a state machine plus a temporal formula constraining its behaviors. Two checkers consume the spec:

• TLC · explicit-state model checker. Enumerates reachable states and looks for invariant violations or liveness counterexamples.
• Apalache · symbolic model checker that translates the spec to SMT and asks the solver. Strong on bounded liveness via its tableau encoding (PDR-017). Chio uses Apalache for the PR safety job and the nightly --temporal= liveness lane.

A clean run of either checker means: no reachable state violates a named invariant, and no infinite execution starves a named liveness property, within the configured bounds (PROCS, CAPS, DEPTH_MAX). Bounds are explicit per cfg file.

RevocationPropagation

This spec models how revocations propagate across authorities. State variables:

VARIABLES
    state,        \* per-process current view: ProcSet -> CapSet -> States
    depth,        \* delegation depth: ProcSet -> CapSet -> 0..DEPTH_MAX
    rev_epoch,    \* per-proc revocation epoch; 0 means not-yet-seen-revoked
    receipt_log,  \* append-only audit log per process
    pending,      \* unordered set of in-flight propagation messages
    clock         \* monotonic clock, advanced by Revoke and Evaluate

Per-process per-capability lifecycle states are active, attenuated, and revoked. The next-state relation 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).

The spec, quoted verbatim from RevocationPropagation.tla:259-262:

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 PropagateAny 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 mapping to Rust (in formal/MAPPING.md):

• state, depth → crates/core/chio-core-types/src/capability/scope.rs
• rev_epoch → crates/kernel/chio-kernel/src/capability_lineage.rs
• receipt_log → crates/kernel/chio-kernel/src/receipt_store.rs
• clock → kernel monotonic receipt counter

Safety Invariants

The spec contains four named safety invariants. The aggregate SafetyInv is what the cfg file points INVARIANT at, but the gate scripts/check-mapping.sh greps for each individual leaf invariant.

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

Mapping: constrains crates/kernel/chio-kernel-core/src/evaluate.rs::evaluate and crates/kernel/chio-kernel/src/capability_lineage.rs. Discharges ASSUME-SQLITE-ATOMICITY per-row.

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.

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: crates/kernel/chio-kernel/src/receipt_store.rs. Together with the per-row budget invariant in crates/kernel/chio-kernel/src/budget_store.rs it constrains the cross-row ordering behind the retired RETIRED-SQLITE-CROSS-ROW assumption; the named discharge evidence is the Apalache ReceiptBeforeAllow invariant (below).

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: crates/core/chio-core-types/src/capability/scope.rs (ChioScope::is_subset_of), crates/kernel/chio-kernel-core/src/normalized.rs. Structural: bounded by DEPTH_MAX, no audited assumption needed.

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. This is the invariant that keeps a stale or future-dated revocation epoch off the allow path.

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

Mapping: crates/trust/chio-revocation-oracle/src/freshness.rs and crates/kernel/chio-kernel-core/src/revocation_view.rs. Discharges ASSUME-OS-CLOCK. The spec folds it into SafetyInv alongside the original three invariants.

Liveness: RevocationEventuallySeen

The named liveness property. For each pair of authorities and each capability, if one authority's local revocation epoch becomes non-zero, the other's eventually catches up.

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

The leads-to operator ~> is shorthand for [](P => <>Q). The property reads: in each state where rev_epoch[a][c] is non-zero, some later state satisfies rev_epoch[b][c] >= rev_epoch[a][c].

The property is gated on WF_vars(PropagateAny) declared in Spec. Without weak fairness the model admits behaviors where pending messages are starved forever and the property would not hold. 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: crates/kernel/chio-kernel/src/capability_lineage.rs, crates/kernel/chio-kernel/src/receipt_store.rs. The property rests on the weak-fairness conjunct WF_vars(PropagateAny) in Spec, not on a trust-base assumption. formal/MAPPING.md still tags this row with an assumption id that is not registered in formal/assumptions.toml, a known inconsistency in the mapping file.

Model Configuration

The PR config formal/tla/MCRevocationPropagation.cfg is nine lines, quoted verbatim:

SPECIFICATION Spec

CONSTANTS
    PROCS = 4
    CAPS = 8
    DEPTH_MAX = 4

INVARIANT
    SafetyInv

The PR gate greps for each leaf invariant name so each one is cited in the build log. The nightly liveness lane runs the same spec at PROCS=6, CAPS=16, DEPTH_MAX=4 and replaces the INVARIANT line with --temporal=RevocationEventuallySeen on the Apalache CLI.

Additional Apalache Models

RevocationPropagation.tla is one of six spec/config pairs the PR Apalache safety job checks. The others are a second TLA+ spec and the four-invariant Apalache kernel-state subset.

DelegationDepthBound

formal/tla/DelegationDepthBound.tla is a separate 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, aggregated under its own SafetyInv:

• DepthBoundedByRoot · every minted delegation link sits at depth at most DEPTH_MAX, and a non-root link is exactly one deeper than its parent. Mirrors validate_delegation_chain's depth 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 · a peer observes a link as revoked only if it is in the issuing authority's revoked set. Mirrors RevocationView::install_if_newer's monotone-epoch gate.

Kernel-State Subset

formal/apalache/ holds a focused Apalache subset: four trust-boundary invariants, each its own .tla/.cfg pair extending Common.tla. All share the reference bounds Authorities = 1..3, CapSet = 1..6, EpochMax = 4, with a 30-minute per-invariant timeout in CI.

formal/apalache/CONTRACTOR-SIGNOFF.md records that this subset is an internal review, not an external audit. A local-only _negative_tests/ suite of deliberately broken spec variants confirms the invariants can fail: each must produce a counterexample, and the suite is excluded from CI by design.

Running TLC and Apalache Locally

Install Apalache via the pinned installer:

./tools/install-apalache.sh

Run the safety lane:

apalache check \
  --inv=SafetyInv \
  --config=formal/tla/MCRevocationPropagation.cfg \
  formal/tla/RevocationPropagation.tla

Run the named-leaf invariants individually (the same set the gate greps for):

apalache check --inv=NoAllowAfterRevoke ...
apalache check --inv=MonotoneLog ...
apalache check --inv=AttenuationPreserving ...
apalache check --inv=RevocationFreshness ...

Run the delegation-depth spec and the Apalache kernel-state subset (the remaining five pairs the PR safety job checks):

apalache check \
  --config=formal/tla/MCDelegationDepthBound.cfg \
  formal/tla/DelegationDepthBound.tla

apalache check \
  --config=formal/apalache/MCReceiptBeforeAllow.cfg \
  formal/apalache/ReceiptBeforeAllow.tla

Run the liveness lane (long; nightly only):

apalache check \
  --temporal=RevocationEventuallySeen \
  --length=20 \
  --cinit=Init \
  formal/tla/RevocationPropagation.tla

Counterexamples

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

• Reproduce: rerun with the same --seed= if Apalache flagged a non-deterministic execution.
• Classify: spec bug (the invariant says something the protocol is not supposed to satisfy), implementation bug (the Rust code violates the invariant), config bug (the cfg bounds let a degenerate behavior through).
• File via formal/issue-templates/property-counterexample.md.
• Counterexamples must not be 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. From formal/MAPPING.md (informational, the gate does not enforce these):

• 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.

Next

• Theorem Inventory · the Lean theorems mapped to TLA+ invariants.
• Bilateral Federation · the protocol interface modeled by the propagation specification.
• On-Chain Settlement · how propagated revocations land in finality-gated evidence.