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.v5); 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. Three things can take a requirement out of scope:

1. Supersession — a newer requirement links to it with supersedes.
2. Retirement — status: retired with a retired_reason: the behavior is gone and nothing replaces it. The applicability reason reads "requirement is retired: the behavior it stated no longer exists".
3. 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 the stages below, in order. Each stage reports a status under its key in proofStages; productionSymbols also carries a typed reason when it does not pass.

1. Semantic inventory

Checks: every assertive statement in the requirement's prose is listed in its semantic inventory and classified as modeled, unresolved, missing or nonlogical.

• passed: the inventory is complete and nothing in it is unresolved.
• missing: there is no inventory, an entry is classified as missing, or an entry is malformed.
• unresolved: at least one statement is classified as unresolved.

2. Logic grounding

Checks: each modeled claim is grounded by a strict property, predicate or safe rule fact, one to one with the declared manifest.

• passed: every modeled claim has exactly one grounding fact.
• missing: a claim has no grounding fact or no manifest entry.
• unresolved: the grounding exists but does not line up (an extra or duplicate manifest entry, claim text that differs, an invalid or undeclared fact, an unsafe rule).

3. Contradictions

Checks: no other current requirement contradicts this one over shared facts.

• passed: no conflict was found and grounding is complete.
• blocked: a conflict was found; conflicts names it.
• unresolved: the check could not finish, usually because logic grounding is incomplete, so the absence of a found conflict is not evidence of safety.

4. Scenarios

Checks: at least one scenario specifies the requirement (specified_by).

• passed: one or more valid scenarios are linked.
• missing: no scenario is linked, or a link points at a scenario that does not exist.
• blocked: a linked success scenario is infeasible; infeasibleScenarios names it.

5. Scenario tests

Checks: each linked scenario is validated by at least one test (verified_by or validates).

• passed: every scenario has a test.
• missing: a scenario has no test, or links a test that does not exist.

5a. Failure side

Checks: a requirement that grounds a claim (a requires_property, requires_predicate or requires_rule fact) is not tested through its happy path alone. At least one linked scenario must expect rejection or error and assume a value or situation the requirement forbids: either the scenario-feasibility analysis finds a witness naming the requirement, or one of its assumes facts opposes one of the requirement's claim facts directly (a conflicting value or polarity on the same subject and property, the opposite polarity of the same predicate, or, for a rule over predicates, a predicate fact instantiating one of the rule's atoms). For a guarantee rather than an input constraint, the assumed fact describes the attempt to break the guarantee, and rejection means the system refuses or contains it.

• passed: negativeScenarios lists the linked scenarios that do this.
• missing: none does; the requirement gets the happy_path_only gap, and suggestedNegatives gives, per open claim, a fact that opposes it (the value just past a numeric bound, the other boolean, a different string, a set missing a required member, the opposite polarity of a predicate).
• not_required: the requirement grounds no claim, or a fresh certificate proves every claim at code scope (certifiedClaims): a certificate decides both sides of the claim already. When every open claim is proved by a certificate test whose receipt is only older than the code (pendingReproofClaims), the evidence floor reports pending_reproof rather than below, as for any other stale receipt.
• waived: the requirement has no failure side to test. Its claims state a capability or an output shape, so there is no input or attempt to refuse. The requirement records why in failure_side_waiver and who accepted it in failure_side_waiver_approved_by, and waiver shows both. A reason without an approver stays missing, and kibi proof explain reports the waiver as awaiting approval.

The negative scenario needs a test like any other linked scenario, so the failure side is proven by the same passing E2E receipts. The canonical scenario-outcome-mismatch check rule reports a scenario that expects rejection or error while current requirements govern and permit everything it assumes.

5b. Quantified claims

Checks: a claim that quantifies over a collection (each, every, all) or bounds a cardinality (exactly, at least, at most, no more than) is grounded on what varies, not only on its verdict. When every fact grounding such a claim is a boolean property_value or a ground predicate, the claim states that the behavior holds without naming the dimension it holds over, and a scenario with one item can pass where several items break. Ground it on an integer count or bound, a set of members, a rule over a variable, or a state machine instead. only, any and some are not counted: they mostly scope a condition ("only when", "before any write") rather than range over one.

• missing: claims lists each such claim with its quantifier, the grounding factIds, and rewrites, the typed groundings that would represent it, likeliest first (bound for a cardinality; rule, count or set for a collection). The requirement gets the dimension_unrepresented gap.
• not_required: no grounded claim is quantified this way, or a fresh certificate proves the claim at code scope. Stale certificate receipts are reported as pendingReproofClaims, as in the failure-side stage.
• waived: every such claim has an approved waiver. When the quantifier word ranges over nothing ("start without all network access"), the grounding fact records why in dimension_waiver and who accepted it in dimension_waiver_approved_by; waivedClaims lists them. A reason without an approver keeps the claim in claims, and kibi proof explain reports it as awaiting approval.

kb_semantic_advisor marks the same clauses: each normative proposition with such a quantifier carries dimension with its quantifier and rewrites, so the grounding can be chosen before the fact is written.

5c. Edge cases

Checks: every value class a typed property claim predicts is refused has a scenario that reaches it. Kibi derives the cases from each property_value fact the requirement grounds a claim on with requires_property:

• a numeric bound yields the bound itself (or the nearest value inside a strict bound) and the class past it: files_per_batch lte 5 gives eq 5 (success) and gt 5 (rejection);
• an integer bounded at one or more also yields zero, one and many (eq 0, eq 1, gte 2), keeping only the classes that fall wholly on one side of the bound;
• a set yields each member (success) and the value outside it: rejection for eq and subset_of, unspecified for includes; each member of an excludes set is a rejection case.

A case is dropped when an earlier one already names its class with the same outcome, and one fact yields at most 12 (limitReached says when the cap cut). Each case has a stable caseId (CASE- and 12 hex characters) and the assumption a scenario would state to land in it.

A case is covered by a scenario of the requirement that is not a draft, whose expects matches the prediction (rejection also accepts error), and whose assumes fact on the same subject and property entails the case: files_per_batch eq 6 covers gt 5. Success cases are reported but do not block; the requirement's success scenarios already exercise them.

• missing: a rejection case is uncovered; uncoveredCases lists them and the requirement gets the uncovered_case gap. The repair plan's case_scenarios phase carries caseSkeletons, an upsert-ready draft scenario and assumed fact per case: fill in any placeholder value, verify the scenario by a test and make it active.
• passed: every rejection case is covered.
• not_required: no grounded claim predicts a rejection case, or a fresh certificate proves the claim at code scope. Stale certificate receipts are reported as pendingReproofClaims.
• waived: the uncovered rejection cases all belong to facts with an approved waiver. When the cases are covered another way (a unit suite that walks every value, a class the system cannot produce), the grounding fact records why in case_waiver and who accepted it in case_waiver_approved_by. A reason without an approver keeps the gap.

kibi coverage --cases lists every requirement's cases with their coverage, and kibi proof explain prints the assumption each uncovered case needs. kb_semantic_advisor previews the cases of each strict-property suggestion in casesPreview, so the scenario debt shows before the fact is written.

6. Passing E2E tests

Checks: every linked scenario has at least one end-to-end test, and every linked E2E test that bears proof carries a valid, fresh, passing kibi.proof-receipt.v1 receipt bound to the current snapshot, contract hash and fingerprint.

• passed: every scenario obligation passed.
• missing: a scenario has no qualifying E2E test or receipt.
• unresolved: the evidence exists but does not qualify (for example a stale, failed or invalid receipt).

Per-scenario results are in scenarioObligations, each with the acceptedScopes it allows. Unit and integration tests linked alongside the E2E tests do not block. A UI pattern scenario also accepts component tests; see Component-scope proof.

7. Executable test symbols

Checks: each qualifying E2E test is linked to executable test code with executable_for.

• passed: every qualifying test has executable code linked.
• missing: a test has no executable_for link; missingTests lists it.
• blocked: there are no passing E2E tests to check.

8. Production symbols

Checks: the production symbols that implement the requirement are covered by the passing E2E tests (covered_by).

• passed: every production symbol is covered.
• missing: no production symbol implements the requirement, or some lack covered_by links; uncoveredSymbols lists them.
• blocked: there is no passing E2E evidence in the current snapshot (usually stale or missing receipts), so coverage cannot be evaluated. reason says so and points at kibi prove.

Type-shape symbols (interfaces, type aliases, enums) are listed under structuralSymbols instead. One counts as covered when it is covered_by a passing E2E test or a unit test with a current passing receipt; an authored status: passing on the unit test is not enough. Without that receipt the symbol is in uncoveredSymbols with the reason structural_unit_receipt_not_current, and kibi prove on the unit test (or kibi prove --stale) clears it.

explanations[] gives each symbol a rollup reason and, for each rejected covered_by candidate, a primary rejection code plus optional secondary codes. See Stage statuses, precisely.

9. Source coordinates

Checks: the requirement source and every linked test and production symbol carry exact published coordinates.

• passed: all coordinates are present.
• missing: the requirement has no source, or a symbol has no coordinates; missingSymbols lists them.
• blocked: there are no linked symbols to check.

Component-scope proof for UI patterns

A scenario whose specifying requirements are all grounded only in the built-in UI pattern predicates (ui_pattern, same_pattern, pattern_marker, each linked with requires_predicate, and no requires_property or requires_rule) accepts tests with verification_scope unit or integration as well as end_to_end. Such a test still needs a valid, fresh, passing receipt, executable_for code, and covered_by links for the production symbols it proves. Its obligation reports acceptedScopes: [unit, integration, end_to_end]; every other scenario reports [end_to_end].

The reason is cost, not leniency: a pattern ("this list is a line-and-dots timeline in both variants") is fully observable by rendering one component in isolation, so demanding a browser test per pattern would make E2E suites heavy for no extra evidence. The moment the requirement also carries a layout fact such as ui_container, a strict property or a logic rule, the scenario goes back to end-to-end proof. See ui-requirements.md.

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.
• unresolved: evidence exists but is not conclusive (for example unresolved statements in the inventory, or a stale receipt).
• blocked: the stage found a hard stop or has nothing to evaluate:
  • contradictions: a conflicting requirement was found.
  • scenarios: a linked success scenario is infeasible.
  • executableSymbols and productionSymbols: there is no passing E2E evidence in the current snapshot (typically stale or missing receipts). productionSymbols says so in reason; uncoveredSymbols still lists every remaining production symbol, and each explanation uses stage_blocked_no_passing_e2e rather than implying the symbol itself lacks covered_by.
  • sourceCoordinates: there are no linked symbols to check.

explanations[] on productionSymbols never changes status, reason, uncoveredSymbols or proofStatus. A rejected covered_by candidate carries the earliest disqualifying reason and optional secondaryReasons already known from cheaper checks. Tests outside the scenario chain do not have their receipts read.

A blocked stage never silently counts as passing. A blocked contradictions stage makes proofStatus unresolved; any other blocked stage does the same unless another stage is missing, in which case proofStatus is missing.

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:
  • tested — all stages passed (proofGaps is empty by invariant). Until kibi.requirement-proof.v4 this value was proven; it was renamed because passing end-to-end tests are evidence, not proof.
  • 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.

Evidence levels

proofStatus says how far a requirement climbed the ladder. evidenceLevel says how strong the evidence behind it is, and is never stronger than what backs it:

Each row's evidence[] lists the entries that earned the level, each with kind (certificate, e2e, human_intent), scope (code for what the tests exercised, intent for what a person stated) and level; an e2e entry names its passing tests, a certificate entry its proved tests and their proof kinds, a human_intent entry its basis (approved or firm) and, when there is one, the ref to the person's words. The coverage summary counts rows per level under evidenceLevels.

From kibi.requirement-proof.v5 each row also judges its claims one by one. claimEvidence[] has an entry per inventory claim with its claimKey, status, whether it is applicable (a nonlogical context span is not), the level it reaches and the certificate bindings behind it (derived, attested or rejected, with the test, kind, scope and reason); claimSummary counts the applicable claims per level (proved, attested, tested, unresolved) and unprovedClaims lists those below proved. A claim is proved only through a derived binding with scope code; an attested binding (the fact has no derivation) and an intent-scope one (an arithmetic claim decided from the facts alone) count as tested. The coverage summary adds the claim totals under proofClaims.

Firmness and evidence level are separate axes. Firmness says how sure the person is; the level says how strong the evidence is. A firm requirement at asserted is the gap to close before relying on it.

Evidence floors

Each current requirement also has a floor: the weakest evidence level it accepts. The evidence-floor rule of kibi check fails while a requirement's level is below its floor, so a regression is caught on the requirement itself and no shared snapshot file has to be kept in step.

Coverage rows carry the floor as evidenceFloor with required, source (explicit, firmness or approval) and status: met, below, or pending_reproof when the floor is tested and every gap only says the receipts are older than the code. A plain kibi check lets pending_reproof pass, so a local check catches grounding, contradiction and link regressions without re-proving first. kibi check --fresh-evidence judges receipts as they are and also needs a clean proof snapshot; run it right after kibi prove, as CI does. The coverage summary counts current requirements with a floor under evidenceFloors (met, below, pendingReproof), the coverage table has a Floor column, and kibi report and kibi signoff show each requirement's floor and whether it is met.

Requirements outside proof scope (proof_exempt, superseded or not current) have no floor. Lowering a floor is a visible edit to the requirement, so reviewers see it; give the reason in the requirement when you lower one.

The schema 11 upgrade (kibi migrate --yes) records required_evidence: asserted on each current firm requirement that has no scenario verified by an end-to-end test with a proof contract and a passing receipt, since it has not reached tested; raise it once the requirement has an end-to-end proof. Firm requirements whose proof has passed keep the tested floor, and the migration lists them. Their proof can still have gaps it does not read, such as a stale receipt or a production symbol without covered_by, so run kibi check --rules evidence-floor after migrating and fix what it reports.

The schema 15 upgrade does the same for approved requirements: an agent's requirement that a person approved and that states no firmness now needs tested, so kibi migrate --yes records required_evidence: asserted on each current one without a passing proof path and lists the ones that keep the tested floor. Remove the pin once the requirement has an end-to-end proof.

One more rule reads the same requirement proofs: agent-requirement-unapproved-implemented (canonical, KB schema 15) blocks a current priority: must requirement whose origin.kind is agent, that production symbols implement, and that nobody has approved (origin.approved_by) more than 14 days after it was written: shipped behavior must not rest on a requirement no person confirmed. The age comes from authored data only: origin.recorded_at (every kb_upsert write records it), else a created_at the requirement's front matter states; a requirement with neither counts as older. So does one whose date is not an ISO 8601 date (yesterday, 2026-13-45) or lies more than a day in the future: the finding names the unusable date, and its evidence carries sinceProblem: not-a-date or future. kb_upsert refuses such a created_at or origin.recorded_at on a requirement, so an agent cannot keep its own requirement out of review with a date. The stored created_at is not read, because sync fills a missing one with the sync time. The schema 15 upgrade (kibi migrate) lists the agent's must requirements this rule can fail right away.

The schema 12 upgrade binds certificates to claims. kibi migrate --yes pins proves on each certificate-kind contract whose test reaches exactly one claim its kind can prove and lists the other contracts for review. Until a contract names its claims, the blocking proof-contract-claims rule reports it and its certificate proves nothing, so a requirement that reported proved before reports tested until its claims are bound and re-proved with kibi prove.

Knowledge-base certificates

Evidence levels describe requirements. The kb-consistency rule of kibi check (and kb_check) covers the knowledge base itself: it states a few theorems about the facts current requirements name, finds a certificate for each, and re-checks every certificate with a separate checker (certificate_check.pl) that never searches and never loads the code that found the certificate.

The property theorem is joint: facts that contradict only together, where every pair still admits a value (for example int >= 0, <= 1, != 0, != 1), are a contradiction here even though the pairwise domain-contradictions rule is silent. A core whose facts are never valid at the same time is reported as property_unresolved, not as a contradiction. A context the checker cannot compare (mixed value types or units, an operator other than eq/neq on a non-numeric value, an unknown polarity) is unresolved and needs no certificate; it never counts as consistent.

A re-verified contradiction (a core, two disagreeing facts or a negation cycle) is a blocking kb-consistency violation, and so is a certificate the checker rejects. An unresolved context is a non-blocking kb-consistency-unresolved diagnostic. kibi check --staged runs the rule too, so a commit that introduces a joint contradiction is blocked. Opposing rule pairs and scenario feasibility are not certified yet; their own kibi check rules still decide them. Certificates are regenerated on each run and are not committed: kibi check --write-certificates <file> saves the bundle, and kibi check --certificates <file> re-checks a saved one and prints each theorem's verdict (proved, disproved or unresolved).

The numeric decision procedure, proved

Numeric contradictions, the arithmetic certificate kind and the property theorem above all rest on intervals.pl, which folds every comparison on a variable into an interval (open or closed ends, excluded points) or, for an integer variable, an integer range, and asks whether it is empty. The Lean 4 project in proof/lean defines the same folds and proves:

The proofs hold for any dense linear order without endpoints that embeds the integers with a floor and a ceiling, so for the rationals and the reals, and rest on Lean's standard axioms only (CI fails on sorry). The rationals the model's executable computes with are proved to be such an order, so the theorems cover the executable itself. A proof about a model says nothing about the shipped code unless the two compute the same thing, so scripts/intervals-differential.ts decides 200000 generated cases (rationals, integers and floats) with intervals.pl on the bundled SWI-Prolog, with the Lean model's executable and with an independent CLP(Q)/CLP(FD) oracle, and fails on any disagreement. intervals.pl rejects a NaN or infinite bound with a domain error. Both run in CI (lean-intervals-proof) and as the proof of REQ-kibi-intervals-verified.

Common failure patterns

Related surfaces

• kibi coverage --by req --status missing (also: tested, 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, propose a proof integration, and return the reviewed plan that writes .kb/proof/integrations.json through kb_apply_plan.
• kibi proof explain REQ-* / kibi proof explain SYM-* — project the same Proof, labeling required_proofs, executable_for, and covered_by separately.
• kibi check --rules evidence-floor — fail every current requirement whose evidence level is below its floor (see Evidence floors). Without --fresh-evidence, 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) count as pending re-proof, so a local run catches semantic regressions without re-proving. Unit or integration scope, missing receipts, invalid evidence, and scenario-chain failures stay blocking.
• bun run proof:gate (this repository) — the integrity rules plus evidence-floor, as the pre-push hook and the KB merge workflow run them; CI runs it again with --fresh-evidence after kibi prove --all.
• 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 compact — one-off: drop receipts that can no longer decide proof from a store written before kibi prove compacted histories on ingest. Coverage decisions are unchanged.
• kibi proof prune --keep 1 — keep only the newest receipt per test, whether or not older ones still decide proof.
• 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 with the project-local CLI (it keeps the gitignored symbol coordinates current), commit, 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 evidence floors (scripts/proof-gate.sh) 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.