The Verification Gate has not produced a single green run in six weeks
60 runs sampled, 2026-07-15 → 2026-08-25:
| conclusion |
count |
| cancelled |
57 |
| failure |
3 |
| success |
0 |
The gate that runs TEST-RULE-SOLVER-DIFFERENTIAL — the artifact whose green run is the no-divergence assertion between Z3 and the certificate-checked ordeal engine — has never been green in the sampled window.
It is timing out, not being superseded
The obvious reading is cancel-in-progress: true killing runs as new pushes land. That is not what is happening: the concurrency group is ${{ github.workflow }}-${{ github.head_ref || github.ref }}, which is per-branch, so separate PRs cannot cancel each other.
Durations of the twelve most recent runs, against timeout-minutes: 30:
30.5 39.2 32.2 31.9 30.4 36.2 41.1 55.5 63.0 102.5 48.0 33.4
Every one exceeds the budget. The floor is 30.4 minutes. The job cannot finish.
The workflow's own comment predicted this — the default filter is narrow because a wider one "would re-run dozens of cargo test invocations and blow the 30-minute job timeout." The filter now matches 23 artifacts and blows it anyway.
The check itself is fine — that is what makes this worth fixing rather than deleting
From run 31727742734, the last one that reached a verdict:
matched 23 artifacts
[RUN ] TEST-RULE-SOLVER-DIFFERENTIAL
[ OK ] TEST-RULE-SOLVER-DIFFERENTIAL
passed: 21
failed: 2
The differential ran and passed. The run was marked failure because two unrelated artifacts failed (loom optimize pipeline smoke, measure_corpus). So the solver cross-check is riding behind 22 other artifacts, and inherits both their runtime and their verdict.
Why nobody noticed
repos/pulseengine/loom/branches/main/protection reports:
{ "required_checks": [], "strict": true }The required-status-checks list is empty, so the Verification Gate is advisory. PRs merge freely regardless — including #352, the v1.4.1 release PR, whose two Verification Gate runs were cancelled at 30.5 and 39.2 minutes. v1.4.1 shipped this morning without this gate ever going green.
That is the same shape as #332: something reports a state it did not establish. #332 was a check that could not go red; this is a check that cannot go green, on a board where nothing reads it.
Suggested shape (not prescriptive)
The cheap fix is to stop coupling the solver differential to everything else:
- A dedicated job for the differential alone —
LOOM_VERIFY_BACKEND=both cargo test --release --lib -p loom-core --features verification -- test_verify_all_rules. It fits inside a small budget because it is one test binary, not 23 artifacts, and it is the one whose green run carries a claim.
- Raise
timeout-minutes for the broad rivet-driven sweep, or split it by tag so each slice fits. A 30-minute budget that the minimum observed run exceeds by 24 seconds is not a budget.
- Then make the differential job required on
main — an advisory gate with a six-week non-green record is indistinguishable from no gate.
Two adjacent notes
- There is a second reason a cadence job would help: the differential only fires when a PR happens to touch loom.
ordeal is exact-pinned, but Z3 arrives through Z3_SYS_Z3_HEADER: /usr/include/z3.h from apt libz3-dev, unpinned, and drifts under the runner image. kiln/kani-verification.yml (weekly) is the shape.
- The scope limit stated in
TEST-RULE-SOLVER-DIFFERENTIAL's own description is worth keeping visible: this is the rule verifier only; the core translation validator has not been migrated. The artifact says so honestly and the release notes should keep doing that.
Measured 2026-08-26. required_checks and durations from the GitHub API; the run log excerpt from the linked run.
The Verification Gate has not produced a single green run in six weeks
60 runs sampled,
2026-07-15 → 2026-08-25:The gate that runs
TEST-RULE-SOLVER-DIFFERENTIAL— the artifact whose green run is the no-divergence assertion between Z3 and the certificate-checked ordeal engine — has never been green in the sampled window.It is timing out, not being superseded
The obvious reading is
cancel-in-progress: truekilling runs as new pushes land. That is not what is happening: the concurrency group is${{ github.workflow }}-${{ github.head_ref || github.ref }}, which is per-branch, so separate PRs cannot cancel each other.Durations of the twelve most recent runs, against
timeout-minutes: 30:Every one exceeds the budget. The floor is 30.4 minutes. The job cannot finish.
The workflow's own comment predicted this — the default filter is narrow because a wider one "would re-run dozens of
cargo testinvocations and blow the 30-minute job timeout." The filter now matches 23 artifacts and blows it anyway.The check itself is fine — that is what makes this worth fixing rather than deleting
From run 31727742734, the last one that reached a verdict:
The differential ran and passed. The run was marked
failurebecause two unrelated artifacts failed (loom optimizepipeline smoke,measure_corpus). So the solver cross-check is riding behind 22 other artifacts, and inherits both their runtime and their verdict.Why nobody noticed
repos/pulseengine/loom/branches/main/protectionreports:{ "required_checks": [], "strict": true }The required-status-checks list is empty, so the Verification Gate is advisory. PRs merge freely regardless — including #352, the v1.4.1 release PR, whose two Verification Gate runs were cancelled at 30.5 and 39.2 minutes. v1.4.1 shipped this morning without this gate ever going green.
That is the same shape as #332: something reports a state it did not establish. #332 was a check that could not go red; this is a check that cannot go green, on a board where nothing reads it.
Suggested shape (not prescriptive)
The cheap fix is to stop coupling the solver differential to everything else:
LOOM_VERIFY_BACKEND=both cargo test --release --lib -p loom-core --features verification -- test_verify_all_rules. It fits inside a small budget because it is one test binary, not 23 artifacts, and it is the one whose green run carries a claim.timeout-minutesfor the broad rivet-driven sweep, or split it by tag so each slice fits. A 30-minute budget that the minimum observed run exceeds by 24 seconds is not a budget.main— an advisory gate with a six-week non-green record is indistinguishable from no gate.Two adjacent notes
ordealis exact-pinned, but Z3 arrives throughZ3_SYS_Z3_HEADER: /usr/include/z3.hfrom aptlibz3-dev, unpinned, and drifts under the runner image.kiln/kani-verification.yml(weekly) is the shape.TEST-RULE-SOLVER-DIFFERENTIAL's own description is worth keeping visible: this is the rule verifier only; the core translation validator has not been migrated. The artifact says so honestly and the release notes should keep doing that.Measured 2026-08-26.
required_checksand durations from the GitHub API; the run log excerpt from the linked run.