Federation Assurance

Each federation result names its method and the object it covers

Six methods reach seven federation objects. Only the bilateral verifier is covered twice, by test and by measurement.

Status words scope each claim: modeled for a TLA+ or loom model, tested for a suite that runs the code, fuzzed for a target that feeds generated inputs, and measured for a bench. Proved results about the kernel's core are listed on Formal verification.

Five TLA+ specifications model revocation across operators

RevocationPropagation.tla and the DistributedRevocation family check safety and temporal properties of revocation propagation over a bounded model, including named channel and partition behavior. Each specification has model-checking configurations beside it:

• formal/tla/RevocationPropagation.tla
• formal/tla/DistributedRevocation.tla
• formal/tla/DistributedRevocationTemporal.tla
• formal/tla/DistributedRevocationTemporalRefinement.tla
• formal/tla/DistributedRevocationTemporalWitness.tla

The formal manifest ties the model to code: its Rust scope names functions from chio_federation::revocation_gossip. The coverage manifest counts each method against the federation and revocation-oracle surfaces. Proof coverage for the federation methods is part of each release's formal report; chio release verify --evidence formal checks it:

Read more in TLA+ specs.

Conformance suites hold the verifiers to their profiles, and fuzz targets feed the parsers

Four suites in chio-conformance run the bilateral verifier and quorum authorization against their profiles:

• b4_bilateral_dsse_pae_conformance.rs and b4_bilateral_dsse_signature_slice.rs: the cosigner-routed PAE profile verifies, a bare signature-slice envelope is rejected under the strict configuration, and the signature-slice profile verifies under its own predicate.
• c2_bilateral_invocation_partial_verifier.rs: the partial verifier rejects each single-field tamper with its section 7.1 code, which covers a subset of section 7.
• frost_quorum.rs: FROST quorum authorization binds the registered action and roster.

Two fuzz targets, federation_trust_establishment and revocation_oracle_merkle, feed handshake envelopes and revocation Merkle inputs. The transport's loom models in limits_loom.rs check that the per-peer accept counter and the directory swap are race-free; they run in the release's qualification lane, and chio release verify --evidence qualification shows their result for the release you run. A criterion bench, bilateral_verify.rs, measures bilateral verification throughput.

Read more in Fuzz infrastructure.

The qualification matrix names one case for each requirement

A matrix covers TRUSTMAX-01 through TRUSTMAX-05. The validator in qualification.rs checks the schema, the references, unique case ids, and coverage of all five requirements, and reference_artifacts_parse_and_validate parses and validates the reference exchange, quorum report, admission policy, and clearing. The published matrix holds five cases:

1. activation-exchange (TRUSTMAX-01, conflicting_activation). Remote trust activation stays an explicit exchange contract and never becomes ambient runtime trust.
2. quorum-conflict (TRUSTMAX-02, insufficient_quorum). Conflicting or stale publisher state fails closed.
3. open-admission-boundary (TRUSTMAX-03, governance_interop). Open admission stays bounded by explicit stake and review policy, and participation stays distinct from runtime trust.
4. shared-reputation-sybil (TRUSTMAX-04, reputation_sybil). Accepted summaries come from distinct issuers, and blocking negative events need corroboration.
5. adversarial-federation (TRUSTMAX-05, eclipse_attempt). Hostile publisher and eclipse inputs stay visible and fail closed under the federation boundary.

{
  "schema": "chio.federation-qualification-matrix.v1",
  "profileId": "chio.federation.profile",
  "exchangeRef": "fex-1",
  "quorumReportRef": "fqr-1",
  "reputationClearingRef": "frc-1",
  "cases": [
    {
      "id": "activation-exchange",
      "name": "Federated activation exchange stays visibility-first and locally reviewable",
      "requirementIds": [
        "TRUSTMAX-01"
      ],
      "scenario": "conflicting_activation",
      "expectedOutcome": "pass",
      "observedOutcome": "pass",
      "notes": "Remote trust activation remains an explicit exchange contract and never becomes ambient runtime trust."
    },
    {
      "id": "quorum-conflict",
      "name": "Quorum, freshness, and anti-eclipse posture remain machine-reviewable",
      "requirementIds": [
        "TRUSTMAX-02"
      ],
      "scenario": "insufficient_quorum",
      "expectedOutcome": "pass",
      "observedOutcome": "pass",
      "notes": "Conflicting or stale publisher state fails closed instead of silently rewriting trust."
    },
    {
      "id": "open-admission-boundary",
      "name": "Open admission stays bounded by explicit stake and review policy",
      "requirementIds": [
        "TRUSTMAX-03"
      ],
      "scenario": "governance_interop",
      "expectedOutcome": "pass",
      "observedOutcome": "pass",
      "notes": "Visibility and participation stay distinct from runtime trust, even when bond-backed admission is allowed."
    },
    {
      "id": "shared-reputation-sybil",
      "name": "Shared reputation clearing resists duplicate-issuer and oracle collapse",
      "requirementIds": [
        "TRUSTMAX-04"
      ],
      "scenario": "reputation_sybil",
      "expectedOutcome": "pass",
      "observedOutcome": "pass",
      "notes": "Accepted summaries come from distinct issuers and blocking negative events require corroboration."
    },
    {
      "id": "adversarial-federation",
      "name": "Hostile publisher and eclipse attempts fail closed under the federation boundary",
      "requirementIds": [
        "TRUSTMAX-05"
      ],
      "scenario": "eclipse_attempt",
      "expectedOutcome": "pass",
      "observedOutcome": "pass",
      "notes": "Hostile federation inputs remain visible but do not collapse governance or admission into ambient trust."
    }
  ]
}

Every case expects pass and records pass. Two schemas under spec/schemas/chio-federation/v1/, treaty-negative-fixture-corpus.schema.json and treaty-runtime-negative-fixture-corpus.schema.json, define fixture corpora a treaty implementation must refuse. An implementation that admits any fixture in them is non-conforming.

The comptroller qualification reruns the cross-operator flow from source

From a checkout of github.com/backbay-labs/chio, ./scripts/qualify-comptroller-federation.sh builds the chio-cli tests into its own target directory and runs four stages in order: multi-hop lineage, evidence import, reconciliation review, and an adversarial open market. It snapshots the proof matrix, then writes a report and a checksum list once every stage exits zero. The procedure is docs/release/CHIO_COMPTROLLER_FEDERATED_PROOF.md.

The lineage stage runs trust_service_federated_issue_supports_multi_hop_imported_upstream_parent, which issues downstream from an imported upstream capability and keeps that parent visible in a four-entry lineage. The import stage runs evidence_import_roundtrip_surfaces_imported_trust_without_rewriting_local_history. The evidence exchange walkthrough runs the same flow with the installed CLI.

$ wc -l target/release-qualification/comptroller-federation/SHA256SUMS
$ ls target/release-qualification/comptroller-federation/logs

       7 target/release-qualification/comptroller-federation/SHA256SUMS
adversarial-open-market.log
evidence-import.log
multi-hop-lineage.log
reconciliation-review.log

You should see a seven-line SHA256SUMS covering every stage log, the matrix snapshot, and the report, with one log per stage. A failing stage stops the script with a nonzero exit and keeps its log under logs/; read that log's first error before rerunning. Save a failed bundle under another name, because the next run rebuilds the output from scratch, and fix the cause before regenerating; the checksum list stays as the run wrote it.

Every result stops at its model or its inputs

The TLA+ and loom results hold for their models, and the suites and fuzz targets for the inputs they run; none is a proof over the Rust runtime. A fuzz target identifies the surface it exercises and carries no universal no-panic guarantee. A partner's infrastructure is outside every result here.

The conformance tier a peer presents at the handshake is the peer's own claim. Your kernel holds it to the floor you set on Peer handshake.

Next: see what is proved about the kernel's core