diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index a61cd651..a7e30030 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -1537,8 +1537,42 @@ jobs:
         run: cargo test -p synth-cli --features verify --test fact_spec_div_494
       - name: Run verify rule-inventory non-vacuity gate (#935 decline denominator)
         run: cargo test -p synth-cli --features verify --test verify_report_935
+      # #1000 (RQ-58-SHIPVERIFY): the capable half of the banner-ordering gate
+      # — a verify-capable binary must still print the strategy banner AND end
+      # in a real verdict. (The missing-capability half runs in the plain
+      # workspace test job, where the test binary is built without `verify`.)
+      - name: Run verify banner/verdict gate (#1000, verify half)
+        run: cargo test -p synth-cli --features verify --test verify_banner_1000
+      # #1000 red leg — keep the released-artifact smoke gate falsifiable on
+      # every push, not just at authoring time: against a binary built WITHOUT
+      # the `verify` feature, scripts/release_verify_smoke.sh (the script
+      # release.yml runs against each packaged tarball) must FAIL, and fail
+      # for exactly the capability reason. A gate whose red direction is not
+      # exercised goes vacuous silently — this repo has shipped that class.
+      - name: Build synth WITHOUT verify (#1000 red-leg binary)
+        run: cargo build -p synth-cli
+      - name: Red leg — release smoke gate must fail on a verify-less binary
+        run: |
+          set -euo pipefail
+          if bash scripts/release_verify_smoke.sh target/debug/synth \
+              > /tmp/smoke_red.log 2>&1; then
+            echo "VACUOUS GATE: release_verify_smoke.sh passed against a binary built without the verify feature" >&2
+            cat /tmp/smoke_red.log >&2
+            exit 1
+          fi
+          grep -q 'built without the `verify` feature' /tmp/smoke_red.log || {
+            echo "release_verify_smoke.sh failed for the WRONG reason:" >&2
+            cat /tmp/smoke_red.log >&2
+            exit 1
+          }
+          echo "red leg OK: smoke gate fails with the capability error on a verify-less binary"
       - name: Build synth (verify feature)
         run: cargo build -p synth-cli --features verify
+      # #1000 green leg — the same script release.yml runs against the
+      # packaged tarballs, here against the freshly built verify binary so a
+      # pre-tag push catches script/CLI drift instead of the release run.
+      - name: Green leg — release smoke gate passes on the verify binary
+        run: bash scripts/release_verify_smoke.sh target/debug/synth
       - uses: actions/setup-python@v7
         with:
           python-version: "3.x"
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index b29190b9..d36283bd 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -30,13 +30,17 @@ env:
 
 jobs:
   # ── Cross-platform binary builds ──────────────────────────────────────
-  # synth-cli builds with `--features riscv` only (the workspace default).
-  # The `verify` feature is intentionally NOT enabled here. Historically it
-  # pulled z3-sys (vendored C++ Z3 build — slow, network-hungry); since #553
-  # it is pure Rust (ordeal engine), so enabling it is now feasible but is a
-  # deliberate follow-up decision, not a build constraint. The CLI degrades
-  # gracefully without it (`synth verify` fails loudly with "rebuild with
-  # --features verify").
+  # synth-cli builds with the workspace default (`riscv`) PLUS `verify`
+  # (#1000, RQ-58-SHIPVERIFY): every released tarball can run `synth verify`
+  # to a real verdict. Historically `verify` pulled z3-sys (vendored C++ Z3
+  # build — slow, network-hungry); since #553 it is pure Rust (ordeal
+  # engine, re-measured for v0.58: `cargo tree -p synth-cli --features
+  # verify` has 0 z3 nodes — Z3 remains a separate `synth-verify/z3-solver`
+  # opt-in that never ships here). The smoke step below is the non-vacuity
+  # gate: it extracts the just-packaged tarball and asserts `synth verify`
+  # reaches a verdict, so dropping this feature flag reds the release run
+  # instead of silently regressing the artifact to help-text-only
+  # (the 0.55.0/0.57.0 state issue #1000 reported).
   build-binaries:
     name: Build ${{ matrix.target }}
     runs-on: ${{ matrix.os }}
@@ -79,11 +83,11 @@ jobs:
 
       - name: Build synth (native)
         if: ${{ !matrix.cross }}
-        run: cargo build --release --target ${{ matrix.target }} -p synth-cli
+        run: cargo build --release --target ${{ matrix.target }} -p synth-cli --features verify
 
       - name: Build synth (cross)
         if: matrix.cross
-        run: cross build --release --target ${{ matrix.target }} -p synth-cli
+        run: cross build --release --target ${{ matrix.target }} -p synth-cli --features verify
 
       - name: Strip binary
         if: ${{ !matrix.cross }}
@@ -107,6 +111,38 @@ jobs:
           tar -czf "$ARCHIVE" -C staging .
           echo "ARCHIVE=$ARCHIVE" >> "$GITHUB_ENV"
 
+      # ── #1000 non-vacuity gate: the TARBALL can `synth verify` ──────────
+      # Extracts the archive packaged above (the artifact a user downloads,
+      # not the loose build output) and asserts `synth verify` runs to a
+      # REAL verdict on a module the same binary just compiled — exit 0,
+      # the verdict line, and a synth-verify-v1 report with >= 1 verified /
+      # 0 failed rule kinds. Red direction proven at authoring and re-proven
+      # on every push by the fact-spec-oracle CI job's red leg: against a
+      # binary built without `--features verify` the script fails with the
+      # capability error. Without this step, "we ship the feature" regresses
+      # silently to "we ship the help text" — the exact #1000 class.
+      #
+      # Execution per target: linux-x86_64 + both macOS tarballs run natively
+      # (x86_64-apple-darwin under Rosetta 2 on the arm64 macos-14 runner);
+      # the cross-built aarch64-linux tarball runs under qemu-user against
+      # the gcc-aarch64-linux-gnu sysroot — all four tarballs are EXECUTED,
+      # none is exempt.
+      - name: Install qemu-user + aarch64 sysroot (cross smoke)
+        if: matrix.cross
+        run: |
+          set -euo pipefail
+          sudo apt-get update
+          sudo apt-get install -y qemu-user gcc-aarch64-linux-gnu
+
+      - name: Smoke-test the packaged tarball runs `synth verify`
+        env:
+          SYNTH_RUNNER: ${{ matrix.cross && 'qemu-aarch64 -L /usr/aarch64-linux-gnu' || '' }}
+        run: |
+          set -euo pipefail
+          mkdir -p smoke-extract
+          tar -xzf "$ARCHIVE" -C smoke-extract
+          bash scripts/release_verify_smoke.sh smoke-extract/synth
+
       - uses: actions/upload-artifact@v7
         with:
           name: binary-${{ matrix.target }}
diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs
index 7cac177a..6ff0a6b4 100644
--- a/crates/synth-cli/src/main.rs
+++ b/crates/synth-cli/src/main.rs
@@ -572,8 +572,9 @@ enum Commands {
     /// List available compilation backends and their status
     Backends,
 
-    /// Verify compilation correctness via Z3 — requires a build with
-    /// `--features verify` (e.g., synth verify input.wat output.elf)
+    /// Verify compilation correctness via SMT translation validation
+    /// (pure-Rust ordeal engine) — requires the `verify` feature
+    /// (e.g., synth verify input.wat output.elf)
     Verify {
         /// Input WASM or WAT file (source)
         #[arg(value_name = "WASM")]
@@ -7174,6 +7175,31 @@ fn verify_command(
 
     let caps = backend.capabilities();
 
+    // #1000: capability check BEFORE the banner. This used to live after the
+    // four `Translation validation:` lines below, so a binary built without
+    // the `verify` feature printed `Strategy: Per-rule SMT verification
+    // (ASIL D path)` and only THEN discovered it could not verify — a
+    // log-scraper grepping for the strategy line would find it in a run that
+    // verified nothing. The exit code was already correct (1, issue #124);
+    // now the output is too: a binary that cannot verify prints nothing
+    // verification-shaped before failing.
+    #[cfg(not(feature = "verify"))]
+    if caps.supports_rule_verification {
+        // This binary was built without the `verify` feature, so no SMT
+        // translation validation can run. Returning Ok here would make
+        // `synth verify` exit success-shaped while doing nothing — a
+        // script or CI step gating on `synth verify` would silently
+        // believe the binary was validated (issue #124). Fail loudly
+        // with a non-zero exit instead.
+        anyhow::bail!(
+            "this `synth` binary was built without the `verify` feature — \
+             SMT translation validation is unavailable.\n  \
+             Rebuild with verification support:\n    \
+             cargo build --features verify\n  \
+             (or `cargo install --path crates/synth-cli --features verify`)"
+        );
+    }
+
     println!("Translation validation:");
     println!("  Source: {}", wasm_input.display());
     println!("  Binary: {}", elf_input.display());
@@ -7329,23 +7355,6 @@ fn verify_command(
                 }
             }
         }
-
-        #[cfg(not(feature = "verify"))]
-        {
-            // This binary was built without the `verify` feature, so no SMT
-            // translation validation can run. Returning Ok here would make
-            // `synth verify` exit success-shaped while doing nothing — a
-            // script or CI step gating on `synth verify` would silently
-            // believe the binary was validated (issue #124). Fail loudly
-            // with a non-zero exit instead.
-            anyhow::bail!(
-                "this `synth` binary was built without the `verify` feature — \
-                 SMT translation validation is unavailable.\n  \
-                 Rebuild with verification support:\n    \
-                 cargo build --features verify\n  \
-                 (or `cargo install --path crates/synth-cli --features verify`)"
-            );
-        }
     } else if caps.supports_binary_verification {
         println!("  Strategy: Binary-level translation validation (ASIL B path)");
         println!("\n  Binary verification not yet implemented.");
diff --git a/crates/synth-cli/tests/verify_banner_1000.rs b/crates/synth-cli/tests/verify_banner_1000.rs
new file mode 100644
index 00000000..4e29b835
--- /dev/null
+++ b/crates/synth-cli/tests/verify_banner_1000.rs
@@ -0,0 +1,143 @@
+//! #1000 (RQ-58-SHIPVERIFY) — `synth verify` capability check runs BEFORE the
+//! banner, and a verify-capable binary reports a real verdict.
+//!
+//! Two halves, selected by how the test binary was built (deliberately NO
+//! `required-features`, so the plain workspace test run exercises the
+//! missing-capability half):
+//!
+//! - WITHOUT `verify` (the plain `cargo test --workspace` build): `synth
+//!   verify` must fail (exit != 0) WITHOUT printing any of the
+//!   `Translation validation:` banner lines — in particular not
+//!   `Strategy: Per-rule SMT verification (ASIL D path)`. Before #1000 the
+//!   banner printed first and the capability check ran after it, so a
+//!   log-scraper grepping for the ASIL-D strategy line found it in a run
+//!   that verified nothing (the exit code was already correct, #124).
+//!   RED-FIRST: under the pre-#1000 ordering this half fails.
+//!
+//! - WITH `verify` (`cargo test -p synth-cli --features verify --test
+//!   verify_banner_1000`, wired into the fact-spec-oracle CI job): the
+//!   banner including the strategy line must still print, and the run must
+//!   end in a REAL verdict on a module synth itself just compiled — not the
+//!   capability-missing error. This is the in-tree twin of
+//!   `scripts/release_verify_smoke.sh`, the released-artifact gate release.yml
+//!   runs against the packaged tarballs.
+
+use std::process::Command;
+
+fn synth() -> &'static str {
+    env!("CARGO_BIN_EXE_synth")
+}
+
+/// Small module with an exported function whose ops are all on the verified
+/// ARM path (and/add) — the same shape the release smoke script compiles.
+const FIXTURE_WAT: &str = r#"(module
+  (func (export "mix") (param i32 i32) (result i32)
+    local.get 0
+    i32.const 255
+    i32.and
+    local.get 1
+    i32.add))
+"#;
+
+/// Compile the fixture with the binary under test; returns (wat, elf) paths.
+fn compile_fixture(tag: &str) -> (std::path::PathBuf, std::path::PathBuf, std::path::PathBuf) {
+    let dir = std::env::temp_dir().join(format!(
+        "synth_verify_banner_1000_{}_{}",
+        tag,
+        std::process::id()
+    ));
+    std::fs::create_dir_all(&dir).expect("create temp dir");
+    let wat = dir.join("mix.wat");
+    let elf = dir.join("mix.elf");
+    std::fs::write(&wat, FIXTURE_WAT).expect("write fixture wat");
+    let compile = Command::new(synth())
+        .args([
+            "compile",
+            wat.to_str().unwrap(),
+            "-o",
+            elf.to_str().unwrap(),
+            "--all-exports",
+        ])
+        .output()
+        .expect("run synth compile");
+    assert!(
+        compile.status.success(),
+        "fixture compile failed:\n{}\n{}",
+        String::from_utf8_lossy(&compile.stdout),
+        String::from_utf8_lossy(&compile.stderr)
+    );
+    (dir, wat, elf)
+}
+
+fn run_verify(wat: &std::path::Path, elf: &std::path::Path) -> std::process::Output {
+    Command::new(synth())
+        .args(["verify", wat.to_str().unwrap(), elf.to_str().unwrap()])
+        .output()
+        .expect("run synth verify")
+}
+
+/// The missing-capability half: fail loudly BEFORE anything
+/// verification-shaped is printed.
+#[cfg(not(feature = "verify"))]
+#[test]
+fn verify_without_feature_fails_before_banner() {
+    let (dir, wat, elf) = compile_fixture("nofeat");
+    let out = run_verify(&wat, &elf);
+    let stdout = String::from_utf8_lossy(&out.stdout);
+    let stderr = String::from_utf8_lossy(&out.stderr);
+
+    // #124 contract, unchanged: non-zero exit, loud capability error.
+    assert!(
+        !out.status.success(),
+        "`synth verify` must fail on a build without the `verify` feature\nstdout:\n{stdout}"
+    );
+    assert!(
+        stderr.contains("built without the `verify` feature"),
+        "capability error must name the missing feature\nstderr:\n{stderr}"
+    );
+
+    // #1000 contract, new: the check runs BEFORE the banner, so none of the
+    // four `Translation validation:` lines — above all the ASIL-D strategy
+    // line — may appear in a run that verified nothing.
+    assert!(
+        !stdout.contains("Strategy: Per-rule SMT verification"),
+        "ASIL-D strategy line printed by a binary that cannot verify:\n{stdout}"
+    );
+    assert!(
+        !stdout.contains("Translation validation:"),
+        "verification banner printed by a binary that cannot verify:\n{stdout}"
+    );
+
+    let _ = std::fs::remove_dir_all(&dir);
+}
+
+/// The capable half: banner still prints, and the run ends in a real verdict.
+#[cfg(feature = "verify")]
+#[test]
+fn verify_with_feature_reports_real_verdict() {
+    let (dir, wat, elf) = compile_fixture("feat");
+    let out = run_verify(&wat, &elf);
+    let stdout = String::from_utf8_lossy(&out.stdout);
+    let stderr = String::from_utf8_lossy(&out.stderr);
+
+    assert!(
+        out.status.success(),
+        "`synth verify` must succeed on a verify-capable build\nstdout:\n{stdout}\nstderr:\n{stderr}"
+    );
+    // The #1000 reorder must NOT cost the capable binary its banner.
+    assert!(
+        stdout.contains("Strategy: Per-rule SMT verification (ASIL D path)"),
+        "strategy banner missing on a verify-capable build:\n{stdout}"
+    );
+    // A real verdict, not the capability-missing error.
+    assert!(
+        stdout.contains("All functions verified successfully."),
+        "expected a real verification verdict:\n{stdout}"
+    );
+    assert!(
+        !stderr.contains("built without the `verify` feature"),
+        "capability error on a build that HAS the feature:\n{stderr}"
+    );
+
+    let _ = std::fs::remove_dir_all(&dir);
+}
diff --git a/scripts/release_verify_smoke.sh b/scripts/release_verify_smoke.sh
new file mode 100644
index 00000000..545a6b55
--- /dev/null
+++ b/scripts/release_verify_smoke.sh
@@ -0,0 +1,120 @@
+#!/usr/bin/env bash
+# #1000 (RQ-58-SHIPVERIFY) — released-artifact non-vacuity gate for `synth verify`.
+#
+# `synth verify` existed in the tree and in --help for many releases while NO
+# obtainable artifact carried the `verify` feature (confirmed on 0.55.0 and
+# 0.57.0 — every platform tarball failed with the capability error). This
+# script is the gate that keeps "we ship the feature" from silently regressing
+# back to "we ship the help text": it takes a synth BINARY (in release.yml, the
+# one extracted from the just-packaged tarball — the artifact itself, not a dev
+# build), compiles a module with it, runs `synth verify` on that module, and
+# asserts a REAL verdict:
+#
+#   * exit 0,
+#   * the human verdict line ("All functions verified successfully."),
+#   * a machine-readable report (--emit-verify-report) whose summary proves
+#     >= 1 rule kind was actually verified and 0 failed,
+#   * and the absence of the capability-missing error.
+#
+# RED DIRECTION (what makes this gate non-vacuous): against a binary built
+# WITHOUT `--features verify` the verify step exits 1 with "built without the
+# `verify` feature" and this script FAILS. The fact-spec-oracle CI job runs
+# that red leg on every push (build without the feature, assert this script
+# fails for exactly that reason), so the gate's ability to go red is itself
+# CI-pinned — this repo has shipped gates that could not fail.
+#
+# Usage:
+#   scripts/release_verify_smoke.sh <path-to-synth-binary>
+#
+# Env:
+#   SYNTH_RUNNER — optional command prefix used to execute the binary, for
+#     tarballs the host cannot run natively (release.yml sets
+#     `qemu-aarch64 -L /usr/aarch64-linux-gnu` for the aarch64-linux tarball).
+set -euo pipefail
+
+if [ $# -ne 1 ]; then
+  echo "usage: $0 <path-to-synth-binary>" >&2
+  exit 2
+fi
+SYNTH=$1
+test -x "$SYNTH" || { echo "error: '$SYNTH' is not an executable file" >&2; exit 2; }
+
+# Intentionally unquoted: SYNTH_RUNNER is a command PREFIX and must word-split
+# (bash word-splits unquoted expansions; this script is bash via its shebang).
+RUNNER=${SYNTH_RUNNER:-}
+run_synth() {
+  # shellcheck disable=SC2086
+  $RUNNER "$SYNTH" "$@"
+}
+
+TMP=$(mktemp -d)
+trap 'rm -rf "$TMP"' EXIT
+
+# Same fixture shape as tests/verify_banner_1000.rs: exported function whose
+# ops (and/add) are on the verified ARM rule path.
+cat > "$TMP/mix.wat" <<'EOF'
+(module
+  (func (export "mix") (param i32 i32) (result i32)
+    local.get 0
+    i32.const 255
+    i32.and
+    local.get 1
+    i32.add))
+EOF
+
+echo "== release_verify_smoke: $SYNTH ${RUNNER:+(runner: $RUNNER)}"
+run_synth --version
+
+# 1. The artifact must be able to COMPILE the module it is about to verify.
+#    No pipes anywhere below: `cmd | tail` has produced false PASSes in this
+#    repo twice — capture to a file, check rc, then read the file.
+if ! run_synth compile "$TMP/mix.wat" -o "$TMP/mix.elf" --all-exports \
+    > "$TMP/compile.log" 2>&1; then
+  echo "FAIL: synth compile failed" >&2
+  cat "$TMP/compile.log" >&2
+  exit 1
+fi
+
+# 2. The verdict, not the help text: `synth verify` must run to a verdict.
+if ! run_synth verify "$TMP/mix.wat" "$TMP/mix.elf" \
+    --emit-verify-report "$TMP/report.json" \
+    > "$TMP/verify.log" 2>&1; then
+  echo "FAIL: synth verify exited non-zero — this artifact cannot verify" >&2
+  cat "$TMP/verify.log" >&2
+  exit 1
+fi
+
+if grep -q 'built without the `verify` feature' "$TMP/verify.log"; then
+  echo "FAIL: capability-missing error in a run that exited 0 (should be unreachable)" >&2
+  cat "$TMP/verify.log" >&2
+  exit 1
+fi
+
+if ! grep -q 'All functions verified successfully\.' "$TMP/verify.log"; then
+  echo "FAIL: no verification verdict in output" >&2
+  cat "$TMP/verify.log" >&2
+  exit 1
+fi
+
+# 3. Machine-readable verdict: the synth-verify-v1 summary must show real
+#    verified rule kinds and zero failures — a grep for a sentence can rot,
+#    counts cannot.
+if ! python3 - "$TMP/report.json" <<'PY'
+import json, sys
+with open(sys.argv[1]) as f:
+    report = json.load(f)
+assert report.get("schema") == "synth-verify-v1", f"unexpected schema: {report.get('schema')}"
+s = report["summary"]
+assert s["verified"] >= 1, f"no rule kind was actually verified: {s}"
+assert s["failed"] == 0, f"verification failures in the smoke fixture: {s}"
+print(f"verdict: {s['verified']} verified / {s['failed']} failed / "
+      f"{s['unknown']} unknown / {s['declined']} declined "
+      f"across {s['applied_rule_kinds']} applied rule kinds")
+PY
+then
+  echo "FAIL: verify report did not carry a real verdict" >&2
+  cat "$TMP/verify.log" >&2
+  exit 1
+fi
+
+echo "PASS: released artifact runs 'synth verify' to a real verdict"