The proof ladder

Consumer-facing reference for proofStatus, proofStages, proofGaps, and proofAdvisories as reported by kibi coverage --by req and kb_coverage. The authoritative implementation is packages/core/src/requirement_proof.pl (proof version kibi.requirement-proof.v3); this document explains what each stage means and what to do when it does not pass.

Applicability: is the requirement in scope at all?

The ladder only evaluates current requirements. A requirement is current when its status is one of:

• Canonical: open, in_progress, closed
• Legacy (accepted for backwards compatibility): active, approved

Everything else is out of scope by design. Two things can take a requirement out of scope:

1. Supersession — a newer requirement links to it with supersedes.
2. Status outside the vocabulary — e.g. the ADR vocabulary accepted. Since that silently excludes the requirement from proof, kibi check reports it as a blocking req-status-vocabulary violation instead of letting it hide.

Out-of-scope requirements report:

{
  "proofStatus": "not_applicable",
  "proofGaps": [],
  "proofStages": {
    "applicability": {
      "status": "not_applicable",
      "reason": "status 'accepted' is not a current requirement status"
    }
  }
}

The typed reason is what not_applicable used to hide: superseded requirements say so; status-vocabulary mismatches name the offending status.

Proof exemption: current but intentionally not E2E-provable

Some current requirements cannot be proven by end-to-end evidence — toolchain-currency gates, architectural boundaries, quality-gate policy. Parking them with an ADR status is exactly the trap above. Instead, mark them explicitly in the requirement document:

---
id: REQ-TOOLCHAIN-001
status: open
priority: must
proof_exempt: true
proof_exempt_reason: architectural boundary — verified by toolchain CI, not product E2E
---

proof_exempt requires a non-empty proof_exempt_reason (upsert validation enforces the pairing, and the ladder ignores an exemption without a reason). Exempt requirements report not_applicable with the author's reason attached, so coverage can distinguish "cannot be proven" from "not proven yet".

To re-enter the proof ladder, remove both properties.

The stages

For in-scope requirements the ladder evaluates nine stages, each reporting status (and, for productionSymbols, a typed reason when it does not pass):

Stage statuses, precisely

• passed — the stage's obligations hold.
• missing — the evidence is absent. The stage names what is missing (missingTests, missingReceiptTests, uncoveredSymbols, missingSymbols, ...), and proofGaps carries the blocking gap code.
• blocked — the stage cannot be evaluated because an upstream input is unavailable. Only two stages use it:
  • contradictions: logical grounding is incomplete, so absence of a found conflict is not evidence of safety.
  • productionSymbols: there is no passing E2E evidence at all in the current snapshot (typically stale or missing receipts). The stage now says so with reason instead of an opaque word. Existing uncoveredSymbols still lists every remaining production symbol; each explanation uses stage_blocked_no_passing_e2e rather than implying the symbol independently lacks covered_by.
  • Additive explanations[] never change status, reason, uncoveredSymbols, or proofStatus. Rejected covered_by candidates carry the earliest disqualifying reason and optional secondaryReasons already known from cheaper gates. Out-of-chain tests do not walk receipts.
• unresolved — evidence exists but is not conclusive (e.g. unresolved propositions in the inventory).

A blocked stage never silently downgrades a requirement's proof status: it maps to proofStatus: unresolved, not proven.

Gaps, advisories, and status

• proofGaps[] — blocking only. Every entry carries a code (e.g. missing_proof_receipt, missing_production_symbol_coverage), a priority, a stage name, and a suggested repair action.
• proofAdvisories[] — explicitly non-blocking context. Receipt-completeness codes (missing_proof_receipt, stale_proof_receipt, failed_proof_receipt, invalid_proof_receipt, and proof_contract_mismatch) remain blocking for every linked E2E obligation; they are never downgraded because another scenario has a passing receipt.
• proofStatus — the headline:
  • proven — all stages passed (proofGaps is empty by invariant).
  • missing — at least one stage is missing (evidence absent).
  • unresolved — evidence is inconclusive or a stage is blocked.
  • not_applicable — out of scope; see applicability above.
• proofRepairs[] — ranked concrete recovery actions derived from blocking gaps.

Common failure patterns

Related surfaces

• kibi coverage --by req --status missing (also: proven, unresolved, not_applicable) — enumerate exactly one proof-status slice; N/A rows include their applicability reason. The summary always reflects the whole KB.
• kibi proof inspect — detect test infrastructure and pick a proof integration.
• kibi proof explain REQ-* / kibi proof explain SYM-* — project the same Proof, labeling required_proofs, executable_for, and covered_by separately.
• kibi proof impact — compare current proof state to HEAD:proof/baseline.json (diagnostic; exits 0 after a successful report). The ratchet remains scripts/check-proof-baseline.mjs.
• bun run proof:baseline:semantic (this repository) — compare the committed baseline without re-proving: gaps that only reflect stale evidence (stale_proof_receipt, proof_contract_mismatch, and production coverage whose symbols all have a qualifying candidate or a scenario-backed E2E candidate rejected solely for stale evidence) are set aside. Unit/integration scope, missing receipts, invalid evidence, and scenario-chain failures remain blocking gaps.
• bun run proof:replay (this repository) — replay the CI proof job's gate steps from .github/workflows/proof.yml in a clean clone of the committed HEAD, outside the repository tree, and stop at the first failing step.
• kibi proof prune --keep 1 — drop superseded receipts (re-proving the same snapshot appends duplicates).
• kibi proof migrate-legacy — remove legacy verification_receipts blocks from tests that already carry a proof_contract.
• docs/proving-requirements.md — the runner-neutral proof pipeline: contracts, integrations, artifacts, and how kibi prove produces receipts.

Before pushing, run kibi sync --refresh-symbol-coordinates with the project-local CLI, review and commit the generated changes, and run bun run proof:prepush. If committing leaves the KB stale, sync it again before the check. This checks the committed manifests, publish metadata (including exact GitHub owner casing), and semantic baseline using the project-local CLI. When proof contracts, coverage links, or proof tooling change, also run bun run proof:replay to reproduce the full CI gate on committed HEAD.

The repository's pre-commit framework configuration includes a pre-push stage for the fast gate. Maintainers using that framework enable it with pre-commit install --hook-type pre-push; tracking the configuration alone does not install the hook. The fast gate checks the current clean checkout; use the corresponding checkout when pushing another branch or an explicit ref.