feat(vgate): the cross-check ran one way — 22 Kani proofs ran for months, untraced

[avrabe]

No Verify-Filter on this PR, deliberately. It changes the gate itself; its
evidence should be the unscoped default sweep.

The finding

v1.135 caught 19 Verus proofs that were defined and never ran. This is the
mirror image, and it had been true the whole time: 22 Kani harnesses that ran
on every push, recorded by nothing.

VGATE-P01 cross-checks in ONE direction — an artifact citing cargo kani -p X
for a crate outside kani.yml's matrix is an orphaned proof, because CI never
runs it. That catches evidence claimed but not executed.

It cannot catch the reverse. And a one-directional check is satisfied by citing
nothing: the fewer proofs an artifact claims, the less can be orphaned. The
incentive runs the wrong way, and the failure is invisible — nothing goes red, an
assessor just reads a hole in the trace that the CI log has been filling all along.

Measured

kani.yml matrix engines              45
cited by >= 1 artifact step          35
cited by NOTHING                     10   <- untraced

engine	harnesses
relay-hk	2	verify_collect_bounded, verify_no_panic
relay-cs	3	verify_crc_deterministic, verify_check_bounded, verify_no_panic
relay-ds	3	verify_decision_bounded, verify_disabled_no_decision, verify_no_panic
relay-fm	2	verify_empty_path_rejected, verify_no_panic
relay-ci	2	verify_valid_header_accepted, verify_no_panic
relay-to	2	verify_subscribe_unsubscribe, verify_no_panic
relay-md	2	verify_sample_bounded, verify_no_panic
relay-mm	2	verify_out_of_range_rejected, verify_no_panic
relay-tbl	2	verify_register_bounded, verify_no_panic
relay-ccsds	2	verify_encode_decode_roundtrip, verify_no_panic
	22

Confirmed by an independent query over different data. For every requirement
at implemented/verified/accepted, collect its verifies edges and flag
those whose verifiers all have zero steps. That returns exactly
SWREQ-{HK,CS,DS,FM,CI,TO,MD,MM,TBL,CCSDS}-P01 — the same ten, reached
without reading kani.yml at all. Their only verifies edge came from a stepless
roll-up (SV-RELAY-*), so the trace said "no executable evidence" for
requirements whose proofs were green in CI that same minute.

Two queries over different data converging is what makes this a finding rather
than an artefact of one script.

The design decision that matters: filter-independence

kani_cited_crates() scans the artifact tree from disk, not the filtered set
the run is executing. Coverage is a property of the graph, not of one run's
scope.

Computed from the filtered set, Verify-Filter: (has-tag "oci") (6 of 213
artifacts) would have reported 39 engines untraced — a spurious failure that
would have got the check deleted inside a week. Verified: under that filter it
still reports exactly the real set.

A filter can shrink what is executed. It must not shrink what is checked
for coverage.

Fail-closed on an empty matrix, mirroring the verus.yml empty-set guard: an
unreadable kani.yml would otherwise make coverage vacuously pass at "0 uncovered".

Negative case — observed, not assumed

+           - relay-fake-untraced        # injected into kani.yml
$ python3 scripts/run-falcon-verification.py --filter '(has-tag "oci")' --dry-run
# 1 UNTRACED PROOF(S) — ... NO rivet artifact cites them ...
#   relay-fake-untraced
exit 1

Reverted → exit 0.

The first injection attempt silently changed nothing (the matrix is a YAML
block list, not the inline-quoted form I assumed) and the run then "passed". So
the substitution count is now asserted before the result is believed — a negative
test that did not actually inject is a passing test proving the opposite of its
claim.

Gap closed, not just detected

FV-RELAY-KANICI-001 — whose stated scope is already "cFS engines' Kani
harnesses model-checked in CI" — goes 6 → 16 engines (30 → 52 harnesses) and
gains verifies edges to the ten SWREQ-*-P01.

Requirement-side query: 11 → 1.

What this does NOT claim

Citing the proofs makes the evidence visible; it does not argue the evidence
is sufficient. Ten of the 22 are verify_no_panic — a totality property, not
a functional one — so the ten requirements stay at implemented, not promoted on
the strength of a link that did not exist yesterday.

The one remaining case is named, not papered over

SWREQ-FALCON-SIM-P04's eight verifiers (FV-FALCON-SIM-006..013) are stepless
gz-sim bench artifacts. A step asserting the recorded bench-evidence CSVs still
exist would zero the query and verify almost nothing — it would check that a
May-2026 record is still on disk, not that the software still produces it. That is
optimising the metric instead of the property, which is the failure this gate
exists to prevent.

Evidence

rivet validate                                   exit 0
python3 scripts/run-falcon-verification.py --dry-run   exit 0, 0 FAIL, 0 UNTRACED
negative injection                               exit 1 (detector fires)

Note for the merge order

This touches scripts/run-falcon-verification.py, as does #342. Expect to rebase
this onto #342 once that lands — #342 goes first (it fixes a gate that can pass
having verified nothing, and everything after it should be validated under the
fixed gate).

Two-commit rule: this PR carries code, so nothing goes past implemented.

Refs #6

🤖 Generated with Claude Code

https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG

[avrabe]

Post-open verification: the steps were only ever run --dry-run. Now executed.

FV-RELAY-VGATE-002's steps recurse into the gate — a gate step that invokes
the gate. That deserved to be executed rather than reasoned about, since a
--dry-run pass says nothing about what CI does.

Executed exactly as CI will, no --dry-run on the outer call:

$ python3 scripts/run-falcon-verification.py --filter '(has-tag "verification-gate")'
# 2 artifact(s) matched: FV-RELAY-VGATE-001, FV-RELAY-VGATE-002

  [PASS] (0.26s) FV-RELAY-VGATE-001: run-falcon-verification.py --filter '(has-tag "rotor-loss")' --dry-run
  [PASS] (0.09s) FV-RELAY-VGATE-001: check-verification-independence.sh 23fc92f && exit 1 || true
  [PASS] (0.04s) FV-RELAY-VGATE-001: check-verification-independence.sh HEAD
  [PASS] (0.20s) FV-RELAY-VGATE-002: run-falcon-verification.py --filter '(has-tag "verification-gate")' --dry-run
  [PASS] (0.33s) FV-RELAY-VGATE-002: test "$(... --filter '(has-tag "oci")' --dry-run | grep -c 'UNTRACED PROOF')" -eq 0
  [PASS] (0.04s) FV-RELAY-VGATE-002: check-verification-independence.sh HEAD

REAL EXIT=0

FV-RELAY-VGATE-001 has shipped a recursive step since v1.116, so the pattern is
CI-proven, not novel here.

Interaction with #342, checked because it is non-obvious

#342 (merged this morning) fails the gate when verification-output.md contains
# 0 artifact(s) matched. A recursive step prints its own # N artifact(s) matched line — so if a nested run ever matched zero, it could trip the outer
guard and fail a gate that was working correctly.

It cannot, and the reason is mechanical rather than lucky:

proc = subprocess.run(cmd, shell=True, capture_output=True, text=True)   # line 483

Step output is captured, so a nested run's stdout never reaches the outer
stream that becomes verification-output.md. Both nested filters are also
non-empty by assertion (verification-gate → 2, oci → 6).

Two-commit rule

FV-RELAY-KANICI-001 moves approved → implemented here, which is within the
rule, but the script decides, not me:

$ scripts/check-verification-independence.sh $(git merge-base origin/main HEAD)
two-commit rule: OK (code-changed=no, terminal-status-added=no)
exit 0

Not pushing these results into the artifact text — that would cancel and restart
a ~50-minute gate run for an evidence note. Recorded here instead; it folds into
the artifact in the post-tag verify PR that promotes it.

🤖 Generated with Claude Code

https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG