Chio/Docs

Checks and Qualification

Run the verification gate, the drift and fixture checks, and the behavioral gates that every change to Chio passes.

Guide chio@5f63e6e

On this page

Every pull request passes one minimal gate, then the checks that cover what it touched. A schema change runs the codegen drift gate; a verifier change runs its fixture facet; a security behavior has a script that exits non-zero the moment it breaks.

The verification gate

Run all four from the checkout root before you open a pull request. Each must pass.

From the checkout rootbash
cargo build --workspace && \
cargo test --workspace && \
cargo clippy --workspace -- -D warnings && \
cargo fmt --all -- --check

The Makefile wraps the gate and the broader tiers:

From the checkout rootbash
make help           # list every target by tier
make gate           # the four commands above
make ci             # the pull-request tier that CI runs
make codegen-check  # schema and codegen drift
make ci-workspace   # the heavier gate run before release qualification

The xtask runner

cargo xtask is the workspace task runner. Commands are grouped by what they produce or check; cargo xtask <group> --help lists each group's leaves.

GroupLeavesUse it to
gen
codegen, errors, snippets, eval-receipt, freeze-vectors, proof-coverage
Regenerate output from its source; each leaf takes --check to compare without writing.
check
adapter-no-bypass, crate-paths, formal-mirrors, fixtures <facet>
Assert a structural property of the workspace, or run one fixture-and-schema facet.
qualify
bounded-chio
Assert the bounded release qualification matrix.
verify
launch-acceptance
Assemble and verify the public Proof Room acceptance package.
formal
itf-to-regression
Turn an Apalache ITF trace into an executable Rust regression test.
release
rust-preview
Assemble an offline Rust registry and an external consumer outside the checkout.

Drift gates

Generated files are committed, and a drift gate fails when one no longer matches its source. The editor snippets are an example: their sources are tool-neutral YAML at integrations/editors/snippets/*.snippet.yaml, validated against a JSON schema, and the build renders them into each editor's native format with a generated by cargo xtask snippets regen header.

From the checkout rootbash
cargo xtask snippets regen          # regenerate the editor snippet files
cargo xtask snippets regen --check  # compare without writing

The check form prints one line and exits zero when the generated files match. The .github/workflows/spec-drift.yml job runs the same invocation. If it fails, run the command without --check and commit what it writes.

cargo xtask snippets regen --checktranscript
$ cargo xtask snippets regen --check
snippets in sync (4 snippet sources)
exit 0in Chio source checkout

The error registry follows the same pattern: edit spec/errors/registry.yaml, then run cargo xtask gen errors to regenerate the Rust codes the CLI and the kernel return.

Fixture facets

A facet is one named fixture-and-schema gate. The runtime facets are listed in ci-gates/runtime.toml and the signal facets in ci-gates/pheromone.toml; an unknown facet name fails. --schema-only validates schemas and metadata without the cargo tests, and --negative-only runs only the negative corpus.

From the checkout rootbash
cargo xtask check fixtures runtime-policy
cargo xtask check fixtures runtime-spine --schema-only

The proof fixture corpus describes the signed scenarios behind the verifier facets.

Behavioral gate scripts

Each scripts/check-*.sh exercises one named behavior and exits non-zero when it breaks: adapter mediation, cage enforcement, the formal proofs, a language SDK's release build. Run the scripts for the area you changed; CI runs them by tier. Behavioral gates lists the security set and what each one proves.

From the checkout rootbash
./scripts/check-adapter-no-bypass.sh
./scripts/check-formal-proofs.sh

Release qualification runs from scripts/qualify-release.sh. It needs node and python3 on PATH and writes its conformance results, logs, coverage, checksums, and signed artifact manifest under target/release-qualification.

Security gates

The security pages state each guarantee once and point here for the gate that holds it. Each script exits non-zero when its behavior breaks; the release workflow runs all of them and records the result in the qualification evidence a reader checks with chio release verify --evidence qualification. chio security selftest runs the behavior suites among them (cage, restart, caller delivery, deception, temporal, keyring, broker) against an installed release.

From the checkout rootbash
./scripts/check-adapter-no-bypass.sh
./scripts/check-http-egress-contract.sh
./scripts/check-sre-metrics-registry.sh
./scripts/check-cage-enforcement.sh --release
./scripts/check-native-restart-safety.sh
./scripts/check-authenticated-caller-delivery.sh
./scripts/check-deception-security.sh
./scripts/check-temporal-security.sh
./scripts/check-keyring-transparency.sh
./scripts/check-secret-broker-boundary.sh
./scripts/check-security-dependencies.sh
./scripts/check-security-provenance.sh
./scripts/check-threat-coverage.sh
./scripts/check-threat-coverage-mutants.sh
./scripts/check-portable-kernel.sh
./scripts/check-liability-roster-enforcement.sh
python3 scripts/check-rust-toolchain-parity.py

Formal gates

The formal pages describe what each method proves. These are the commands that prove it, with the pinned toolchains from formal/toolchains.toml. The release workflow signs the proof report they produce, and chio release verify --evidence formal checks it against an installed binary.

From the checkout rootbash
./scripts/check-formal-proofs.sh          # Lean roots and the theorem registry
./scripts/check-kani-public-core.sh       # the public Kani lane
./scripts/check-aeneas-production.sh      # production extraction
./scripts/check-aeneas-equivalence.sh
./scripts/check-creusot-core.sh
./scripts/check-rust-verification-gates.sh
./scripts/check-apalache-positive.sh
./scripts/check-apalache-negative.sh
./scripts/check-mapping.sh                # TLA+ invariant to MAPPING.md rows
./scripts/check-proof-report.sh
bash scripts/check-programmable-sovereignty-artifact.sh --full
cargo xtask check formal-mirrors
cargo xtask gen proof-coverage --check
cargo test -p chio-formal-diff-tests
cargo test -p chio-arena --test determinism_gate -- --nocapture

The constant-time harnesses set harness = false and parse their own arguments, so name each test binary and leave libtest flags off. The threshold check prints one dudect verdict: line with max|t| against 4.5.

From the checkout rootbash
cargo test -p chio-kernel-core --features dudect --release --test dudect_mac_eq
cargo test -p chio-kernel-core --features dudect --release --test dudect_scope_subset
cargo test -p chio-credentials --features dudect --release --test dudect_jwt_verify
bash scripts/check-dudect-threshold.sh --dry-run

Named source tests

Several reader pages cite one test as the evidence for a behavior: the trust-control quorum drill, the restart that terminalizes an unrecorded dispatch, the budget-exhaustion flow, the Colorado control suites, and the iroh transport with its loom model. Run them by name.

From the checkout rootbash
cargo test -p chio-cli --test trust_cluster \
  trust_control_cluster_requires_quorum_and_heals_after_partition -- --exact --nocapture
cargo test -p chio-kernel --test durable_admission_sqlite \
  sqlite_restart_terminalizes_an_unrecorded_dispatch_without_moving_funds -- --exact
cargo test -p chio-e2e --test full_flow full_flow_budget_exhaustion -- --exact
cargo test -p chio-kernel -- checkpoint dpop monetary retention
cargo test -p chio-manifest -- sign_and_verify_manifest
cargo test -p chio-federation-transport-iroh
RUSTFLAGS="--cfg chio_iroh_transport_loom" cargo test -p chio-federation-transport-iroh --lib loom_

The bindings conformance suite runs the same vectors in every language. Readers run it against published packages with chio conformance run.

From the checkout rootbash
cargo test -p chio-conformance                 # Rust reference
(cd sdks/typescript/chio-ts && npm test)       # TypeScript
(cd sdks/python/chio-py && pytest)             # Python
(cd sdks/go/chio-go && go test ./...)          # Go

Release lanes

A release passes the bounded qualification matrix, the seven trust-control drills, the input check, and each package's release build. chio release check reads the result for an operator deciding whether a node can move to the release.

From the checkout rootbash
cargo xtask qualify bounded-chio
./scripts/qualify-trust-control.sh
./scripts/check-release-inputs.sh
./scripts/check-chio-py-release.sh
./scripts/check-chio-ts-release.sh
./scripts/check-chio-go-release.sh
./scripts/check-dashboard-release.sh
./scripts/qualify-release.sh

Reproducible build

check-reproducible-build.sh builds the chio binary twice from clean archives of the same commit in separate directories, with each build's path remapped away, and compares the outputs byte for byte. The release workflow attaches the signed result, which chio release verify --evidence reproducible checks.

From the checkout rootbash
git checkout "v\${VERSION}"
cargo fetch --locked
bash scripts/check-reproducible-build.sh --rev "v\${VERSION}" "$WORK_DIR"

Example smoke runner

The source tree carries a verifier for each protocol edge and framework adapter. The runner lists its 14 targets and runs any subset of them by name.

From the checkout rootbash
cd examples
./run-hello-smokes.sh --list
Output
hello-openapi-sidecar
hello-trust-control
hello-receipt-verify
hello-fastapi
hello-fastify
hello-chi
hello-express
hello-django
hello-elysia
hello-spring-boot
hello-dotnet
hello-mcp
hello-a2a
hello-acp

Each target runs its own smoke.sh. The HTTP verifiers share examples/_shared/hello-http-common.sh for ports, readiness, and trust-service setup; copy the helper with a verifier when you move it into another CI.

From examples/bash
./run-hello-smokes.sh hello-fastapi hello-fastify

Container verifier

The Docker example defines a trust service and a hosted MCP edge in compose.yaml, with a mock MCP server and a smoke client. Its README covers startup, health checks, the smoke run, and teardown.

Next: the fixture corpus