Formal Quickstart

formal/proof-manifest.toml lists gate_commands: the commands that reproduce the assurance posture the rest of this section describes. They are shell scripts under scripts/, two cargo xtask invocations and one cargo test, and each exits non-zero on failure. The manifest declares its primary toolchain as lean4, creusot, kani and aeneas, so most of the work of running the gates is installing those first.

What each gate prints

A gate succeeds by exiting zero. Every one also prints a line naming itself, which is the line to grep for when the gate runs inside a longer log:

The three gates that wrap a verifier also emit that verifier's own verdict inside the log: Kani prints VERIFICATION:- SUCCESSFUL once per harness, lake build prints Build completed successfully with the job count, and Apalache prints EXITCODE: OK above the wrapper's own line. Those are the lines that move if a proof breaks; the wrapper lines only tell you the script reached its end.

Prerequisites

Five toolchains pin to specific versions, and each pin lives in the source rather than in this page.

Rust

rust-toolchain.toml pins the channel to 1.94.1 with the minimal profile and the clippy and rustfmt components, and the workspace Cargo.toml sets rust-version = "1.94" on edition 2021. rustup reads the pin from the checkout, so no explicit rustup default is needed once rustup is present.

curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
source "$HOME/.cargo/env"
rustc --version  # rustc 1.94.1

Lean 4

The Lean toolchain pin lives at formal/lean4/Chio/lean-toolchain: leanprover/lean4:v4.28.0. Install elan; it reads the pin and downloads the matching toolchain on the first lake invocation inside formal/lean4/Chio. The Lean project requires a vendored Aeneas package from formal/lean4/vendor/aeneas and pulls Mathlib and its dependencies through lake-manifest.json, so the first build is long and later builds replay from formal/lean4/Chio/.lake.

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
source "$HOME/.elan/env"
elan --version

Kani

Kani is the bounded model checker for Rust on top of CBMC. It installs as a cargo subcommand. Chio pins cargo-kani 0.67.0 through CHIO_KANI_VERSION, which .github/workflows/formal-pr-smoke.yml, .github/workflows/nightly.yml and .github/workflows/release-qualification.yml all set to the same value, and the pull-request job verifies the installed version before running a harness.

cargo install kani-verifier --locked --version 0.67.0
cargo kani setup
cargo kani --version

Apalache

The TLA+ lane uses Apalache, not the older TLC model checker. tools/install-apalache.sh pins APALACHE_VERSION="0.50.1" together with the SHA-256 of the upstream release archive, unpacks it into ~/.local/share/apalache/apalache-0.50.1, and links the launcher at ~/.local/bin/apalache-mc. It refuses to run without a Java 17 or newer runtime on PATH, and warns when ~/.local/bin is not on PATH. The wrapper the gates call refuses any binary that does not report exactly 0.50.1.

./tools/install-apalache.sh
apalache-mc version

Aeneas and Charon

Aeneas extracts a functional model from Rust source through Charon. scripts/install-aeneas-toolchain.py reads the pinned release tag and per-architecture SHA-256 digests out of formal/aeneas/production.toml, downloads the archive for the host architecture, and installs aeneas, charon and charon-driver under target/formal/aeneas-toolchain/<arch>/bin. The production and equivalence gates refuse to run against anything else; the pilot gate accepts an aeneas and charon found on PATH.

./scripts/install-aeneas-toolchain.py

Other tools on PATH

• python3. Most gate scripts parse the registries with an inline Python block that imports tomllib and falls back to tomli. CI pins python-version: "3.12".
• rg (ripgrep) for the placeholder scan in scripts/check-formal-proofs.sh. The script falls back to grep -RInw when rg is missing.
• timeout, which scripts/check-apalache-positive.sh requires and refuses to run without.

Clone and bootstrap

Clone the source and warm the cargo cache. The first cargo fetch pulls the dependencies the formal checks use; later gate runs work offline.

git clone https://github.com/bb-connor/arc.git
cd arc
cargo fetch --workspace
( cd formal/lean4/Chio && lake build )

That last line is the expensive one. It elaborates Mathlib and the vendored Aeneas package as well as the Chio proof root, and everything it produces lands in formal/lean4/Chio/.lake. Continuous integration caches that directory keyed on the toolchain pin, the lakefile and the lake manifest, which is why a warm build finishes in seconds and a cold one does not.

Run each gate

Every command below runs from the root of the source checkout. The transcripts are the output of running them there at the pinned commit.

Lean root build and inventory check

scripts/check-formal-proofs.sh runs five stages in order, and prints a banner for each: a canonical-JSON Lean fixture drift check, lake build on the project at formal/lean4/Chio/, a literal sorry scan across the shipped Lean modules, an elaborated assumption-audit regression suite, and a Python pass that checks the proof manifest, the theorem inventory and the claim registry agree. A sorry anywhere under formal/lean4/Chio/Chio fails the gate rather than warning.

Filtered to the stage banners and the lines that carry a verdict, a warm run looks like this:

$ ./scripts/check-formal-proofs.sh 2>&1 \
  | grep -E '^(==>|Build completed|PASS:|formal proof check)'

==> Canonical JSON Lean fixture drift
==> Lean 4 proof build
Build completed successfully (1525 jobs).
==> Lean 4 placeholder scan
==> Elaborated Lean assumption audit regressions
PASS: elaborated Lean assumptions include public, private, and generated declarations
==> Proof manifest and theorem inventory sanity
formal proof check passed

Aeneas pilot, production, equivalence

Three scripts cover the Aeneas lanes. The pilot extracts formal/aeneas/verified_core.rs through Charon and then Aeneas into the Chio.AeneasPilot namespace, and fails unless the generated Funs.lean defines all six of time_window_valid, dpop_subset, budget_precheck, governed_approval_passes, evaluate_signature_time_scope and report_may_use_verified_label, and unless Types.lean defines inductive Decision.

$ ./scripts/check-aeneas-pilot.sh 2>&1 | grep -aE '^(==>|Aeneas pilot check)'

==> Charon extraction for Aeneas pilot
==> Aeneas Lean extraction for pure verified-core pilot
Aeneas pilot check passed

The production and equivalence lanes read the two [[sources]] entries in formal/aeneas/production.toml, crates/kernel/chio-kernel-core/src/formal_aeneas.rs and crates/economy/chio-credit/src/formal_economy.rs, and compare their re-extraction against the committed snapshots under formal/lean4/Chio/FormalAeneas and formal/lean4/Chio/FormalEconomy. Both refuse to run against an Aeneas binary whose digest does not match the pinned toolchain entry, so they need scripts/install-aeneas-toolchain.py first rather than an Aeneas on PATH.

./scripts/check-aeneas-pilot.sh
./scripts/check-aeneas-production.sh
./scripts/check-aeneas-equivalence.sh

The equivalence script writes target/formal/aeneas-production/equivalence-artifacts.json, tagged chio.aeneas-equivalence-artifacts.v1. That report carries a sha256 map over the snapshot files, the lakefile, the lake manifest and the toolchain report, the vendored Aeneas release tag and content digest, and the equivalence theorem registered for each generated symbol. It then elaborates Chio.Proofs.AeneasGeneratedEquivalence under the same Lean toolchain as the root build.

Kani public lane

scripts/check-kani-public-core.sh has no harness list of its own. It parses formal/rust-verification/kani-public-harnesses.toml with an inline Python block, cross-checks the registry against every #[kani::proof] function in crates/kernel/chio-kernel-core/src/kani_public_harnesses.rs and fails if either set holds a name the other does not, then runs cargo kani -p chio-kernel-core --lib --harness <name> --default-unwind 8 once per selected name. --no-unwinding-checks is added for every harness except the ones listed in the registry's unwinding_checks array.

--lane selects which set to run and defaults to pr; --list prints the selected names and exits before invoking Kani. The registry declares two lanes:

[lanes.pr]
description = "Kani harnesses run on pull requests touching the scoped paths (full sweep)"
harnesses = [
  "public_verify_capability_rejects_untrusted_issuer_before_signature",
  "public_normalized_scope_subset_rejects_widened_child",
  "public_normalized_scope_subset_rejects_value_widened_child",
  "public_normalized_scope_subset_rejects_identity_mismatch",
  "public_resolve_matching_grants_rejects_out_of_scope_request",
  "public_resolve_matching_grants_preserves_wildcard_matching",
  "public_evaluate_rejects_untrusted_issuer_before_dispatch",
  "public_sign_receipt_rejects_kernel_key_mismatch_before_signing",
  "public_sign_receipt_accepts_matching_kernel_key",
  "public_sign_receipt_refuses_content_hash_mismatch",
  "public_sign_receipt_accepts_matching_content_hash",
  "verify_scope_intersection_associative",
  "verify_revocation_predicate_idempotent",
  "verify_revocation_admission_projection",
  "verify_delegation_chain_step",
  "verify_receipt_roundtrip",
  "verify_budget_checked_add_no_overflow",
  "verify_budget_admission_projection",
  "verify_reservation_ledger_terminal_classification",
  "verify_reservation_ledger_conservation",
  "verify_composite_quota_all_or_nothing",
  "verify_quota_maximum_immutable",
  "verify_family_binding_preservation",
  "verify_threshold_distinct_signers",
  "verify_delegate_no_widen",
  "verify_delegation_receipt_canonical",
  "verify_revocation_view_freshness",
  "verify_inclusion_step_equivalence",
  "verify_oracle_inclusion_walk_parity",
  "public_delivery_contract_allow_implies_digest_match",
]

[lanes.nightly_only]
description = "Slow Kani harnesses gated to the nightly lane (currently empty; reserved for future slow harnesses)"
harnesses = []

So the local script, the pull-request job (--lane pr) and the nightly job (--lane all) currently run the same set, because lanes.nightly_only is empty. --list counts them:

$ ./scripts/check-kani-public-core.sh --list | wc -l

30

The registry's own lane comment explains the split it is holding open: the concrete-fixture harnesses dominate runtime because public_verify_capability and public_evaluate exercise the full canonical-JSON serialize plus signature verify path, while the algebraic harnesses model signatures with model_sign and model_verify and finish in seconds. Budget for the sweep the way continuous integration does: the job that runs this lane on a pull request is capped at 120 minutes.

./scripts/check-kani-public-core.sh

Creusot and the registered Kani lanes

scripts/check-rust-verification-gates.sh is the aggregate. It first validates the schema and coverage declarations of .kani/harnesses.toml, formal/rust-verification/creusot-contracts.toml, formal/rust-verification/kani-harnesses.toml and formal/rust-verification/kani-public-harnesses.toml, then runs scripts/check-creusot-body-sync.sh. Past that point it refuses to continue without Creusot and Kani on PATH, and runs the Creusot smoke and core proofs, the Kani smoke and core harnesses, the public core lane again, and the non-core pull-request lane from the multi-crate manifest.

Setting CHIO_RUST_VERIFICATION_METADATA_ONLY=1 stops it after the registry checks and prints Rust verification gate metadata passed; strict Creusot/Kani execution explicitly disabled. That is the mode the pull-request job runs, under a job named rust-verification-metadata (schema only, no proofs), so a green pull request on this lane means the registries agree with the source, not that Creusot or Kani ran.

./scripts/check-rust-verification-gates.sh

Adapter no-bypass

The adapter check is cargo xtask check adapter-no-bypass behind a one-line wrapper. It is not a grep. It parses each adapter source with syn, walks the resulting syntax trees, and enforces a table of call contracts: a named function in a named file must call a named target at least a declared number of times. It also flags direct Command::new, .spawn and .invoke uses in adapter code. On success it prints adapter-no-bypass: structured mediation contracts passed.

At the pinned commit it does not reach that line. The source-parsing pass indexes functions by name within a file, and crates/platform/chio-finding-hosted-edge/src/tls.rs defines validate_permissions twice, once behind #[cfg(unix)] and once behind #[cfg(not(unix))]. The index reads that pair as one duplicate identity and stops:

$ ./scripts/check-adapter-no-bypass.sh

xtask: adapter-no-bypass: duplicate function identity in crates/platform/chio-finding-hosted-edge/src/tls.rs: validate_permissions

Differential tests

The differential test crate at formal/diff-tests/ uses proptest to compare a reference specification against the production Rust on generated input pairs. Its integration targets cover canonical JSON in both the native and browser configurations, scope subset relations, treaty predicate evaluation, receipt encoding, anchored Merkle roots and their tamper cases, and one named regression replay.

Filtered to the per-target header and result lines, the whole lane looks like this:

$ cargo test -p chio-formal-diff-tests 2>&1 \
  | grep -E '^( +Running|running |test result)'

     Running unittests src/lib.rs (target/debug/deps/chio_formal_diff_tests-385994c59526858a)
running 13 tests
test result: ok. 13 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s
     Running tests/anchored_root.rs (target/debug/deps/anchored_root-5601d1d4e3da02d8)
running 3 tests
test result: ok. 3 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.08s
     Running tests/anchored_root_tamper.rs (target/debug/deps/anchored_root_tamper-6f994694fa3d9c1e)
running 4 tests
test result: ok. 4 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.06s
     Running tests/browser_canonical_json_diff.rs (target/debug/deps/browser_canonical_json_diff-277c6b64e9ac17a5)
running 3 tests
test result: ok. 3 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 3.95s
     Running tests/canonical_json_diff.rs (target/debug/deps/canonical_json_diff-4f1a913f93ce7313)
running 13 tests
test result: ok. 13 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.14s
     Running tests/receipt_encoding_diff.rs (target/debug/deps/receipt_encoding_diff-469b8481dae73492)
running 7 tests
test result: ok. 5 passed; 0 failed; 2 ignored; 0 measured; 0 filtered out; finished in 0.22s
     Running tests/regression_formal_receipt_before_allow_c01406cfbbeb.rs (target/debug/deps/regression_formal_receipt_before_allow_c01406cfbbeb-5a92b894b99b0cab)
running 2 tests
test result: ok. 2 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.03s
     Running tests/scope_diff.rs (target/debug/deps/scope_diff-b252546adb3163bd)
running 24 tests
test result: ok. 24 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.70s
     Running tests/treaty_predicate_diff.rs (target/debug/deps/treaty_predicate_diff-560f1671fda66a23)
running 4 tests
test result: ok. 4 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 3.19s
running 0 tests
test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s

Two of those targets carry ignored tests rather than failures: receipt_encoding_diff.rs holds a live Python encoder comparison and a live TypeScript one, both opted into with CHIO_LIVE_SDK_DIFFERENTIAL=1 cargo test -- --ignored because they need an installed SDK. The gate passes when every test result: line reads 0 failed.

Portable-kernel parity

This gate is a build check, not a verdict comparison. It redirects CARGO_TARGET_DIR to target/portable-kernel, adds the wasm32-unknown-unknown target, and builds chio-kernel-core twice with --no-default-features: once for the host and once for wasm. What it proves is that the proof-target crate still compiles in the portable configuration the proof boundary is drawn around.

./scripts/check-portable-kernel.sh

Proof report aggregator

scripts/check-proof-report.sh reads target/formal/proof-report.json, calling scripts/generate-proof-report.sh first if that file is absent, and validates it against the chio.proof-report.v1 schema. Run it last: it aggregates what the earlier gates wrote under target/formal/.

./scripts/check-proof-report.sh

Apalache safety shards

The Apalache lane is not in gate_commands. It runs from .github/workflows/apalache-safety.yml, which drives nine spec and config pairs through one wrapper, scripts/check-apalache-positive.sh. The wrapper checks that apalache-mc reports exactly 0.50.1, runs the checker under timeout, and then hands the log to scripts/lib/apalache_evidence.py, which has to agree before the wrapper prints its own passing line.

Each shard names its own invariant, computation length and timeout. Seven run at length 6, the post-admission drop-guard shard at length 8, and the distributed-domains shard at length 0. The .cfg file supplies the constants and the invariant name; the wrapper supplies the length and the wall-clock bound:

./tools/install-apalache.sh

Then run one shard. Filtered to the last six lines, the monotone-log shard looks like this:

$ ./scripts/check-apalache-positive.sh \
    --invariant SafetyInv --length 6 --timeout-seconds 1800 \
    --config formal/apalache/MCMonotoneLogApalache.cfg \
    formal/apalache/MonotoneLogApalache.tla 2>&1 | tail -6

The outcome is: NoError                                           I@03:05:02.031
Checker reports no error up to computation length 6               I@03:05:02.032
It took me 0 days  0 hours  0 min  5 sec                          I@03:05:02.032
Total time: 5.59 sec                                              I@03:05:02.032
EXITCODE: OK
positive Apalache check: invariant SafetyInv passed at length 6

The declared timeouts are the budget rather than the cost. One shard is allowed 600 seconds, six are allowed 1,800, two are allowed 10,800, and the job around them is capped at 360 minutes. What a shard spends is a property of its own bounds and its state space, and the cheapest ones return in seconds.

Run every gate command

There is no single target for all of them, and continuous integration invokes them separately so a failure names a gate. To run the set in one shell, take it from the manifest rather than from this page:

gate_commands = [
  "cargo xtask gen proof-coverage --check",
  "./scripts/check-formal-proofs.sh",
  "./scripts/check-aeneas-pilot.sh",
  "./scripts/check-aeneas-production.sh",
  "./scripts/check-aeneas-equivalence.sh",
  "./scripts/tests/aeneas-equivalence.test.sh",
  "./scripts/check-rust-verification-gates.sh",
  "cargo xtask check formal-mirrors",
  "./scripts/check-kani-public-core.sh",
  "./scripts/run-kani-manifest.sh --lane pr --crate chio-open-market",
  "./scripts/check-adapter-no-bypass.sh",
  "cargo test -p chio-formal-diff-tests",
  "./scripts/check-portable-kernel.sh",
  "./scripts/check-receipt-trace.sh",
  "./scripts/check-distributed-revocation-refinement.sh",
  "./scripts/check-proof-report.sh",
]

Six of those sixteen entries have not appeared above. cargo xtask gen proof-coverage --check and cargo xtask check formal-mirrors compare generated coverage material and mirrored constants against their sources. ./scripts/tests/aeneas-equivalence.test.sh is the regression suite for the equivalence gate itself. ./scripts/run-kani-manifest.sh --lane pr --crate chio-open-market runs the entries of the multi-crate manifest .kani/harnesses.toml for one crate outside chio-kernel-core. And two need Apalache in addition to cargo: ./scripts/check-receipt-trace.sh and ./scripts/check-distributed-revocation-refinement.sh each build a trace from the running implementation and check it against a TLA+ model. The order matters only at the end: check-proof-report.sh reads what the others wrote.

If a gate fails

The documented gates have known failure formats. The Failure Modes page catalogs each one with the literal error format and a triage path. Common cases:

• A sorry scan hit means a Lean proof ships unfinished. The scan in scripts/check-formal-proofs.sh fails the build with formal proof check failed: found literal sorry in shipped Lean modules.
• A Kani VERIFICATION:- FAILED line means CBMC found a counterexample within the unwind bound. See Failure Modes for how to read the counterexample trace and convert it to a regression test with --concrete-playback inplace.
• A diff-test divergence prints both spec and impl values plus the shrunken proptest input. The crate writes regression seeds under formal/diff-tests/proptest-regressions/ automatically.
• A registry disagreement fails before any verifier runs. check-kani-public-core.sh reports it as source and registry harness sets differ with both differences named, and check-formal-proofs.sh fails its manifest and inventory pass.

See also

• P1 Tour: Capability Monotonicity · trace capability attenuation through its proof and test methods.
• Theorem Inventory · the full table of theorems by id, statement, file, claim class, and property mapping.
• Failure Modes · what each gate failure looks like and how to triage.
• Formal Assurance Overview · assurance methods, the proof boundary, and audited assumptions.