fix(ci): pin the Kani version — an upstream release broke every merge - #426
Merged
Merged
Conversation
…#425) The required `Kani gate` went red on main and blocked every merge in the repo. 45 engine legs failing at once. ROOT CAUSE, with the timeline: kani-0.68.0 released 2026-09-16T03:43:14Z first failing CI run 2026-09-16T03:55:44Z <- 12 minutes later last passing CI run 2026-09-15T19:49 <- the v1.138.0 tag commit `model-checking/kani-github-action@v1` has a `kani-version` input that defaults to `latest`. We never set it, so every run installed whatever Kani had most recently published. Upstream shipped 0.68.0 and our required gate fell over twelve minutes later. IT IS NOT THE PROOFS, established rather than assumed. Every failing leg completed in about 11 s, which is far too fast for model checking, and the only change to the tree between the last green run and the first red one was PR #406 — artifacts and release notes, no Rust. Running the same thing locally on 0.67.0 settles it: crates/relay-lc $ cargo kani ** 0 of 75 failed VERIFICATION:- SUCCESSFUL Complete - 9 successfully verified harnesses, 0 failures, 9 total. 0.67.0 is exactly what `latest` resolved to for the whole period the gate was green (it was released 2026-01-16), so this pins the known-good state rather than picking a new one. Moving to 0.68.0 is a deliberate change with its own validation — not something an upstream release gets to do to us at 03:43 on a required gate. THE GENERAL LESSON, which this repo has now paid for twice. An unpinned tool in a REQUIRED gate is an unreviewed dependency on someone else's release schedule. The same class already bit us on the other side: a stale, four-month-old local synth binary silently emitted wrong float code with exit 0. Floating means "whatever, whenever", in both directions. Also worth recording: this was visible for hours as "the Kani gate is red" and read as a proof problem. The 11-second job duration was the tell, and duration is not something anyone looks at when a verification gate goes red. Closes #425. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
avrabe
enabled auto-merge (squash)
September 16, 2026 13:05
This was referenced Sep 16, 2026
avrabe
added a commit
that referenced
this pull request
Sep 16, 2026
…427) (#428) A required status check that does not RUN does not pass by default. It never reports, and the PR stays blocked forever. I promoted `Gazebo SITL (real gz bridge)` to a required context earlier today with its stated precondition met — five consecutive green runs on main, the wasm leg executing 6250 ticks and holding 0.01 m, bit-identical to native. It deadlocked every merge in the repo within minutes. PR #426 sat BLOCKED with ZERO failing checks, because it touched only `.github/workflows/kani.yml` and the path filter meant gazebo never triggered. Removing the context returned it to CLEAN instantly. The precondition I checked was "is this leg meaningful". The one that decides whether a context can be required is "does it report on EVERY pr", and those are different properties. This removes the `pull_request` path filter so the job always runs. Cost: about 7 minutes of runner time per PR, against the only gate in the repo that flies the actually-published wasm component through real physics and compares it to native bit for bit. That is cheap. NOT PROMOTING IT IN THIS COMMIT. The sequence is: land this, observe the job reporting on a PR that touches none of the old filter paths, THEN add the required context. Promoting on the strength of reasoning rather than evidence is exactly what caused the deadlock, and doing it again in the same day would be hard to explain. Worth naming the shape, because this repo now has both halves of it: #417 — a job that is SKIPPED but reports `success` verifies nothing while looking green. #427 — a job that is SKIPPED and reports nothing blocks everything. Same root: a gate whose workflow does not always run. The only shape safe to require is one that always runs and always reports. Refs #427. Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #425. Unblocks #424 and every other open PR.
What happened
The required
Kani gatewent red on main, failing 45 engine legs at once,and blocked every merge in the repo.
kani-0.68.0released upstreammodel-checking/kani-github-action@v1has akani-versioninput thatdefaults to
latest. We never set it. So every run installed whatever Kanihad most recently published, and a required gate fell over twelve minutes after
an upstream release.
It is not the proofs — established, not assumed
Three independent lines:
finish in 11 s.
PR plan(v1.139): the two dark gates, the horizontal hold, and v1.138.0's release notes #406 — artifacts and release notes, no Rust.
The fix
Pin
kani-version: '0.67.0'— exactly whatlatestresolved to for the entireperiod the gate was green (released 2026-01-16). This restores the known-good
state rather than choosing a new one. Moving to 0.68.0 is a deliberate change
with its own validation.
The lesson, which we have now paid for twice
An unpinned tool in a required gate is an unreviewed dependency on someone
else's release schedule. The same class bit us from the other direction days
ago: a stale, four-month-old local
synthbinary silently emitted wrong floatcode with exit 0, and we nearly reported "floats don't lower" because of it.
Floating means "whatever, whenever" — in both directions.
Worth recording separately: this was visible for hours as "the Kani gate is red"
and read as a proof problem. The 11-second job duration was the tell, and
duration is not something anyone looks at when a verification gate goes red.
🤖 Generated with Claude Code
https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG