diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index b1a789496f..40d51e395d 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -296,11 +296,16 @@ Project requirements:
 - Rust 1.90+
 - Python 3.11+
 - Docker (running)
+- CMake 3.16+ (only required when building with the `bundled-z3` feature)
 
 ### Z3 installation
 
-The `openshell-prover` crate links against Z3. On macOS and Linux, install the
-system Z3 development package; `z3-sys` discovers it through `pkg-config`.
+The `openshell-prover` crate links directly against Z3. The `openshell-server`
+crate depends on the prover, and the `openshell-gateway` binary crate depends
+on `openshell-server` in turn; both forward a `bundled-z3` feature down to
+`openshell-prover/bundled-z3`. The `openshell-cli` crate does not depend on
+Z3. On macOS and Linux, install the system Z3 development package; `z3-sys`
+discovers it through `pkg-config`.
 
 ```bash
 # macOS
@@ -314,7 +319,7 @@ sudo dnf install z3-devel
 ```
 
 If you prefer not to install Z3 system-wide, use the bundled Z3 feature. This
-compiles Z3 from source during the Rust build:
+compiles Z3 from source during the Rust build and requires CMake 3.16+:
 
 ```bash
 cargo build -p openshell-prover --features bundled-z3
@@ -328,16 +333,29 @@ For x86-64 Windows MSVC builds, use one of these Z3 paths:
   is set.
 - Bundled Z3: pass `--features bundled-z3` so `z3-sys` builds Z3 from source.
 
-Both Windows paths still require `libclang.dll` for `bindgen`. If LLVM is not on
-the default search path, set `LIBCLANG_PATH` to the directory containing
-`libclang.dll`.
+`openshell-prover` itself has no `bindgen`/`libclang` dependency, so building
+just this crate does not require `LIBCLANG_PATH`:
+
+```powershell
+cargo build -p openshell-prover --target x86_64-pc-windows-msvc --features bundled-z3
+```
+
+### Windows full build
+
+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`:
 
 ```powershell
 $env:LIBCLANG_PATH='C:\Program Files\Microsoft Visual Studio\2022\<Edition>\VC\Tools\Llvm\x64\bin'
-cargo build -p openshell-cli --target x86_64-pc-windows-msvc --features bundled-z3
+mise run --skip-tools windows:build:x64
 ```
 
-To use a local x64 Z3 release with the Windows task wrapper:
+To use a local x64 Z3 release instead of the bundled build, set
+`Z3_LIBRARY_PATH_OVERRIDE` and `Z3_SYS_Z3_HEADER` before running the task:
 
 ```powershell
 $env:Z3_LIBRARY_PATH_OVERRIDE='C:\path\to\z3-4.16.0-x64-win\bin'