verus.yml PR trigger is path-filtered on LEAN paths — the Verus gate never runs on a PR that touches a Verus proof

[avrabe]

What

.github/workflows/verus.yml:19-27

  # PR runs are path-filtered (CI diet): the Lean proofs (Lyapunov/WCET) are
  # self-contained under proofs/lean. NON-REQUIRED check; skip never blocks a
  # merge. push:main stays UNFILTERED (backstop).
  pull_request:
    branches: [main]
    paths:
      - 'proofs/lean/**'
      - '.github/workflows/lean.yml'

The entire 13-line header and the on: block are copy-pasted from lean.yml
and describe Lean/Mathlib. But the job body runs
bazel query 'kind("verus_test rule", //:*)'.

Verus sources live in crates/*/src/engine.rs and the targets in BUILD.bazel.
Neither path is in the filter. So no PR that edits a Verus proof, adds a
verus_test target, or edits verus.yml itself ever triggers this workflow.

It runs only on push: main — where it has failed on every run since
2026-09-11 (#405).

Why this compounds #405

#405 is "the Verus toolchain cannot find core/std, so all 19 proofs fail in
0.1s". This is the other half: even when the toolchain is fixed, a PR that
breaks a Verus proof will still merge green, because the workflow will not run
on it. Fixing #405 alone restores a gate that only ever fires after the fact.

The workflow was created by b777ba9 — "enforce the Verus track — 19 proofs
were defined and NONE ever ran". The enforcement mechanism reintroduced the
defect one layer up.

Also self-contradictory

verus.yml:21 says "NON-REQUIRED check; skip never blocks a merge".
verus.yml:31 says "required check, evidence preservation".
Neither Verus proofs, Lean proofs nor Rocq + Gappa proofs is in the
required set — and lean.yml:8 and rocq.yml:9 carry the same false "required
check" claim. Rivet artifacts cite these workflows as their enforcer.

Fix

Set the filter to what the workflow actually verifies — crates/**,
BUILD.bazel, .github/workflows/verus.yml — and reconcile the two
contradicting comments. The discovery logic inside the job (bazel query plus
an empty-set guard at :113-117) is the correct pattern and should stay; it is
the model the rest of the repo should copy.

Falsification

Wrong if a PR that edits crates/relay-primitives/src/engine.rs triggers the
Verus proofs workflow.