Skip to content

Trust diffblue/cbmc tap so macOS Kani CI survives Homebrew 6.0+ - #688

Merged
feliperodri merged 1 commit into
model-checking:mainfrom
feliperodri:bump-kani-macos-cbmc-fix
Sep 17, 2026
Merged

feliperodri merged 1 commit into
model-checking:mainfrom
feliperodri:bump-kani-macos-cbmc-fix

Conversation

@feliperodri

Copy link
Copy Markdown
Member

Problem

Homebrew 6.0 started refusing to load formulae from untrusted third-party taps. The pinned Kani's scripts/setup/macos/install_cbmc.sh runs brew tap diffblue/cbmc, which now fails on macos-latest runners, so CBMC never gets installed and every macOS Kani job dies with:

[Errno 2] No such file or directory: 'cbmc'

This is currently red on all macOS jobs (see #685), and the fail-fast cancellation also takes down the ubuntu counterparts.

Fix

Run brew trust diffblue/cbmc 2>/dev/null || true in run-kani.sh right before it invokes the macOS setup script, so the tap is trusted before Kani taps it — regardless of which Kani commit is pinned. The guard makes it a no-op on older Homebrew that lacks brew trust.

This mirrors the upstream Kani fix model-checking/kani#4785, applied at the verify-rust-std layer so it does not require bumping the pinned Kani commit / toolchain.

Testing

Ubuntu path is unchanged; macOS CI on this PR exercises the fix.

Homebrew 6.0 began refusing to load formulae from untrusted third-party
taps, so the pinned Kani's scripts/setup/macos/install_cbmc.sh fails at
`brew tap diffblue/cbmc`, leaving CBMC uninstalled and every macOS Kani
job broken (e.g. `[Errno 2] No such file or directory: 'cbmc'`).

Run `brew trust diffblue/cbmc` before invoking the macOS setup script so
CBMC installs regardless of the Kani commit currently pinned. Mirrors the
upstream fix model-checking/kani#4785 without requiring a toolchain bump.

Guarded with `2>/dev/null || true` for older Homebrew lacking `brew trust`.
@feliperodri
feliperodri requested a review from a team as a code owner September 17, 2026 02:19
@feliperodri feliperodri added the Maintenance Maintenance related issues for the challange label Sep 17, 2026
@feliperodri
feliperodri added this pull request to the merge queue Sep 17, 2026
Merged via the queue into model-checking:main with commit 82ab358 Sep 17, 2026
30 checks passed
@feliperodri
feliperodri deleted the bump-kani-macos-cbmc-fix branch September 17, 2026 18:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Maintenance Maintenance related issues for the challange

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants