Three verification runs printed green while the run could not have failed: an assertion never reached, a model checker that instrumented nothing, and an axiom audit identical for a correct model and a wrong one.

The system said: Verifier: green.
The evidence showed: The run could not have failed: a Kani assertion never reached, a loom test that instrumented nothing, and a Lean axiom audit byte-identical for a correct and a wrong model.

§ 1

The record

FINDING · verifier-green-run-could-not-failverify · coverage illusion

Three verification runs printed green while the run could not have failed: an assertion never reached, a model checker that instrumented nothing, and an axiom audit identical for a correct model and a wrong one.

Claim: A Kani harness left its second assertion UNREACHABLE after the first injected bug, so its pass carried no information; a loom test reported 1 passed on a build containing a lost update because the atomic was never loom-instrumented, with byte-identical output for the clean and broken builds; and two Lean models of the same Rust function, one pinning real sizes and one returning 0 for every type, produced byte-identical axiom audits.

Status: OBSERVED Witnessed in one instance. No claim about how often.

Question: Passed is not correct

Subject: Recorded verification outputs from Kani, loom and cargo test on the governor and jsonwebtoken crates (third-party code, injected defects), and two Lean models of a kernel Rust parser. third-party subject

Frame: Three case studies with inputs, patches, outputs and reproduction commands committed; Lean audit compared by sha256.

Method: A grader that extracts what a run actually explored (reachability, instrumented interleaving counts, value lemmas) and grades on that rather than on the printed verdict.

Oracle: What distinguishes the runs when the verdicts do not: an execution count (9 uninstrumented against 54 instrumented interleavings), an UNREACHABLE status, and value lemmas proved by rfl that fail on the wrong model.

Negative control: Present One control was mistaken for two until a second, independent Kani bug was built; the loom clean and broken runs are both committed so the byte-identity is checkable.

Denominator: 3 catches, each with committed inputs and outputs; 9 versus 54 interleavings; 0 bytes of difference in the two axiom audits.

Limitation: No defect in governor or jsonwebtoken is claimed; the crates are subjects for the recorded-output grader, and the bugs were injected. The grader reads recorded outputs and runs no verifier itself. Version 0.1.

Source: repowazdogz-droid/evidence-audit @ 996d248

Reproduce: pip install -e . && python3 -m pytest tests/ -q

Independent reproduction: None known.

§ 2

Where this sits

This finding answers Passed is not correct and supports the VERIFY stage of the operating method. It is an instance of the coverage illusion mechanism.

Evidence ledger Bring a claim like this one