pv proof-status credits L3 for kani_harnesses whose harness fn does not exist, even with --verify-bindings #4531

Measurement

pv 0.70.0 (1274d04). Command: pv proof-status contracts --binding contracts/binding.yaml --verify-bindings . --format json, run on paiml/rust-mdipierro-nlib at dda2faa.

Ten contracts reach L3 on Kani claims that cannot run:

• fourier-transform-v1, graph-algorithms-v1, integration-v1, matrix-algebra-v1, monte-carlo-v1, nonlinear-solvers-v1, optimization-v1 and random-generators-v1 each declare 3 harnesses and have 0 present.
• sorting-v1 and statistics-v1 each declare 3 and have 1 present.

Example: matrix-algebra-v1 declares harness: verify_matmul_shape, verify_inverse_roundtrip and verify_cholesky_roundtrip. None of the three exist anywhere in the crate, yet pv proof-status reports the contract at L3.

Expected

--verify-bindings already downgrades phantom "implemented" bindings: it checks that the function exists in source. The same check belongs on L3. A kani_harnesses[].harness name should count only if a #[kani::proof] fn with that name exists under the scanned root. Otherwise it should be reported as phantom, the way ONT-2a excludes self-declared L4.

Stronger still, and already parked as #3495: credit only harnesses that CI actually ran.

Related

• 824 of 876 contracts have anonymous obligations and 586 kani references point at nothing — pv validate says 0 errors #3314: dangling kani_harnesses[].obligation references (a different field).
• VERIFY-001: run the 132 Kani harnesses in CI (proof credit from runs, not declarations) and pilot Verus on one dequant/parser function #3495: proof credit from runs, not declarations.

Downstream workaround

scripts/proof_ratchet.sh in rust-mdipierro-nlib checks each harness name against the #[kani::proof] fns under src/. The README states "Kani harnesses exist for 12 of the 22 contracts that declare them", and the phantom count (28) may only fall.

🤖 Generated with Claude Code