Formalization lemma verdict consistency

The check is formalization_lemma_verdict_consistency. It is verify-stage. Severity of a conflict is warning, not fail. The inspect command is the same audit, plus proof verify-lemma --no-cache ./....

The hop joins SYS-REQs whose formalization_status is valid against a lemma the YAML names in traces.verified_by_extra as LEMMA:<scope>/<name>, or a Go lemma that names the SYS-REQ with // verifies:. The cache is .proof/lemma-cache.json, filled by proof verify-lemma. A conflict is a most-recent verdict of timeout, unknown, translation_error, or solver_crash. The honest status for that row is inconclusive.

The help file teaches the silent overstatement first. Status and solver cache live in separate files. Nothing in the suite asked whether they contradicted.

# specs/system/requirements/SYS-REQ-010.req.yaml
id: SYS-REQ-010
verification:
  formalization_status: valid
traces:
  verified_by_extra:
    - LEMMA:resolve/resolvable_reset_clears_walker_state

# .proof/lemma-cache.json
# resolvable_reset_clears_walker_state: timeout

# proof audit --check formalization_lemma_verdict_consistency
# [VERIFICATION] formalization_lemma_verdict_consistency
# SYS-REQ-010 claims formalization_status=valid but lemma
# "resolvable_reset_clears_walker_state" is inconclusive (verdict=timeout)
# silent valid: the suite still printed green

Downgrade to inconclusive if the lemma is still undecided. Re-run proof verify-lemma --no-cache ./... if a rewrite should decide it. Remove the LEMMA: row only when the lemma is gone, then proof verify-lemma --prune-cache ./.... Then re-run the same check. Do not delete a live lemma reference to make the warning disappear. That leaves valid standing on nothing.

proof verify-lemma --no-cache ./...
proof verify-lemma --no-cache --timeout 120s ./...
proof verify-lemma --prune-cache ./...
proof audit --check formalization_lemma_verdict_consistency --verbose

The teaching graph is still one SYS-REQ whose board called the formalization done and whose lemma cache never decided. Close it by writing inconclusive, by re-running the solver until it PROVES, or by dropping a lemma that is genuinely gone. The same hop also walks the reverse // verifies: annotation. A pair that appears both ways is one finding. A missing cache file is a skip, with a hint to run verify-lemma. An absent lemma name in the cache is a separate informational finding, not this mis-classification. Do not treat proof verify-lemma --allow-unknown as this hop. That flag changes the CI exit code. It does not make valid true.

# specs/system/requirements/SYS-REQ-010.req.yaml
verification:
  formalization_status: inconclusive
traces:
  verified_by_extra:
    - LEMMA:resolve/resolvable_reset_clears_walker_state

# proof audit --check formalization_lemma_verdict_consistency
# no valid-on-undecided join. this hop is quiet

The solver hop stays on Z3/Kind2 on one function. The assume hop stays on assume contract consistency. Jama still authors. Proof vs Jama.

Warning, not fail. Not blocking. No project loaded is a pass. No .proof/lemma-cache.json is a skip, not a fail. A SYS-REQ with valid and no lemma reference is a silent pass: a FRETish-only formalization may claim that. The hop looks at formalization_status, LEMMA: traces, // verifies: comments, and the cached verdict. It does not re-run Kind2. It does not re-run Z3. It does not write the YAML. It does not prove the Go. Raising severity to error in proof.yaml is a strictness setting, not a remediation. We have not scored this floor against a frozen Jama pack or a ReqIF export. The loss is named, not scored.

The solver hop stays on Z3/Kind2 on one function. The engagement stays on software correctness audit. Jama still authors.

What is formalization lemma verdict consistency? Same question. Same URL.

Is this Z3 or Kind2 on one function? No. That hop runs the solver. This hop asks whether a SYS-REQ that already claims valid still matches that cache. See Z3/Kind2 on one function.

Is this lemma binding freshness? No. That hop is a separate-file binding whose SHA-256 no longer matches the live function. This hop is a SYS-REQ that still says valid while the lemma cache is timeout. See lemma binding freshness.

Is this lemma branch coverage? No. That hop is a production AST branch with an empty covered_by. This hop is a SYS-REQ that still says valid while the lemma cache is timeout. See lemma branch coverage.

Is this assume contract consistency? No. That hop is a source // reqproof:assume whose callee lemma must exist. This hop is a SYS-REQ that already names a lemma. See assume contract consistency.

Is this DO-333? No. That hop is the DO-178C formal-methods supplement. This hop is one cache join. See DO-333.

Is this design by contract? No. That hop matches YAML assume/guarantee pairs. This hop is valid vs the lemma cache. See design by contract.

Does a tree with no lemmas pass? Yes. No valid SYS-REQ with a lemma is a pass. That is not a proof that the Go is correct. It is a proof that this hop had nothing to join.

Does a green hop prove the code matches the shall? No. The hop observes YAML fields and a cache file. It does not prove the Go.

Is Proof a Jama alternative for the shall? No. Jama still authors. Proof vs Jama.