@@ -116,7 +116,7 @@ The lane targets a Windows host with Visual Studio Build Tools and rustup.
 | Visual C++ ARM64 tools | `vswhere -latest -products * -requires Microsoft.VisualStudio.Component.VC.Tools.ARM64 -property installationPath` | Required for native ARM64 check, build, and tests and for x64-to-ARM64 check/build. Tests always require a native runner. |
 | Visual C++ ARM64 Spectre-mitigated libraries | `vswhere -latest -products * -requires Microsoft.VisualStudio.Component.VC.Runtimes.ARM64.Spectre -property installationPath` | Required by `regorus` through `msvc_spectre_libs`; the build fails when the selected MSVC toolset lacks `lib\spectre\arm64`. |
 | Visual C++ Clang tools | `vswhere -latest -products * -requires Microsoft.VisualStudio.Component.VC.Llvm.Clang -property installationPath` | Provides host-native `libclang.dll` for `bindgen` and `clang-cl.exe` for ARM64 crypto dependencies such as `aws-lc-sys`. On ARM64, the wrapper uses `VC\Tools\Llvm\Arm64\bin`. |
-| Visual C++ CMake tools | `vswhere -latest -products * -requires Microsoft.VisualStudio.Component.VC.CMake.Project -property installationPath` | Provides CMake and Ninja for bundled Z3 and other native dependencies. The x64-to-ARM64 path adds Ninja to `PATH`; Z3 uses MSVC's Visual Studio generator. |
+| Visual C++ CMake tools | `vswhere -latest -products * -requires Microsoft.VisualStudio.Component.VC.CMake.Project -property installationPath` | Provides CMake and Ninja for native dependencies. The x64-to-ARM64 path adds Ninja to `PATH`; Z3 uses an architecture-specific prebuilt release. |
 | Windows SDK | `where.exe rc.exe` from a Developer PowerShell | Install an SDK containing target libraries and ARM64 tools. |
 | Rust via rustup | `rustc --version` | Add each target being validated: `x86_64-pc-windows-msvc` and/or `aarch64-pc-windows-msvc`. The wrapper also adds the selected target. |
 | mise | `mise --version` | Used as a task runner only. |
@@ -136,6 +136,8 @@ from this skill.
 | `CARGO_TARGET_DIR` | `target` under repo root | Override Cargo output location. Use a short absolute path when x64-to-ARM64 builds approach Windows path-length limits. |
 | `Z3_LIBRARY_PATH_OVERRIDE` | unset | Directory containing an x64 system `libz3.lib`; not valid for ARM64. |
 | `Z3_SYS_Z3_HEADER` | unset | Full `z3.h` path required with a system Z3 library. |
+| `Z3_SYS_Z3_VERSION` | `4.16.0` | Pinned official prebuilt Z3 release selected by the wrapper. |
+| `READ_ONLY_GITHUB_TOKEN` | unset | Optional token for the Z3 release lookup; GitHub Actions supplies `github.token`. |
 | `RUSTC_WRAPPER` | inherited | The wrapper resolves an available command to an absolute path. If it is unavailable, the wrapper warns and continues without compiler caching. |
 
 Legacy fork variables such as `OPENSHELL_UPSTREAM`,
@@ -216,8 +218,7 @@ jobs in the current mirror push run, or push a new mirrored commit. The binaries
 The ARM64 check/build steps in this x64-host contract are cross-builds. The
 wrapper discovers and adds host-native LLVM and Ninja to `PATH`, requires the
 ARM64 compiler and Spectre-mitigated libraries, lets ARM64 crypto crates select
-`clang-cl`, and builds bundled Z3 with native MSVC `cl.exe` and the Visual
-Studio generator.
+`clang-cl`, and downloads the official prebuilt ARM64 Z3 static library.
 
 On ARM64 hosts, validate the native ARM64 check, build, and test path. The
 wrapper rejects test targets that do not match the host architecture, so x64
@@ -328,12 +329,13 @@ Useful log files:
 | `test-x86_64-pc-windows-msvc-mxc-real.log` | Native x64 real-MXC integration output. |
 | `test-aarch64-pc-windows-msvc-mxc-real.log` | Native ARM64 real-MXC integration output. |
 
-The first check builds bundled Z3 from source through `z3-sys`. Cargo stores the
-native build output in its target tree, so the Windows target cache reuses it.
-The resulting release executables do not require `libz3.dll`. The artifact
-report computes SHA256 through .NET directly and does not rely on the
-`Get-FileHash` module being available inside the mise-launched Windows
-PowerShell process.
+The first check downloads the pinned official Z3 archive for the target
+architecture through `z3-sys`. GitHub Actions authenticates the lookup with its
+read-only workflow token; local users can set `READ_ONLY_GITHUB_TOKEN` if an
+unauthenticated lookup is rate-limited. Cargo stores the extracted library in
+its target tree, so the Windows target cache reuses it. The artifact report
+computes SHA256 through .NET directly and does not rely on the `Get-FileHash`
+module being available inside the mise-launched Windows PowerShell process.
 
 ## Common Fix Patterns
 
 
@@ -68,11 +68,11 @@ file.
 For ARM64, verify the Visual Studio instance contains the ARM64 MSVC tools,
 ARM64 Spectre-mitigated libraries, Clang tools, CMake tools, and a Windows SDK.
 Clang supplies host-native `libclang.dll` for `bindgen` and `clang-cl.exe` for
-ARM64 crypto dependencies such as `aws-lc-sys`. Native builds use the normal
-bundled-Z3 CMake path. An x64-to-ARM64 check/build discovers and adds
-host-native Ninja to `PATH`, builds bundled Z3 with native MSVC `cl.exe` and
-the Visual Studio generator, and lets the crypto crates select `clang-cl`. Use
-a short `CARGO_TARGET_DIR` if Windows path-length limits are reached.
+ARM64 crypto dependencies such as `aws-lc-sys`. Native and x64-to-ARM64 builds
+use the official prebuilt Z3 4.16.0 static library for the target architecture.
+An x64-to-ARM64 check/build discovers and adds host-native Ninja to `PATH`,
+while the crypto crates select `clang-cl`. Use a short `CARGO_TARGET_DIR` if
+Windows path-length limits are reached.
 
 ## Unsupported Driver Rules
 
 
@@ -56,6 +56,7 @@ jobs:
             rust_target: aarch64-pc-windows-msvc
     runs-on: ${{ matrix.runner }}
     env:
+      READ_ONLY_GITHUB_TOKEN: ${{ github.token }}
       SCCACHE_GHA_ENABLED: "true"
       SCCACHE_GHA_VERSION: windows-msvc-${{ matrix.arch }}
       SCCACHE_CLIENT_SIDE: "1"
@@ -121,6 +122,7 @@ jobs:
             rust_target: aarch64-pc-windows-msvc
     runs-on: ${{ matrix.runner }}
     env:
+      READ_ONLY_GITHUB_TOKEN: ${{ github.token }}
       SCCACHE_GHA_ENABLED: "true"
       SCCACHE_GHA_VERSION: windows-msvc-${{ matrix.arch }}
       SCCACHE_CLIENT_SIDE: "1"
@@ -178,6 +180,7 @@ jobs:
             rust_target: aarch64-pc-windows-msvc
     runs-on: ${{ matrix.runner }}
     env:
+      READ_ONLY_GITHUB_TOKEN: ${{ github.token }}
       SCCACHE_GHA_ENABLED: "true"
       SCCACHE_GHA_VERSION: windows-msvc-${{ matrix.arch }}
       SCCACHE_CLIENT_SIDE: "1"
 
@@ -340,14 +340,19 @@ cargo build -p openshell-prover --features bundled-z3
 
 For x86-64 and ARM64 Windows MSVC builds, use one of these Z3 paths:
 
-- Bundled Z3 (the default for `windows:*` tasks): `z3-sys` builds Z3 from
-  source and links it into the OpenShell binaries. This keeps the release
-  executables independent of `libz3.dll` when they are copied to another host.
+- Prebuilt Z3 (the default for `windows:*` tasks): `z3-sys` downloads the
+  pinned Z3 4.16.0 GitHub release for the target architecture on the first
+  build. Cargo reuses the extracted archive from its target directory. Windows
+  CI authenticates the GitHub API request with `READ_ONLY_GITHUB_TOKEN` and
+  preserves the archive in the architecture-specific Cargo target cache. For
+  cold local builds, you may set `READ_ONLY_GITHUB_TOKEN` to avoid anonymous
+  GitHub API rate limits.
 - System Z3: point `Z3_LIBRARY_PATH_OVERRIDE` at the directory containing the
-  target-compatible MSVC Z3 library and `Z3_SYS_Z3_HEADER` at the full path to
-  `z3.h`. The `windows:*` tasks use this path automatically when
-  `Z3_LIBRARY_PATH_OVERRIDE` is set. Deploy the matching `libz3.dll` with any
-  binaries built against a dynamic system Z3.
+  target-compatible MSVC Z3 library and `Z3_SYS_Z3_HEADER` at the full path to `z3.h`.
+  The `windows:*` tasks use this path automatically when `Z3_LIBRARY_PATH_OVERRIDE`
+  is set.
+- Bundled Z3: for direct Cargo builds, pass `--features bundled-z3` so `z3-sys`
+  builds Z3 from source.
 
 `openshell-prover` itself has no `bindgen`/`libclang` dependency, so building
 just this crate does not require `LIBCLANG_PATH`:
@@ -360,17 +365,17 @@ cargo build -p openshell-prover --target x86_64-pc-windows-msvc --features bundl
 
 To build the full set of Windows binaries, including `openshell-gateway.exe`
 and `openshell.exe`, use the `windows:build:x64` mise task instead of a
-single-crate `cargo build`. It builds Z3 from source (bundled) by default. A full
-build also compiles crates that use `bindgen` (e.g. the MXC driver on Windows),
-so it requires `libclang.dll`; if LLVM is not on the default search path, set
-`LIBCLANG_PATH` to the directory containing `libclang.dll`:
+single-crate `cargo build`. It downloads the pinned prebuilt Z3 release by default. A
+full build also compiles crates that use `bindgen` (e.g. the MXC driver on
+Windows), so it requires `libclang.dll`; if LLVM is not on the default search
+path, set `LIBCLANG_PATH` to the directory containing `libclang.dll`:
 
 ```powershell
 $env:LIBCLANG_PATH='C:\Program Files\Microsoft Visual Studio\2022\<Edition>\VC\Tools\Llvm\x64\bin'
 mise run --skip-tools windows:build:x64
 ```
 
-To use a local x64 Z3 release instead of the bundled build, set
+To use a local x64 Z3 release instead of the prebuilt download, set
 `Z3_LIBRARY_PATH_OVERRIDE` and `Z3_SYS_Z3_HEADER` before running the task:
 
 ```powershell
 
@@ -110,13 +110,15 @@ packaging-asset tests; its
 cross-platform Python, Markdown, license, and documentation checks still run.
 Test tasks require the Rust target architecture to match the Windows host, so
 an ARM64 test result is native coverage rather than x64 emulation coverage.
-By default it enables bundled Z3 for reproducible Windows builds. `z3-sys`
-builds Z3 from source and links it into the release binaries, so copying
-`openshell-gateway.exe` and `openshell.exe` does not create an undeclared
-`libz3.dll` runtime dependency. When `Z3_LIBRARY_PATH_OVERRIDE` points at a
-directory containing `libz3.lib`, the wrapper uses that system Z3 instead and
-requires `Z3_SYS_Z3_HEADER` to point at the full path to `z3.h`. Binaries built
-against a dynamic system Z3 must be deployed with the matching `libz3.dll`.
+By default it enables the `z3-sys` prebuilt-release feature and pins Z3 4.16.0.
+On a clean target directory, `z3-sys` downloads the official static library for
+the selected Windows architecture instead of compiling Z3 through
+CMake/MSBuild. GitHub Actions supplies its read-only workflow token for the
+release lookup, and the Cargo target cache preserves the extracted library for
+subsequent runs. When `Z3_LIBRARY_PATH_OVERRIDE` points at a directory
+containing `libz3.lib`, the wrapper uses that system Z3 instead and requires
+`Z3_SYS_Z3_HEADER` to point at the full path to `z3.h`. Local clean builds use
+the unauthenticated GitHub API unless `READ_ONLY_GITHUB_TOKEN` is set.
 
 GitHub Actions layers the Cargo target cache with sccache's GitHub Actions
 backend. The target cache lets Cargo skip intact dependency builds; sccache
@@ -136,10 +138,10 @@ Spectre-mitigated libraries, host-native Clang tools, CMake tools, and an
 ARM64-capable Windows SDK. Clang provides `libclang.dll` for `bindgen` and
 `clang-cl.exe` for ARM64 crypto dependencies. During x64-to-ARM64 check/build,
 the wrapper discovers and adds the Visual Studio-bundled Ninja to `PATH` for
-native dependencies. Bundled Z3 uses native MSVC `cl.exe` with the Visual
-Studio generator, while the crypto crates select `clang-cl`. Artifact hashing
-uses .NET SHA256 directly because module autoloading in the mise-launched
-Windows PowerShell process is not guaranteed.
+native dependencies. Z3 uses the official prebuilt ARM64 static library, so it
+does not inherit compiler settings from those native dependencies. Artifact
+hashing uses .NET SHA256 directly because module autoloading in the
+mise-launched Windows PowerShell process is not guaranteed.
 
 The wrapper defaults Cargo compilation to four jobs. Set
 `OPENSHELL_WINDOWS_BUILD_JOBS` to a positive integer to override that limit.
 
@@ -73,6 +73,7 @@ telemetry = ["openshell-core/telemetry", "openshell-server/telemetry"]
 ## `rust:verify:defaults-without-telemetry`.
 defaults-without-telemetry = ["in-tree-compute-drivers"]
 bundled-z3 = ["openshell-server/bundled-z3"]
+prebuilt-z3 = ["openshell-server/prebuilt-z3"]
 
 [lints]
 workspace = true
 
@@ -53,12 +53,13 @@ $WindowsCargoMutex = [System.Threading.Mutex]::new($false, "Local\OpenShellWindo
 $UnsupportedDriverPackageExcludes = "--exclude openshell-driver-docker --exclude openshell-driver-kubernetes --exclude openshell-driver-kubernetes-secrets --exclude openshell-driver-podman --exclude openshell-driver-vault --exclude openshell-driver-vm --exclude openshell-sandbox --exclude openshell-supervisor-process --exclude openshell-vfio"
 $WindowsClippyPackageExcludes = $UnsupportedDriverPackageExcludes
 $WindowsClippyLintArgs = "-D warnings -A dead-code -A unused-imports -A clippy::unused-async"
-$BundledZ3WorkspaceFeatures = "--features openshell-prover/bundled-z3"
-$BundledZ3ServerFeatures = "--features openshell-server/bundled-z3,openshell-prover/bundled-z3"
-$BundledZ3GatewayFeatures = "--features openshell-gateway/bundled-z3"
-$Z3WorkspaceFeatures = $BundledZ3WorkspaceFeatures
-$Z3ServerFeatures = $BundledZ3ServerFeatures
-$Z3GatewayFeatures = $BundledZ3GatewayFeatures
+$PrebuiltZ3WorkspaceFeatures = "--features openshell-prover/prebuilt-z3"
+$PrebuiltZ3ServerFeatures = "--features openshell-server/prebuilt-z3,openshell-prover/prebuilt-z3"
+$PrebuiltZ3GatewayFeatures = "--features openshell-gateway/prebuilt-z3"
+$PrebuiltZ3Version = "4.16.0"
+$Z3WorkspaceFeatures = $PrebuiltZ3WorkspaceFeatures
+$Z3ServerFeatures = $PrebuiltZ3ServerFeatures
+$Z3GatewayFeatures = $PrebuiltZ3GatewayFeatures
 
 function Get-VsInstallRoots {
     $programFiles = @(
@@ -354,11 +355,13 @@ function Resolve-Z3HeaderPath([string] $HeaderPath) {
 
 function Configure-Z3 {
     if ([string]::IsNullOrWhiteSpace($env:Z3_LIBRARY_PATH_OVERRIDE)) {
-        Write-Host "==> Z3: bundled"
+        Write-Host "==> Z3: prebuilt release"
+        $env:Z3_SYS_Z3_VERSION = $PrebuiltZ3Version
+        Write-Host "    Z3_SYS_Z3_VERSION=$env:Z3_SYS_Z3_VERSION"
         return [pscustomobject]@{
-            WorkspaceFeatures = $BundledZ3WorkspaceFeatures
-            ServerFeatures = $BundledZ3ServerFeatures
-            GatewayFeatures = $BundledZ3GatewayFeatures
+            WorkspaceFeatures = $PrebuiltZ3WorkspaceFeatures
+            ServerFeatures = $PrebuiltZ3ServerFeatures
+            GatewayFeatures = $PrebuiltZ3GatewayFeatures
         }
     }