TLA+ Specs

TLA+ is a temporal-logic specification language for distributed and concurrent systems. Chio uses TLA+ for the one surface that Lean cannot easily reach: the cross-authority revocation propagation protocol, where the property of interest involves multiple processes, message passing, and weak fairness over an infinite-execution semantics.

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 nightly --temporal= 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

The single chio 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/chio-core-types/src/capability.rs
• rev_epoch → crates/chio-kernel/src/capability_lineage.rs
• receipt_log → crates/chio-kernel/src/receipt_store.rs
• clock → kernel monotonic receipt counter

Safety Invariants

The spec contains three 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/chio-kernel-core/src/evaluate.rs::evaluate and crates/chio-kernel/src/capability_lineage.rs. Discharges ASSUME-SQLITE-ATOMICITY per-row.

MonotoneLog

Per-authority receipt-log timestamps are strictly increasing. The append-only structural shape is enforced by every 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/chio-kernel/src/receipt_store.rs. Jointly with the per-row budget invariant in crates/chio-kernel/src/budget_store.rs this discharges the prior RETIRED-SQLITE-CROSS-ROW assumption.

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

Liveness: RevocationEventuallySeen

The single named liveness property. For every pair of authorities and every 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 every 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/chio-kernel/src/capability_lineage.rs, crates/chio-kernel/src/receipt_store.rs. Discharges ASSUME-PROPAGATE-FAIRNESS (weak fairness on Propagate).

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.

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

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 surface that the propagation spec models.
• On-Chain Settlement · how propagated revocations land in finality-gated evidence.