plan(v0.58): add RQ-58-SHIPVERIFY (#1000) — we ship a verifier nobody can run

[avrabe]

Adds RQ-58-SHIPVERIFY for #1000, and corrects the stale README sentence that kept the issue's escape hatch alive.

The problem

synth verify exists in the tree and in --help, and fails closed with an exemplary message — but it is in no artifact a user can obtain. The reporter confirmed it on the layer build (0.55.0) and the current release (0.57.0), whose four platform tarballs all lack the feature.

For a compiler whose entire argument is verified code generation, the ASIL-D translation-validation path being unobtainable is the gap worth closing first. It is also uncomfortably on-theme for v0.58: we ship a verifier nobody can run.

The escape hatch is dead — measured, not assumed

#1000 offers "or, if the Z3 dependency makes that undesirable for the default artifact, publish a variant". There is no Z3 dependency:

build	z3 nodes
cargo tree -p synth-cli --features verify	0
... --features verify,synth-verify/z3-solver	2

verify = ["synth-verify"] and nothing more. z3-solver = ["z3"] is a separate opt-in with optional = true, and even enabled it links the system libz3 rather than bundling it (#553). Ordeal (pure Rust QF_BV) has been the default engine since v0.27.0.

So shipping --features verify costs no Z3, no libz3, no C++ toolchain — a release-workflow change, not a trade-off.

README:98 is the other half of the finding

It said the CLI verify feature "currently also enables the feature-gated Z3 differential oracle (statically linked)". False since v0.27.0 — and precisely the sentence that would make a maintainer accept the escape hatch and not ship the feature.

Prose that was true once, quietly stopped being, and stayed load-bearing on a release decision. Same class the v0.57 cold review kept surfacing; found this time by a user questioning a stale premise. Corrected here.

Scope, with the weight in the middle

1. Build the released binaries (four tarballs + npm) with --features verify.
2. A non-vacuity gate — a released-artifact smoke test that actually runs synth verify on a freshly compiled module and asserts a verdict, not the capability-missing error. Red-first against a binary built without the feature. Without it, "we shipped the feature" regresses silently to "we shipped the help text".
3. Move the capability check ahead of the banner — today Strategy: Per-rule SMT verification (ASIL D path) prints before the tool discovers it cannot verify, so a log-scraper finds the ASIL-D line in a run that verified nothing. Exit code is already correct.

Out of scope, named: #1000's synthesize-vs-compile overlap, --format json, help-line width.

Also re-grades RQ-58-MIRRORS (#993) and RQ-58-SELECT973 (#992) → implemented; both merged and the ledger had not caught up.

Gates

rivet 50 errors before and after (unchanged); warnings +2, the standard pair every artifact carries. claim_check 49/49.

Refs #1000, #242

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!