Failure modes

Lean 4 build failure

scripts/check-formal-proofs.sh runs five stages in order, each announced with a ==> banner: a canonical-JSON fixture drift check, the Lean build, a placeholder scan, the elaborated assumption audit, and a manifest-plus-inventory sanity pass. It refuses to start at all without lake on PATH, printing formal proof check requires lake on PATH (install Lean 4 / elan first). The build itself is a plain lake build run inside formal/lean4/Chio, so a build failure is Lean's own diagnostic naming the module and position.

Common triggers:

• Tactic typo or rename. A Mathlib lemma name changed under a toolchain bump and the old name no longer resolves. The toolchain pin is leanprover/lean4:v4.28.0 in formal/lean4/Chio/lean-toolchain and the Mathlib revision comes from formal/lean4/Chio/lake-manifest.json. The Aeneas equivalence gate cross-checks both: it fails with Aeneas vendor host toolchain mismatch when the vendored support declares a different host toolchain, and with Lake manifest does not bind the vendored Aeneas Mathlib revision when the manifest and the vendor manifest disagree on Mathlib.
• Unapproved surface control. The sanity pass parses every project Lean file for open, export and abbrev. An open outside allowed_open_modules fails with unexpected Lean open modules found and the file and line; any export at all fails with unexpected Lean export declarations found; an abbrev whose name shadows an approved axiom fails with Lean abbrevs shadow approved axioms.
• Axiom shift. A new axiom entered the elaborated environment. See below.

An axiom entered the environment

The manifest's allowed_axioms has exactly one entry, and the manifest's own comment says what it is: the Lean idealization registered as ASSUME-SHA256.

allowed_axioms = [
  # Symbolic collision resistance over the image of the mechanized canonical
  # UTF-8 renderer. This is the Lean idealization registered as ASSUME-SHA256.
  "Chio.Json.hash_collision_resistant",
]

Two independent checks defend that list, and they fail with different messages. The first compares the manifest against the theorem inventory's assumptions array and fails with approved axiom list does not match theorem inventory assumptions. The second runs scripts/lean-assumption-audit.lean under lake env lean --run over the elaborated environment and compares the axioms Lean actually reports against the same list.

if set(environment_axioms) != set(approved_axioms):
    missing = sorted(set(approved_axioms) - set(environment_axioms))
    extra = sorted(set(environment_axioms) - set(approved_axioms))
    raise SystemExit(
        f"Lean environment axiom mismatch; missing={missing} extra={extra}"

The audit also collects opaque declarations and compares them against a hard-coded set of nine compiler-generated deriving Repr helpers in Chio.Json.Value, failing with Lean environment opaque mismatch. That is why an added deriving clause can fail this gate without anyone writing an axiom.

Triage: run #print axioms <name> on the suspect theorem to see what it depends on. If the new axiom is intended, it needs a matching assumptions entry in formal/theorem-inventory.json with kind axiom and rootImported true, because the sanity pass rejects an assumption that lacks either with assumption is not marked as axiom or assumption not marked rootImported.

Lean 4 theorem unproved

A literal sorry in any shipped Lean module fails the gate independently of the build. The scan is ripgrep when available and grep -RInw otherwise, over formal/lean4/Chio/Chio and formal/lean4/Chio/Chio.lean. A match is exit 0 from the scan, which the gate treats as its own failure; any exit other than 0 or 1 is treated as the scan itself breaking.

"${placeholder_scan[@]}" && placeholder_rc=0 || placeholder_rc=$?
if [[ "${placeholder_rc}" -eq 0 ]]; then
  echo "formal proof check failed: found literal sorry in shipped Lean modules" >&2
  exit 1
elif [[ "${placeholder_rc}" -ne 1 ]]; then
  echo "formal proof placeholder scan failed with exit ${placeholder_rc}" >&2
  exit 1
fi

The build can still succeed with a sorry because Lean elaborates it as an unsafe witness, which is exactly why the scan exists as a separate stage. Common triggers are a draft proof landing before the body was finished, or a placeholder left behind while iterating on a tactic chain.

Aeneas extraction failure

scripts/check-aeneas-production.sh drives Charon and then Aeneas over the sources registered in formal/aeneas/production.toml. There are two of them, not one: crates/kernel/chio-kernel-core/src/formal_aeneas.rs into target/formal/aeneas-production/lean/ and crates/economy/chio-credit/src/formal_economy.rs into target/formal/aeneas-production/economy/lean/. Each run announces itself with ==> Charon extraction for <source-id> and ==> Aeneas Lean extraction for <source-id>.

The two failures the script raises itself are about missing outputs rather than about Charon's own diagnostic: Aeneas production check failed: Charon did not produce <llbc-file> when the LLBC step emits nothing, and Aeneas production check failed: output missing for <source-id> when either Funs.lean or Types.lean is absent afterwards. Charon's unsupported-item message, when there is one, precedes those lines in the captured output.

Before any of that runs, the script requires an authenticated toolchain: it refuses with Authenticated Aeneas toolchain missing: <path> and directs the reader to ./scripts/install-aeneas-toolchain.py, and with Authenticated Aeneas install receipt missing when the receipt is gone. It also refuses an unsupported host architecture outright.

Common triggers:

• A new branch added dyn dispatch, async, IO, or string formatting inside one of the two registered sources. Both files are the pure numeric and boolean core; anything beyond that has to live in a sibling module.
• A struct in the same file gained a non-extractable field type such as Box<dyn Trait>.
• The Charon or Aeneas pin moved. The equivalence gate checks the pin from three directions at once and fails with Aeneas release tag mismatch when the two workflows' CHIO_AENEAS_RELEASE_TAG, the registry's vendor_release_tag, and the vendor manifest's release_tag are not all one value.

Aeneas equivalence gate failure

scripts/check-aeneas-equivalence.sh does not elaborate Lean. It first checks that the production outputs exist and that each source's committed source.sha256 stamp still matches the file; if any of that is missing it delegates to scripts/check-aeneas-production.sh and exits. Then it compares the regenerated Lean against the committed snapshots under formal/lean4/Chio/FormalAeneas and formal/lean4/Chio/FormalEconomy. A divergence is the single most common failure here, and it names both paths and the exact recovery:

    echo "aeneas-equivalence: GENERATED SNAPSHOT DRIFT" >&2
    echo "  regenerated ${generated_dir}/${file} differs from" >&2
    echo "  committed ${snapshot_dir}/${file}" >&2
    drift=1
  fi
done

if [[ "${drift}" -ne 0 ]]; then
  echo "  Re-run: ./scripts/check-aeneas-production.sh" >&2
  echo "  then: ./scripts/snapshot-aeneas-generated.sh" >&2
  echo "  Commit the snapshot diff after reviewing the generated semantics." >&2
  exit 1

The rest of the gate is registry bookkeeping over formal/aeneas/production.toml and the generated module it names, formal/lean4/Chio/Chio/Proofs/AeneasGeneratedEquivalence.lean. Every declared target has to carry status = "generated_equivalence", one equivalence theorem row per registered function, and a theorem name that resolves to a declaration in the generated module.

targets = registry.get("targets", [])
registered_theorems = {}
registered_functions = []
for target in targets:
    if target.get("status") != "generated_equivalence":
        raise SystemExit(f"Aeneas target is not equivalence-checked: {target.get('name')}")
    functions = target.get("functions", [])
    theorem_rows = target.get("equivalence_theorems", [])
    if len(functions) != len(theorem_rows):
        raise SystemExit(f"Aeneas theorem count mismatch for {target.get('name')}")
    for row in theorem_rows:
        symbol, separator, theorem = row.partition("|")
        if not separator or symbol in registered_theorems:
            raise SystemExit(f"Malformed or duplicate generated equivalence theorem row: {row}")
        short_name = theorem.rsplit(".", maxsplit=1)[-1]
        if short_name not in declared_proofs:
            raise SystemExit(f"Generated equivalence theorem missing for {symbol}: {theorem}")
        registered_theorems[symbol] = theorem
    registered_functions.extend(functions)
if set(registered_functions) != set(registered_theorems):
    raise SystemExit("Aeneas generated equivalence theorem inventory is incomplete")

Adding an extracted symbol without its theorem therefore fails at Aeneas theorem count mismatch for <target> or Generated equivalence theorem missing for <symbol>, not at a Lean type error. Four further refusals in the same script are worth knowing because none of them is a proof failure either: Aeneas equivalence must not depend on handwritten externals when the registry grows an external_models key; Generated equivalence module contains a placeholder proof for a sorry; Generated equivalence axiom-report coverage mismatch when a declared theorem lacks its #print axioms line; and Generated Aeneas equivalence module is absent from proof manifest roots when the module leaves root_modules.

Triage path:

• Read the drift block. It names the regenerated file and the committed file, so the diff between them is the whole question.
• Regenerate with ./scripts/check-aeneas-production.sh, then ./scripts/snapshot-aeneas-generated.sh, then read the snapshot diff before committing it. The script says so in its own output, and the reason is that the diff is a change in generated semantics rather than formatting.
• Check target/formal/aeneas-production/equivalence-artifacts.json to see whether the Rust source hash moved. If it did not, the change is on the Lean or toolchain side.

Kani assertion violation

scripts/check-kani-public-core.sh reads the harness list out of formal/rust-verification/kani-public-harnesses.toml with an inline tomllib block, filters by --lane, and runs one cargo kani invocation per harness against -p chio-kernel-core --lib with --default-unwind 8. It adds --no-unwinding-checks for every harness except the ones the manifest lists in unwinding_checks. A clean sweep ends with Kani public core harnesses passed (<N> harnesses, lane <lane>).

A harness that finds a counterexample fails inside Kani rather than inside the script: Kani prints VERIFICATION:- FAILED with the failing check, the source position, and a CBMC trace assigning a concrete value to every kani::any input and assigned variable at the failure point. One failing check flips the whole harness, and the script propagates the non-zero exit because it runs under set -euo pipefail.

Common triggers:

• Implementation regression. A change to the code the harness calls flipped a comparison axis, and the harness's symbolic state space reaches the new bug.
• Spec regression. The assertions encode the wrong invariant. The implementation is fine but the harness asserts something the code is not supposed to satisfy.
• Harness bug. The kani::assume predicates are too weak and admit an input the production path would never see.

Triage path:

• Reproduce as a regular Rust test: cargo kani -p chio-kernel-core --lib --harness <name> --concrete-playback inplace. Kani writes the counterexample as a #[test] next to the harness so it can be stepped through under a debugger.
• Classify against the three triggers above, then file with formal/issue-templates/property-counterexample.md.
• Fix the underlying issue and pin the counterexample as a regression test, so the shape stays rejected even if the symbolic search misses it next time.

Kani timeout or unwind exceeded

Every harness runs at a fixed unwind depth of 8. Exceeding it surfaces as an unwinding assertion when the harness is one of the manifest's unwinding_checks entries, and as an unsound truncation otherwise, which is why that list is short and explicit rather than a default.

Common triggers:

• A new branch widened a symbolic input without a matching kani::assume bound, and the state space grew accordingly.
• A loop bound rose above 8. The harness convention is to construct inputs so loops bound at one or two iterations regardless, so a violation usually means the harness needs a structural pin on its input.
• The runner is slower than the sizing assumption. The lane note in formal/rust-verification/kani-public-harnesses.toml records the full sweep at roughly 2.2 minutes locally against a 10-minute warm pull-request target, and says the concrete-fixture harnesses dominate that time because they exercise the full canonical-JSON serialise plus Ed25519 and P-384 verify path while the algebraic harnesses model signatures and finish in one to three seconds.

Triage path:

• Run the failing harness alone: cargo kani -p chio-kernel-core --lib --harness <name> --default-unwind 8 --no-unwinding-checks.
• Add kani::assume predicates to constrain the new symbolic axes.
• The manifest carries a second lane for a harness whose shape is structurally slow. The nightly job runs the union of lanes.pr and lanes.nightly_only while the pull-request workflow runs only lanes.pr; every harness currently sits in the first.

Apalache invariant violation

The safety lane runs one scripts/check-apalache-positive.sh invocation per matrix shard, each with its own spec, config, invariant name, computation length and timeout. Seven shards pass --invariant SafetyInv, which is a per-spec name rather than one formula: each spec defines its own SafetyInv as the conjunction of that spec's own leaves. The one in formal/tla/RevocationPropagation.tla has six conjuncts.

SafetyInv ==
    /\ DomainsOK
    /\ NoAllowAfterRevoke
    /\ MonotoneLog
    /\ AttenuationPreserving
    /\ RevocationFreshness
    /\ RevocationStateCoupled

The script refuses before running for reasons that are not model failures at all, and each has its own exit code 2: positive Apalache check: length must be non-negative and timeout must be positive, positive Apalache check: config and specification must be files, positive Apalache check: executable not found, and a version pin, positive Apalache check: Apalache 0.50.1 is required. A run that gets past those is wrapped in timeout at the shard's timeout_seconds, its full log is printed, and the log is then handed to scripts/lib/apalache_evidence.py.

That evidence step is where a violation is actually detected, and it is stricter than a non-zero exit. It parses the log for exactly one The outcome is: Error | NoError | ExecutionsTooShort line and requires NoError. It requires the log to configure exactly the invariant the shard asked for, via > Set an invariant to <Name>, so a spec that quietly checks something else fails with expected exactly invariant <Name>, found [...]. It requires a Checker reports no error up to computation length N line whose N equals the requested length exactly, so a run that stopped short fails with NoError outcome lacks the exact requested computation length. And it requires that no violation* trace file exists anywhere under the run directory. Any of those failing prints positive Apalache check: evidence validation failed and exits 1. A clean shard prints positive Apalache check: <mode> <property> passed at length <N>.

A real violation is an Error outcome accompanied by exactly one Checker has found an error report and one State N: state invariant M violated. summary, plus one non-empty numbered violation<N>.itf.json trace. That ITF file, not a .tla counterexample, is the artifact to read: it holds the state sequence from Init through the Next steps that reach the violation. Set CHIO_APALACHE_POSITIVE_OUTPUT_DIR before the run to keep the work directory instead of having it cleaned up on exit.

Common triggers:

• A change to the spec made an action fire under conditions the invariant did not anticipate.
• The model bounds in the shard's config widened and a previously unreachable state became reachable. Each shard names its own config, so the bounds are per shard rather than shared.

Triage path:

• Read the ITF trace and identify the action that drove the violating step.
• Compare against the Lean cross-reference. formal/MAPPING.md records these as informational and says the script does not enforce them: NoAllowAfterRevoke corresponds to Chio.Proofs.evalToolCall_revoked_token_never_allows and Chio.Proofs.evalToolCall_revoked_ancestor_never_allows in formal/lean4/Chio/Chio/Proofs/Evaluation.lean. A divergence between the abstract invariant and the Lean theorem means one of them is wrong; it does not by itself say which.
• File with formal/issue-templates/property-counterexample.md, or formal/issue-templates/liveness-counterexample.md for a temporal property.

Apalache deadlock

A deadlock is a state where no Next action is enabled. Apalache reports it as an error outcome, so it reaches the same evidence path as an invariant violation and produces the same evidence validation failed refusal. The deadlock check can be turned off per invocation with --no-deadlock, which scripts/check-apalache-positive.sh accepts and forwards. The temporal lanes pass it; the safety matrix does not, so the safety shards are checking for deadlock as well as for their invariant.

For formal/tla/RevocationPropagation.tla a deadlock should not arise: every authority can take a stuttering step and PropagateAny is guarded only by pending being non-empty. A deadlock report there usually means the spec gained a guard that conflicts with the action contract, so check recent edits to Attenuate, Revoke and Evaluate, and confirm [][Next]_vars is intact in Spec.

Diff test divergence

formal/diff-tests/ runs an executable reference specification against the shipped Rust on generated input pairs. The spec at formal/diff-tests/src/spec.rs states its own purpose: it reimplements the shipped subset logic without calling into chio_core, so a divergence is detectable at all. Each property compares a spec-side result with an impl-side result over the same generated value and prints both when they disagree.

fn scope_subset_spec_matches_impl(
    ((spec_a, impl_a), (spec_b, impl_b)) in arb_paired_scope_pair()
) {
    let spec_result = spec_a.is_subset_of(&spec_b);
    let impl_result = impl_a.is_subset_of(&impl_b);

    prop_assert_eq!(
        spec_result, impl_result,
        "Scope subset mismatch!\n  spec: {}\n  impl: {}\n  child grants: {}\n  parent grants: {}",
        spec_result, impl_result, spec_a.grants.len(), spec_b.grants.len()
    );
}

proptest shrinks toward the smallest input that still diverges and persists the seed. In this crate the persistence file sits beside the test rather than in a directory: formal/diff-tests/tests/canonical_json_diff.proptest-regressions is the committed one, and a new failure writes the same shape for its own test file. The case count is 256 by default and is overridable through the PROPTEST_CASES environment variable.

Common triggers:

• The reference spec drifted from the production Rust. Either the spec is wrong, which is rarer because it is written to be read, or the implementation is.
• A new variant was added to SpecConstraint or to the production Constraint enum without a matching update on the other side. The generators in formal/diff-tests/src/generators.rs build both halves of each pair, so a one-sided addition shows up as a mismatch rather than as a compile error.

Triage path:

• Read the minimal failing input. After shrinking it is usually one or two grants.
• Run the spec and the implementation on that input by hand; one of them is wrong.
• Fix the offending side and commit the persisted seed alongside the fix so later runs replay the exact case first.

dudect timing leak

The dudect lane measures three harnesses. mac_eq and scope_subset live in crates/kernel/chio-kernel-core/tests/dudect/ and run as the dudect_mac_eq and dudect_scope_subset test binaries; jwt_verify lives in crates/trust/chio-credentials/tests/dudect/ and runs as dudect_jwt_verify. scripts/check-dudect-threshold.sh reads the captured stdout, takes the maximum absolute max t across every checkpoint line, and compares it against 4.5.

Its output is a single verdict line, not a leak banner: dudect verdict: max|t|=<value> threshold=<T> result=<PASS|FAIL>. The comparison is at or above, so exactly 4.5 is a FAIL. Exit 0 is a pass, exit 1 is over threshold, and exit 2 is a precondition failure such as an unreadable file or one with no max t lines at all. The workflow records those three as the literal strings PASS, FAIL and ERROR, so a parse failure is neither a pass nor an alarm.

A single FAIL does nothing. Every job in .github/workflows/dudect.yml carries continue-on-error: true, and the workflow header states the posture: the lane is advisory and the GitHub issue is the signal. The correlate job compares the current verdict against the most recent prior completed run and, only when both read FAIL for the same harness, opens or comments on an issue titled dudect: sustained timing leak in <harness> (t >= 4.5 in 2 consecutive runs) with the label timing-leak. Otherwise it prints no sustained leaks (two-consecutive-run rule); nothing to file.

Common triggers:

• A change to the byte-equality compare path introduced a short-circuit. mac_eq drives two classes of signature pair, differing at byte 0 and at byte 63, so a constant-time compare produces statistically identical timing and a short-circuiting one does not.
• A change to the scope-subset walk started branching on attacker-visible values. scope_subset places the matching parent grant first and last in a 16-wide fan-out, and both classes resolve to the same verdict.
• A change to the JWT VC verify fail path started branching on input contents. jwt_verify pushes an all-zero compact string and a random ASCII string of the same length through chio_credentials::verify_chio_passport_jwt_vc_json; both fail closed, so a distinguishable distribution means the rejection path leaks why a candidate was rejected.
• A noisy runner. dudect is a statistical detector and a single-run reading on a shared runner is commonly noise, which is exactly what the two-consecutive-run rule exists to filter.

Triage path:

• Reproduce one harness at a time on a quiesced machine: cargo test -p chio-kernel-core --features dudect --release mac_eq or cargo test -p chio-credentials --features dudect --release jwt_verify.
• Compare the two runs the issue links. Each artifact keeps the raw <harness>.out for 30 days, so both checkpoint sequences are available. A leak commonly grows with the sample count; noise does not.
• If the signal persists on a quiet machine, inspect the compare path. The conventional fix for byte equality is subtle::ConstantTimeEq; for higher-level branching it is lifting the data-dependent branch out of the timing-sensitive path.
• See Constant-Time Tests for the harness layout and the threshold rationale.

Fuzz crash

The libFuzzer targets in fuzz/fuzz_targets/ run under three workflows. On a crash libFuzzer writes the input under the artifact prefix and prints a sanitizer report naming the frame that faulted; the crash files upload as cflite-pr-crashes-<PR> on the pull-request lane and cflite-batch-<target>-<run-id> on the nightly rotation.

Common triggers:

• A trust-boundary parser panicked on an adversarial input. The fuzz workspace denies unwrap_used and expect_used, and its own comment says why: targets must consume Result values with if let Ok(_) or match so a panic is reported as a bug rather than masked.
• An AddressSanitizer report on a memory-safety fault. Both CFLite lanes pass sanitizer: address.

Triage path:

• Reproduce by replaying the single input: cargo +nightly fuzz run <target> fuzz/artifacts/<target>/crash-<id>.
• Minimize with cargo +nightly fuzz tmin <target> <crash-file>, which shrinks one input. cmin minimizes a whole corpus and is a different operation.
• Resolve the owning crate through fuzz/owners.toml and file against that owner.
• Promote the minimized seed with scripts/promote_fuzz_seed.sh --target <name> --input <path> --mode libfuzzer. The script moves the seed to fuzz/corpus/<target>/<sha>.bin and writes a regression test under the owning crate, so the case keeps running as a normal cargo test. See Fuzz Infrastructure for the other two modes.

A gate did not run

formal/proof-manifest.toml names the gate commands a release claim rests on. There are sixteen of them, and they are the list, not a summary of it.

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",
]

scripts/check-proof-report.sh is the aggregator. It reads target/formal/proof-report.json (overridable with CHIO_PROOF_REPORT_PATH) and, when the file is absent, runs ./scripts/generate-proof-report.sh to produce one rather than failing. What it is checking is stated in the report itself, as a string the checker requires the report to carry verbatim:

EVIDENCE_BOUNDARY = (
    "gate statuses attest the trusted generator process; this checker validates "
    "structure and source binding but does not replay proof commands"
)

Read that literally. The aggregator validates structure and source binding. It does not re-run the gates, so a green report is a statement about a generator run, not a reproduction of the proofs.

Within that boundary the checks are exact. gateResults must match the manifest's command list in order, with no duplicates, after removing the aggregator's own commands and the generator commands. The coverage preflight cargo xtask gen proof-coverage --check must be registered exactly once and must be the first report gate command. And the required status per gate depends on the report's mode:

if actual_commands != expected_commands or len(actual_commands) != len(set(actual_commands)):
    fail("gateResults do not match the exact unique manifest command order")
if mode == "strict":
    for result in gate_results:
        if result["status"] != "passed":
            fail(f"strict gate did not pass: {result['command']} status={result['status']}")
else:
    for result in gate_results:
        expected_status = "passed" if result["command"] == COVERAGE_COMMAND else "not_run"
        if result["status"] != expected_status:
            fail(
                f"metadata-only gate status mismatch: {result['command']} "
                f"status={result['status']}"
            )
    print("WARNING: proof report is metadata-only; only coverage preflight was executed")

So there are two shapes a report may legitimately have. strict requires every gate to be passed. metadata_only requires every gate other than the coverage preflight to be not_run and prints WARNING: proof report is metadata-only; only coverage preflight was executed. A metadata-only report is a valid report and a not_run gate is not a drift failure inside it. The lever that forbids one is --require-strict, which refuses a non-strict mode with a named reason: that the risk register's formal-verification claim rules require a strict proof report for release qualification.

How to detect and where to look:

• Run the aggregator locally with ./scripts/check-proof-report.sh. It names the first mismatch, and --require-strict is what turns a metadata-only report into a failure.
• A manifest command with no matching workflow invocation surfaces as the ordering mismatch rather than as a missing file, because the generator emits one gateResults row per manifest command.
• The claim gate is checked separately and refuses a claimGate.status other than passed, an inputs list that differs from claim_gate_inputs, and a required-terms list that is not the canonical six.

Drop and cancel-unwind

Two Apalache specs cover this path and they scope themselves differently. formal/apalache/KernelTransitionCancelSafe.tla models a cancelled in-flight kernel transition, and its own header records the modeling bound in its own words: Commit is guarded by cancel_pending = FALSE, so no action mutates budget_used or receipt_count while a cancel is pending and the invariant holds by construction. The same header says the model does not exercise the Rust reversal transition or concurrent commit-versus-cancel races, and that the abstraction anchors identify the runtime handoff without proving restoration.

The header then points at the broader model, and so does the manifest. formal/apalache/PostAdmissionDropGuard.tla carries the pre-dispatch and post-dispatch lifecycle, runs as its own safety shard at computation length 8, and defines its own SafetyInv over ReservationConservation, TerminalReceiptExactlyOne, ChildReceiptsFlushed and RetainedIffAborted alongside DomainsOK. The manifest note scopes it precisely: the post-admission drop lifecycle is model-checked at two invocations and one buffered child per invocation, and its evidence requires both a positive result and every paired negative mutation producing a registered ITF counterexample.

Reproduce

The cheapest whole-posture check is the aggregator, because it validates the report's structure and source binding without a proof toolchain. It generates a report first if none exists, so the first run is slower than later ones.

./scripts/check-proof-report.sh

Add --require-strict to refuse a metadata-only report. To exercise one gate on its own, run the command the manifest names for it; the Lean gate needs lake on PATH and the Apalache shards need Apalache 0.50.1.

./scripts/check-formal-proofs.sh
./scripts/check-kani-public-core.sh --lane pr
cargo test -p chio-formal-diff-tests

Keeping gates aligned

Three registries define the expected inventory: formal/proof-manifest.toml for the gates, the covered surfaces and the allowed axioms, formal/theorem-inventory.json for the theorems and their property mapping, and formal/assumptions.toml for the 15 audited assumptions each result rests on. Several of the failures above are the gates catching those three disagreeing with each other rather than a proof breaking, and the fix is to move the registry and the code in one change.

• Formal Quickstart · running the gates from a fresh clone.
• Lean 4 Proofs · the proof structure and the build flow.
• Aeneas Pipeline · the extraction pipeline and the equivalence theorems.
• Kani Harnesses · the public harness inventory and the unwind bound.
• TLA+ Specs · the cross-authority protocol model and the named invariants.
• Differential Tests · the proptest generators and the spec/impl comparison.
• Constant-Time Tests · the dudect harnesses, the verdict script, and the two-consecutive-run rule.
• Fuzz Infrastructure · the libFuzzer trust-boundary harness inventory.