Run two verify:quint jobs at once

[0thernet]

Why

The verification job is part of Required and runs everything serially. On main the bun run verify step now takes 19 to 31 minutes of its 50-minute bound (#379 raised the bound as slow-runner headroom). On main's run at 4a89c83 (job 30m41s) the Quint model checks took about 21.5 minutes (fence alone 7.7) and the replay run 6.6 minutes, one process at a time on a 4-vCPU, 16 GB runner. Six open lanes add or deepen models (#380 promotion.qnt alone adds about 7 minutes of checks and 3 of replay on CI), which would push the step past its bound.

Change

verify:quint treats each model's checks (typecheck, simulation, mutant simulation, Apalache, Apalache mutants) as one job and the replay run as a second kind of job, and runs two jobs at once through a new runAtMost helper (QUINT_CONCURRENCY = 2). Two jobs hold at most two 4 GiB Apalache heaps on the 16 GB runner.

Unchanged: every command, bound, seed, timeout, verdict rule, log file, and artifact. The replay run still covers every model's replay test in one bun test process. toolchain.json still lists the models in manifest order; it is now written after the replay run too.

Failure semantics: after a job fails no further job starts, the running jobs finish (each is bounded by its own checker timeout), and the failure of the earliest-listed failed job is rethrown. A failure still fails verify:quint, the step, the job, and Required.

Tests

• scripts/verification-tools.test.ts "concurrent checker jobs": ordered start and the concurrency cap with gated tasks; no start after a failure, waiting for running tasks, and the earliest-listed failure rethrown; invalid limits rejected before any task runs; and a property over random task plans and limits (assertAsyncProperty) checking once-only in-order starts, a peak of exactly min(limit, tasks), no start after a failure, and the rethrown failure.
• Four mutants of runAtMost each fail these tests: ignoring failures (2 tests fail), ignoring the limit (3), rethrowing the first-in-time failure (2), and returning before running tasks finish (3).
• A local end-to-end bun run verify:quint on a manifest narrowed to lock and messaging passed in 1m22s with the replay run and model checks interleaved, and wrote toolchain.json in manifest order; the manifest was restored.
• bun run typecheck and bun run verify:claims (130 pass).

Review focus

This changes how the required verification job runs its checks, so it needs independent review against the prior coverage (AGENTS.md). The job, step, commands, and bounds in .github/workflows/ci.yml are untouched; this PR's own verification run measures the new duration.

Generated with Devin

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated
ghostget	Ready	Preview	Sep 25, 2026 2:28am UTC