Formal Failure Modes

Lean build or fixture failure

The formal proof script runs its stages in order: canonical-JSON fixture drift, the lake requirement, the Lean project build, the placeholder scan, assumption-audit regressions, then the manifest and theorem inventory checks. The first stage that refuses names the evidence that is missing.

When a theorem fails to elaborate, read Lean's source position, local context, and remaining goal. Confirm that the changed definition still has its intended meaning before changing a tactic. A fixture mismatch calls for reviewing the canonicalization change and regenerating the fixture through its source generator.

A missing lake executable is a toolchain failure and carries no evidence about any theorem. Install the project's pinned Lean toolchain as Qualification: formal gates describes, then rerun the gate.

Assumption environment change

The script compares the elaborated axiom and opaque declarations with its allowlists, and checks approved assumption identifiers against the theorem inventory and the claim registry. A new declaration changes what the proof trusts even when the project still builds.

Approved axiom

The manifest names Chio.Json.hash_collision_resistant as its one allowed explicit Lean axiom. The external assumption registry is a separate record that names contracts such as the deployment clock, SQLite, and transport. Keep the two inventories apart; neither one is a complete deployment trusted computing base.

Axiom mismatch diagnostic

The check fails with Lean environment axiom mismatch and lists the missing and extra declarations:

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}"

Compare each named declaration with the source diff and the approved manifest. An unexpected axiom, opaque, export, or alias needs investigation, and expanding an allowlist is a change to the proof boundary. Assumptions & TCB explains the contracts that stay external.

Surviving placeholder

A separate scan rejects a literal sorry in shipped Lean modules, because a successful build leaves the unfinished proof that placeholder represents undischarged. The script reports formal proof check failed: found literal sorry in shipped Lean modules.

"${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

Finish the proof, or remove the unfinished claim from the shipped modules through a reviewed scope change. The scan stays in the gate.

Inventory sanity checks look for a matching theorem or lemma declaration in each named file. The general theorem check reads rootImported as a registry flag and leaves the import graph of each theorem unresolved. Axiom and opaque checks read elaborated-environment evidence.

Aeneas extraction or authentication failure

Production extraction processes the Rust sources registered in formal/aeneas/production.toml, which include kernel decisions and economy conversion logic. Charon produces LLBC, Aeneas generates Lean function and type files, and the script checks the registered function and type inventory.

A change that adds an unsupported operation to an extracted source needs a deliberate boundary decision. Moving the effect into a caller keeps the source extractable only while the caller's behavior and the implementation link stay accounted for.

Generated Lean and committed evidence mismatch

The equivalence script checks source stamps, generated snapshots, registered functions and theorem declarations, toolchain identities, and the generated module's root import. When required outputs are absent or stale, it runs production extraction first. These bookkeeping and identity checks are separate from Lean elaborating the equivalence proofs.

Generated snapshot drift

The snapshot script names the regenerated file and the committed snapshot it differs from:

    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

Review whether the Rust semantics, the extraction toolchain, or the generated support changed; the production script can stop at this drift. After inspecting it, update the snapshots, then rerun extraction and the Lean proof gate.

The snapshot update covers the kernel snapshot unless told otherwise. A reviewed economy-source change selects its generated directory and the committed FormalEconomy snapshot explicitly, then reruns the extraction and Lean gates.

Function-to-theorem mapping

Every extracted function needs its registered equivalence theorem. The refusals are Aeneas theorem count mismatch, Generated equivalence theorem missing, and Generated equivalence axiom-report coverage mismatch. Restore the mapping and elaborate the resulting proof; a declaration name copied into the registry satisfies neither.

Kani assertion violation

A failing Kani check reports the assertion, its source location, and a counterexample. Three explanations fit: the implementation violates the intended property, the assertion states the wrong property, or the harness admits an input outside its justified domain.

Keep the counterexample as a regression case, with the input assumptions that produced it. The public runner validates the harness inventory against source and runs the registered PR lane. Kani Harnesses identifies the exact harness, so a smaller test with a similar name never substitutes for it.

Kani timeout or unwinding failure

The public runner uses default unwind 8. It omits unwinding assertions for harnesses outside the registry's unwinding_checks list, and the published list retains them for verify_oracle_inclusion_walk_parity. Read every result with that policy and the harness's loop bounds.

A timeout is incomplete verification. An unwinding assertion says the selected bound left part of the loop behavior unexplored. Preserve the original command, then inspect the changed loop, the symbolic input space, and the solver resources. Removing an unwinding check or adding kani::assume can hide the failing behavior.

Constrain an input only when the production precondition and the intended property justify the restriction. When a bound or lane changes, record which obligation the new run establishes and which remains open; a quicker passing run leaves the original obligation open.

Apalache model or evidence rejection

The positive wrapper checks the requested invariant or temporal property, configuration, computation length, and timeout, and requires the pinned Apalache version. It validates the output beyond the process exit: exactly one NoError outcome, the expected property, the exact requested length, and no violation trace.

SafetyInv is defined separately by each specification. Inspect the formula in the selected spec and the bounds in its config; the shared name says nothing about whether two shards checked the same property.

• Counterexample. Preserve the numbered ITF trace and find the action that reaches the violating state.
• positive Apalache check: evidence validation failed. Read the preceding diagnostic: a malformed log, a wrong property, a shortened run, or a timeout each refuse qualification.

Set CHIO_APALACHE_POSITIVE_OUTPUT_DIR before running the registered command to retain its work directory.

Compare model and implementation assumptions when reading the trace. Cross-references in formal/MAPPING.md help navigation, and an informal link between a TLA+ invariant and a Lean theorem is a pointer between two results rather than a checked equivalence.

Model deadlock

A deadlock means no modeled transition is enabled. Inspect the terminal state and the guards on the model's Next actions, then decide whether the state should be terminal, should permit a stuttering step, or exposes a missing progress transition. Use the lane's registered deadlock setting: the wrapper accepts --no-deadlock, and adding it changes the check being performed.

A model deadlock maps to a production outage only through the corresponding implementation link. A bounded model that avoids deadlock establishes progress within its bounds, and unbounded progress in a deployed network needs its own evidence. Retain the fairness, timing, and partition assumptions.

Differential divergence

The differential tests compare an independently written executable specification with production behavior on the same generated input. Inspect the shrunk counterexample and both results: either side, or the generator's mapping between them, can be wrong.

Preserve the regression seed and the minimal input before editing the test. Check the intended semantics for the exact operation, fix the responsible side, and rerun the case. A source enum change can require both generator and specification updates, and compilation may catch it before any behavioral mismatch surfaces.

Timing threshold crossing

The threshold check reads the maximum absolute max t value from the captured output. At the default threshold 4.5, values at or above the threshold fail and values below it pass; missing or unparsable measurement input is an error. The workflow reports these as PASS, FAIL, and ERROR, and chio security selftest timing reports the same three outcomes for a run on your own host.

The advisory lane records each measurement and correlates two consecutive FAIL results for the same harness before filing its sustained-signal issue. A single threshold crossing is still evidence to inspect. A passing run means the experiment stayed under its threshold on that machine; repeated failures establish neither exploitability nor a cause.

Keep the raw checkpoints, input classes, sample counts, binary, and machine conditions. Reproduce on a controlled machine and inspect the affected branch or comparison. Changing the threshold or dropping a noisy run changes the evidence. Constant-Time Tests lists the other registered harnesses.

Fuzz crash or sanitizer failure

Save the input artifact and the failing stack before another run changes the output directory. Identify the target and its owning crate, replay the input against that target, then minimize it.

tmin minimizes one input; cmin minimizes a corpus. Once the failure is understood, the seed-promotion script preserves the minimized bytes and generates a regression test in the owning target. Review the test and its expected behavior. Fuzz Infrastructure documents ownership and promotion modes.

Proof gate not run

The manifest's gate_commands list defines the expected report commands. The generator excludes its own command and the report checker's from gateResults, and the coverage preflight is registered exactly once and runs first. Compare the report with that list and with the workflow invocation.

Report mode and gate status

The checker validates structure and source binding; it does not replay proof commands in an existing report. Passing --require-strict rejects metadata_only. An absent report invokes the generator, so a first checker call can require the full proof toolchain.

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

The command-order check detects disagreement with the manifest. Whether a hosted workflow invoked the generator, and on which revision a CI job ran, comes from the job logs. Keep the report, the job logs, and the source identity together.

Cancellation model results

Two models cover cancellation, at different scopes. Identify which model and which lifecycle phase applies before expecting a refund or a clean rollback.

KernelTransitionCancelSafe

Clean cancellation preserves the pre-transition budget and receipt snapshot. The model prevents commit while cancellation is pending and has no Rust reversal action, so concurrent commit-versus-cancel restoration is outside it.

PostAdmissionDropGuard

A broader lifecycle distinguishes pre-dispatch cleanup, post-dispatch outcomes, and retained reservations. The manifest scopes it to two invocations and one buffered child per invocation, with positive and paired negative evidence. Persistence and cleanup in the running kernel need their own implementation evidence.

A model's abstraction anchors identify the related Rust code; showing that the Rust reversal path restores state takes implementation evidence. Formal Assurance explains the production boundary.

Reproducible failure package

Keep the source revision and local diff, the exact command, the toolchain identity, the full log, the exit status, the configuration, and the counterexample or generated artifact. Start with the failed gate. After repairing it, rerun the evidence the original claim needs, including the strict report when release qualification depends on it.

Generating a strict report executes substantial verification work. Qualification: formal gates lists each gate's source entry point, prerequisites, and pins. For a report you already have, inspect its mode before choosing whether to validate its structure or reproduce its gates.