Checks and Qualification
Run the verification gate, the drift and fixture checks, and the behavioral gates that every change to Chio passes.
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.
cargo build --workspace && \
cargo test --workspace && \
cargo clippy --workspace -- -D warnings && \
cargo fmt --all -- --checkThe Makefile wraps the gate and the broader tiers:
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 qualificationThe 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.
| Group | Leaves | Use 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-, crate-paths, formal-mirrors, fixtures <facet> | Assert a structural property of the workspace, or run one fixture- |
qualify | bounded-chio | Assert the bounded release qualification matrix. |
verify | launch- | Assemble and verify the public Proof Room acceptance package. |
formal | itf- | 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.
cargo xtask snippets regen # regenerate the editor snippet files
cargo xtask snippets regen --check # compare without writingThe 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 --checksnippets in sync (4 snippet sources)
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.
cargo xtask check fixtures runtime-policy
cargo xtask check fixtures runtime-spine --schema-onlyThe 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.
./scripts/check-adapter-no-bypass.sh
./scripts/check-formal-proofs.shRelease 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.
./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.pyFormal 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.
./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 -- --nocaptureThe 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.
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-runNamed 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.
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.
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 ./...) # GoRelease 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.
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.shReproducible 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.
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.
cd examples
./run-hello-smokes.sh --listhello-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.
./run-hello-smokes.sh hello-fastapi hello-fastifyContainer 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.