fix(tests): add gnn_api_url to live_config; wire GPU backends in CI

- live_prover_suite.rs + live_prover_verify.rs: add missing `gnn_api_url:
  None` to the `live_config` ProverConfig literal (cargo check
  --features live-provers was failing with E0063)
- live_prover_suite.rs: add live_gpuverify_version and live_faial_version
  tests (T4, auto-skip when binaries absent)
- live-provers.yml: add tier4-gpu matrix job (gpuverify + faial) running
  quarterly with continue-on-error, provisioning notes and version checks

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/live-provers.yml

@@ -376,3 +376,43 @@ jobs:
           echo "Tier-4 backends (Mizar, Nuprl, PVS, Minlog, Dedukti, Arend, KeY, Prism, UPPAAL,"
           echo "ViPER, NuSMV, Spin, TLC, CBMC, Seahorn, dReal, Boogie, Kissat, Alloy) are"
           echo "retained as mock-only unless a maintainer volunteers a Containerfile."
+
+  # ============================================================================
+  # Tier 4 GPU — quarterly, best-effort / allow-fail.
+  # GPUVerify and Faial require CUDA SDK or OpenCL runtime; provisioning is
+  # deferred to a developer workstation or GPU-capable CI runner.
+  # ============================================================================
+  tier4-gpu:
+    name: T4 / ${{ matrix.backend }}
+    if: github.event_name == 'schedule' && github.event.schedule == '0 6 1 */3 *' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '4' || inputs.tier == 'all'))
+    runs-on: ubuntu-latest
+    continue-on-error: true
+    strategy:
+      fail-fast: false
+      matrix:
+        backend:
+          - gpuverify
+          - faial
+    steps:
+      - name: Checkout
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      - name: Install Rust
+        uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable
+      - name: Cache Cargo
+        uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2
+      - name: Provision ${{ matrix.backend }} (best-effort, CUDA/OpenCL required)
+        continue-on-error: true
+        run: |
+          case "${{ matrix.backend }}" in
+            gpuverify)
+              echo "GPUVerify requires CUDA SDK + .NET; deferred to developer workstation."
+              echo "See: https://github.com/mc-imperial/gpuverify"
+              ;;
+            faial)
+              echo "Faial requires CUDA/OpenCL headers; install via: cargo install faial"
+              echo "See: https://github.com/elliotttate/faial"
+              ;;
+          esac
+      - name: Run live version check (SKIP if binary absent)
+        continue-on-error: true
+        run: cargo test --test live_prover_suite --features live-provers -- --nocapture live_${{ matrix.backend }}_version

tests/live_prover_suite.rs

@@ -49,6 +49,7 @@ fn live_config(executable: &str) -> ProverConfig {
         args: vec![],
         timeout: 30,
         neural_enabled: false,
+        gnn_api_url: None,
     }
 }
 
@@ -350,3 +351,23 @@ async fn live_imandra_version() {
     // licence is available.  Test SKIPs on public CI.
     assert_version_reachable(ProverKind::Imandra, "imandra").await;
 }
+
+// ==========================================================================
+// Tier 4 — quarterly.  GPU verification backends.  Require CUDA SDK or
+// OpenCL runtime; provisioned via Containerfile or developer workstation.
+// Tests SKIP when the binary is absent.
+// ==========================================================================
+
+#[tokio::test]
+async fn live_gpuverify_version() {
+    // GPUVerify targets CUDA/OpenCL kernels via Boogie+Z3.
+    // Install: https://github.com/mc-imperial/gpuverify
+    assert_version_reachable(ProverKind::GPUVerify, "gpuverify").await;
+}
+
+#[tokio::test]
+async fn live_faial_version() {
+    // Faial is a static GPU data-race detector targeting CUDA.
+    // Install: https://github.com/elliotttate/faial (or `cargo install faial`)
+    assert_version_reachable(ProverKind::Faial, "faial-drf").await;
+}

tests/live_prover_verify.rs

@@ -41,6 +41,7 @@ fn live_config(executable: &Path) -> ProverConfig {
         args: vec![],
         timeout: 30,
         neural_enabled: false,
+        gnn_api_url: None,
     }
 }