ci: Kani Proofs fails ~58% with exit 143 and has never passed on a push to main

[avrabe]

Summary

Kani Proofs fails roughly 58% of the time and has not succeeded once on a
push to main in the sampled window. Exit code is always 143 (SIGTERM).
It is continue-on-error: true and is not among ci-gate's needs, so it
blocks nothing — which is exactly why it has been merged past repeatedly today
without anyone establishing what is actually killing it.

Data — last 15 CI runs

conclusion	count	durations
success	5	454, 457, 468, 484, 500 s
failure	7	270, 283, 344, 345, 368, 375, 460 s
cancelled	2	3300, 3301 s

The distribution is bimodal. Successes cluster tightly at 454–500 s; six of
seven failures die at 270–375 s — before the work would have completed. This
is not a uniform random kill.

Split by event:

event	success	failure	cancelled
push → main	0	4	2
pull_request	4	3	0
schedule	1	0	0

Ruled out

• Not a job timeout. timeout-minutes: 45; failures die at ~5 minutes.
• Not concurrency cancellation. cancel-in-progress is
  ${{ github.event_name == 'pull_request' }}, yet push-to-main runs fail
  too — and those would report cancelled, not failure.
• Not a proof regression. The failing step is the
  model-checking/kani-github-action@v1 step itself; cargo kani -p rivet-core
  is skipped afterwards, so verification never starts.

Not established

What sends the SIGTERM. Worth noting that the evidence is inconsistent:
some failures log ##[error]The runner has received a shutdown signal (e.g.
the run on #813), others log only Process completed with exit code 143 with no
shutdown line (the run on #836). If it were purely hosted-runner reclaim I would
expect that message consistently.

Candidates for whoever picks this up:

1. OOM inside CBMC. Kani is memory-hungry and ubuntu-latest is modest. A
   kernel OOM-kill is normally SIGKILL/137, but a wrapper script can translate
   it to 143 — check dmesg/runner diagnostics, or add /usr/bin/time -v.
2. An internal timeout in the action. The action's own script references a
   cargo timeout investigation; it may impose a bound well under our 45 min.
3. Hosted-runner reclaim, which would fit the message-bearing subset.

The PR path runs -p rivet-core --only-codegen while main runs the full
27-harness suite; that main/PR asymmetry lines up with main never passing, and
is the first thing to probe.

Why it matters even though it blocks nothing

A gate that fails 58% of the time trains everyone to merge past it. I did so
four times today, and each time the justification had to be re-derived. Either
it should be reliable enough to be a signal, or it should be explicitly marked
advisory and moved off the PR surface so it stops costing attention.

Related: #299 decoupled kani from needs:[test]; #509 covers self-hosted pool
liveness (kani is on ubuntu-latest, so a different surface).

[avrabe]

Triage note (scheduled routine, first pass on this issue — filed 2026-08-21, no prior comments).

The body is unusually well-instrumented for a CI-flake triage: 15-run sample, split by conclusion, split by event, both durations tabulated, and — the load-bearing bit — the observation that failures cluster tightly at 270–375s while successes cluster at 454–500s, i.e. the kill lands at a distinctly earlier point in the run than a natural completion, which is what tells you it isn't uniform-random. The ruled-out list is also tight: not the 45-min job timeout (deaths at ~5 min), not concurrency cancellation (those would report cancelled, and push-to-main fails anyway), not a proof regression (the failing step is the action itself, cargo kani is skipped afterwards).

What the routine can't autopick without is an ## Acceptance Criteria block, because the body deliberately leaves what sends the SIGTERM as "not established" — and the three candidates (OOM inside CBMC translated 137→143 by a wrapper; an internal action timeout; hosted-runner reclaim) point at three quite different fixes. Landing a remediation before diagnosis would just be a guess dressed up as a PR. The natural first slice is therefore instrumentation: make the next 15 runs answer the question the current 15 couldn't.

Sketch matching the kill-criterion shape used across adjacent triage threads (#832 / #833 / #835 / #807) — drop in / revise; picks the diagnostic slice as the starting point, since the remediation slice can't be pinned without it:

## Acceptance Criteria — Phase 0 (diagnose: pin what sends the SIGTERM)

- [ ] The `Kani Proofs` job in `.github/workflows/ci.yml` grows a pre-step
      that captures resource ceilings and post-mortem signals **before** the
      `model-checking/kani-github-action@v1` step runs, so a failure at
      270–375s carries evidence of what killed it:
      - `/usr/bin/time -v` (or equivalent) wraps the kani invocation so
        wall time, peak RSS, and the exit signal are in the job log
        regardless of how the outer process dies.
      - A post-step (`if: always()`) dumps `dmesg -T | tail -200` (looking
        for `Out of memory: Killed process`), `journalctl -k --since '-10m'`,
        and `free -m` — so a kernel OOM-kill translated 137→143 by a wrapper
        script is legible in the log, and so is the case where memory
        headroom was never the problem.
      - The action's own environment (`KANI_TIMEOUT`, any internal
        cargo/CBMC bound the action script sets) is printed so a "the
        action's own timeout is well under our 45 min" hypothesis is
        checkable rather than inferred.
- [ ] The job runs on a **matrix** for one release cycle: `ubuntu-latest`
      (current) and `ubuntu-latest` with an explicit `runs-on` upgrade to
      whichever larger runner class is available (`ubuntu-latest-8core` if
      exposed, or a self-hosted equivalent per #509's fleet). Distinct job
      names in the CI summary so the failure rate per class is directly
      comparable. Purpose: falsify the "modest runner + hungry CBMC" branch
      quickly, without committing to a permanent runner change.
- [ ] The `push`→main asymmetry in the body (0/4 success vs. 4/3 on PR) is
      addressed head-on: the diagnostic run flips the PR path to the full
      27-harness suite (matching main) on the diagnosis branch, so the
      main/PR asymmetry is confirmed to live in scope-of-work, not in
      trigger-type or runner assignment. If flipping the PR path is too
      costly to keep on, the diagnosis PR reverts it before merge — the
      point is a single deliberate reproduction of the failure mode on a PR
      where the log is readable, not a permanent change.
- [ ] After 15 fresh runs against the instrumented job (mix of push, PR,
      schedule), the follow-up on this issue posts the actual cause with
      the log evidence: **OOM (which harness), action-internal timeout
      (which knob), or hosted-runner reclaim (matching the "runner has
      received a shutdown signal" line rate)**. That comment closes Phase 0
      and unblocks Phase 1 (the remediation AC).
- [ ] `rivet validate` PASS (no artifact edits expected — this is CI-yaml-
      and-diagnostic-only); `cargo fmt` / `cargo clippy --all-targets
      -- -D warnings` clean on any accompanying shell/python instrumentation
      script.
- [ ] Commit trailers: CI-workflow-only, so `Trace: skip` per AGENTS.md is
      acceptable — preferred is `Refs: #839, #299` (299 decoupled kani from
      `needs:[test]` and is the reason this can stay advisory during
      diagnosis) so the instrumentation is linkable from `rivet commits`.
- [ ] **Explicitly out of scope (file as Phase 1 once cause is known):**
      the actual remediation — whether that's "keep kani on a beefier
      runner and re-enable as a gate" (OOM case), "raise the action's
      internal timeout and shrink the harness selection on `push`"
      (timeout case), "explicitly declare kani advisory + move off the PR
      surface" (reclaim case, or a policy call any way); the docs/AGENTS.md
      update pinning kani's gate/advisory status; a decision on whether
      #509's self-hosted pool should own kani going forward.

If instead the diagnostic slice feels like premature investment and the right first move is the advisory-move — accept that the gate is unreliable, mark it explicitly advisory in the workflow name and CI dashboard, and stop letting it cost attention on PRs — the AC is much smaller (a name: change, a docs note, a README.md badge tweak, and a policy line in AGENTS.md) but forecloses ever making kani load-bearing. Recommend Phase 0 first: the data cost is one release cycle, the answer is the input to a durable call.

Adjacent state worth flagging:

• CI has a single point of failure: when the self-hosted runner pool goes offline, every gate queues forever with no fallback and no liveness alert #509 (CI single point of failure — self-hosted runner pool) is the neighbouring surface: kani currently runs on ubuntu-latest, so a fleet outage doesn't affect it, but if diagnosis lands on "needs a bigger runner", CI has a single point of failure: when the self-hosted runner pool goes offline, every gate queues forever with no fallback and no liveness alert #509's fleet-liveness posture becomes the natural home. Sequencing suggestion: pin the cause here first; only then decide whether kani moves onto the self-hosted pool CI has a single point of failure: when the self-hosted runner pool goes offline, every gate queues forever with no fallback and no liveness alert #509 is meant to protect.
• The body cross-links ci: decouple playwright/kani/rocq from needs:[test] to reduce blast radius of rust-cpu queue saturation #299 (decoupled kani from needs:[test], which is why kani being red doesn't block merges today). That posture is exactly why "runs 58% and blocks nothing" is a stable equilibrium that trains readers to ignore the gate — the same "passes and checks nothing" family this tracker keeps surfacing (serve: /api/v1/artifacts silently truncates at limit=1000 (repo has 1017) — no truncation signal in the response #832 / ci: Test job silently falls back to cargo test, producing no JUnit XML and losing retries — three stacked silencers #833 / check verification-evidence is useless as a gate: blind to nested workspaces (false fail) + satisfied by an empty stub (false pass) #807 / Declare cited-source on the verification types (sw/unit/sys-verification) + a native 'named-test-exists' check — make requirement→test evidence drift-checked #556 / rivet verify advances on the existence of evidence, not its sufficiency #838). The remediation Phase (whichever it becomes) is what breaks the equilibrium; the diagnostic Phase just gives it a defensible direction.

Process side-rail: consulted https://pulseengine.eu/blog/ at the start of this run — 200 OK. No post speaks to CI-diagnosis convention or per-issue AC shape; the closest workflow-relevant post is "Where the seams still show" (2026-07-12, the wired-in-CI / demonstrated-once / still-manual maturity lens). Today Kani Proofs is nominally wired-in-CI but functionally advisory-plus-noise — Phase 0 is what tells us whether it can be promoted back to wired, or whether the honest classification is manual and the workflow should stop pretending otherwise.

Not implemented this run — no PR opened; the AC block on the body is the gating input. Once you pin the phase (diagnosis first vs. advisory-move first), the next routine pass can open a focused branch.

---

Generated by Claude Code

[avrabe]

Correction: some of these failures were a real compile error, and I dismissed them

I opened this issue attributing Kani's failures to hosted-runner reclaim, and
I have since merged past a red Kani check on roughly six PRs citing it. At least
part of that was wrong, and the part that was wrong is my own defect.

REQ-309 (#848, merged in #850) added two fields to CoverageEntry. I updated
every struct literal in coverage.rs, export.rs, schema.rs, lifecycle.rs
and validate.rs — and missed rivet-core/src/proofs.rs:216. So Kani was
reporting:

error[E0063]: missing fields `exempt` and `exempt_ids`
              in initializer of `coverage::CoverageEntry`
   --> rivet-core/src/proofs.rs:216:21

Fixed in #865, reported by @avrabe from a PR whose diff does not touch
rivet-core at all.

Why my self-verify could not catch it

proofs.rs is #[cfg(kani)]. That makes it invisible to every gate I run
before pushing:

cargo build              skips it
cargo test --workspace   skips it
clippy --all-targets     skips it

So a green local run said nothing about it, and CI's Kani job was the only thing
that could — which is precisely the check I had decided in advance to discount.

What I actually got wrong

Not "Kani is sometimes infra-flaky" — that part holds, and #865's own Kani run
died on exit 143 with a runner shutdown signal, so both causes are live
concurrently. The error was treating the two as interchangeable without ever
opening a log to tell them apart. A compile error and a runner reclaim look
identical from the checks list. Distinguishing them costs one log read, and I
did that read for #862's fleet-restart investigation but never for Kani itself.

What this issue should track now

The infra half is still real, so I am not closing it. But the ~58% failure rate
quoted in the original description is not a clean measurement — it pooled two
causes, one of which was a hard build break present from #850 onward. Any future
"Kani is red, merge anyway" decision needs the log checked first:

gh api repos/pulseengine/rivet/actions/jobs/$JOB/logs --allow-escape-sequences \
  | grep -E "error\[E[0-9]+\]|shutdown signal|exit code"

error[...] means the proofs do not build and the check is telling the truth.
shutdown signal means the runner went away.

Related

• fix(proofs): Kani proof CoverageEntry init missing exempt/exempt_ids (REQ-309, #848) #865 — the fix
• ci: the self-hosted fleet restarts mid-run, killing all in-flight jobs and reporting them as failures #862 — the self-hosted fleet restarts, the other half of this