URGENT: the required Kani gate is RED on main — ~14 engines fail in ~11s each, so nothing can merge

[avrabe]

What

Kani gate is a required status check. It is failing on main, and has been
across every recent main commit. The matrix legs failing include:

relay-sc  relay-lc  relay-hs  relay-to  relay-cfdp  relay-sca  relay-hk
relay-ci  relay-hal relay-fsafe relay-sensvote relay-sec relay-sch relay-tbl

Consequence: no PR can merge. The Format fix (#409 / PR #424) is blocked
behind it right now, and so is everything else.

It is infrastructure, not fourteen proof regressions

Each failing job completes in about 11 seconds:

05:47:36  Set up job
05:47:47  job complete   (failure)

Kani model checking does not finish in 11 s. The step that fails is
Kani verify <crate>; checkout and setup succeed. Fourteen engines regressing
simultaneously is not plausible; a toolchain or environment fault on the
self-hosted fleet is.

Runner: pulseengine-ci-01, group hetzner-private, runner version 2.337.0.
Disk is healthy (54% used, threshold 70%) so it is not the disk-full failure
mode.

I could not retrieve the failing step's own output — gh run view --log and
the jobs API both return the setup/teardown envelope without the step body.
Someone with log access should pull it; that is the missing piece.

This is the same shape as #405 (Verus: all 19 targets fail in 0.1 s with
can't find crate for core/std). Two verification tracks on the same fleet,
both failing fast, both in a way that looks like the toolchain cannot resolve
its environment.

It also exposes the vacuous-pass mechanism from #417

Kani runs pair up at the same minute, one success and one failure:

time	sha	result
05:47	8d53dd26	failure
05:25	3bf51253	success
05:25	1dfe4cf1	failure
05:17	fc7d47df	success

The successes are runs where the matrix was skipped — kani.yml's changes
job emits run=false when the diff matches nothing under crates/, and the
roll-up maps skipped → pass. The failures are the runs that actually executed.

So on PRs the gate has been reporting green without running anything, while
on main it has been red. Both halves are wrong in the same direction, and the
green half is the one people see on their PR.

Credit where due: the roll-up is honest when the matrix does run — Kani gate
correctly reports failure rather than masking it.

Suggested order

1. Get the failing step's log and fix the environment. This unblocks all merges.
2. Then All three required gates can pass vacuously for a PR that touches only the shipped wasm components #417: make the skip arm say it proved nothing, so a skipped matrix is
   not indistinguishable from a passing one.

Falsification

Wrong if Kani (relay-lc) passes on current main.