diff --git a/.github/actions/rewrite-require/action.yml b/.github/actions/rewrite-require/action.yml
new file mode 100644
index 0000000000..513d52f95c
--- /dev/null
+++ b/.github/actions/rewrite-require/action.yml
@@ -0,0 +1,30 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Rewrite require to local path
+description: >
+  Rewrite a [[require]] block in a downstream lakefile.toml to point at a
+  local path instead of a git/rev dependency. Used by downstream-check
+  workflows to build a downstream repo against an upstream PR's checked-out
+  code (fork-safe: the PR head SHA need not be fetchable from the upstream
+  remote). The targeted block keeps its `name`; any git/rev/path/scope lines
+  are replaced with a single `path` line. Fails if no matching block exists.
+
+inputs:
+  lakefile:
+    description: Path to the downstream lakefile.toml to rewrite.
+    required: true
+  package:
+    description: The require `name` to override (e.g. "Strata", "StrataDDM").
+    required: true
+  path:
+    description: Local path to substitute (relative to the lakefile's repo root).
+    required: true
+
+runs:
+  using: composite
+  steps:
+    - name: Rewrite require
+      shell: bash
+      run: |
+        python3 "${{ github.action_path }}/../../scripts/rewrite_require.py" \
+          "${{ inputs.lakefile }}" "${{ inputs.package }}" "${{ inputs.path }}"
diff --git a/.github/scripts/rewrite_require.py b/.github/scripts/rewrite_require.py
new file mode 100644
index 0000000000..1f553ce22f
--- /dev/null
+++ b/.github/scripts/rewrite_require.py
@@ -0,0 +1,114 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+"""Rewrite a `[[require]]` block in a lakefile.toml to point at a local path.
+
+Used by the downstream-check workflow: a downstream repo's git/rev dependency
+on an upstream package (e.g. Strata) is replaced with a local `path` require so
+the build runs against the PR's checked-out code instead of a published rev.
+This is fork-safe (no need for the PR head SHA to be fetchable from the upstream
+remote) and faster (no re-clone of the upstream).
+
+Usage:
+    python rewrite_require.py <lakefile.toml> <package-name> <local-path>
+
+Example:
+    python rewrite_require.py downstream/lakefile.toml Strata ../upstream
+
+The targeted `[[require]]` block keeps its `name` line; any `git`, `rev`,
+`path`, `subDir`, or `scope` lines in that block are dropped and replaced with a
+single `path = "<local-path>"` line. Other require blocks are left untouched.
+Exits non-zero if no matching block is found, so the workflow fails loudly
+rather than silently building against the wrong rev.
+"""
+
+import sys
+
+# Keys that describe a dependency source. We strip all of them from the target
+# block and substitute a single `path` line, so a prior `git`+`rev` pair can't
+# linger and shadow the local override.
+SOURCE_KEYS = ("git", "rev", "path", "subdir", "scope", "url")
+
+
+def main() -> int:
+    if len(sys.argv) != 4:
+        print(__doc__)
+        return 2
+    lakefile, pkg, local_path = sys.argv[1], sys.argv[2], sys.argv[3]
+
+    with open(lakefile, encoding="utf-8") as f:
+        lines = f.readlines()
+
+    out: list[str] = []
+    i = 0
+    n = len(lines)
+    rewrote = False
+
+    while i < n:
+        line = lines[i]
+        if line.strip() == "[[require]]":
+            # Collect the block: every line up to (but not including) the next
+            # table header (`[` at column 0) or EOF.
+            block = [line]
+            j = i + 1
+            while j < n and not lines[j].lstrip().startswith("["):
+                block.append(lines[j])
+                j += 1
+
+            # Does this block require the package we're overriding?
+            is_target = any(
+                _is_name(bl, pkg) for bl in block
+            )
+            if is_target:
+                rewrote = True
+                out.append("[[require]]\n")
+                # Preserve the name line verbatim; drop source keys; keep
+                # anything else (e.g. options) as-is. Trailing blank lines are
+                # collected separately so the substituted `path` line sits
+                # directly under the kept keys, not after a gap.
+                kept: list[str] = []
+                trailing_blanks: list[str] = []
+                for bl in block[1:]:
+                    if bl.strip() == "":
+                        trailing_blanks.append(bl)
+                        continue
+                    # A non-blank line ends any run of pending blanks (they
+                    # were interior, not trailing) — flush them back.
+                    kept.extend(trailing_blanks)
+                    trailing_blanks = []
+                    key = bl.split("=", 1)[0].strip().lower()
+                    if key in SOURCE_KEYS:
+                        continue
+                    kept.append(bl)
+                out.extend(kept)
+                out.append(f'path = "{local_path}"\n')
+                out.extend(trailing_blanks)
+            else:
+                out.extend(block)
+            i = j
+        else:
+            out.append(line)
+            i += 1
+
+    if not rewrote:
+        print(
+            f"ERROR: no [[require]] block with name = \"{pkg}\" found in {lakefile}",
+            file=sys.stderr,
+        )
+        return 1
+
+    with open(lakefile, "w", encoding="utf-8") as f:
+        f.writelines(out)
+    print(f"Rewrote require \"{pkg}\" -> path = \"{local_path}\" in {lakefile}")
+    return 0
+
+
+def _is_name(line: str, pkg: str) -> bool:
+    s = line.strip()
+    if not s.startswith("name"):
+        return False
+    _, _, rhs = s.partition("=")
+    return rhs.strip().strip('"').strip("'") == pkg
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())
diff --git a/.github/workflows/downstream-check.yml b/.github/workflows/downstream-check.yml
new file mode 100644
index 0000000000..5852122e73
--- /dev/null
+++ b/.github/workflows/downstream-check.yml
@@ -0,0 +1,134 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+#
+# Downstream check: builds each repo that depends on Strata against this PR's
+# code, so we catch breakage before it lands on main. Advisory only — these
+# checks are visible on the PR but do not gate merge.
+#
+# Mechanism: check out the PR's Strata, clone each downstream, rewrite the
+# downstream's `require "Strata"` to a local path pointing at the checked-out
+# PR code (fork-safe: no need for the PR head SHA to exist on the strata-org
+# remote), then `lake update Strata` + build + test.
+#
+# Trigger: non-draft PRs only (ready_for_review + every push via synchronize).
+# We deliberately do NOT support an issue_comment (`!downstream-check`) trigger:
+# that runs in the privileged default-branch context, and building untrusted PR
+# code there is a cache-poisoning / code-execution vector (CodeQL
+# actions/cache-poisoning/poisonable-step). pull_request runs the same build in
+# an isolated, unprivileged context, which is safe. If on-demand checks are
+# wanted later, add them via label-indirection (a privileged workflow turns a
+# comment into a label; `pull_request: types: [labeled]` does the build
+# unprivileged) — never by reintroducing issue_comment here.
+
+name: Downstream check
+
+on:
+  pull_request:
+    types: [ready_for_review, synchronize]
+
+# One in-flight run per PR; a new push cancels the previous downstream check.
+concurrency:
+  group: downstream-${{ github.event.pull_request.number }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  downstream:
+    # Non-draft PRs only. (The `types` filter already restricts to
+    # ready_for_review/synchronize.)
+    if: ${{ !github.event.pull_request.draft }}
+    runs-on: ubuntu-latest
+    strategy:
+      # Don't let one broken downstream hide the status of the others.
+      fail-fast: false
+      matrix:
+        include:
+          # Boole and Python define a lake testDriver, so `test: true` builds
+          # and runs their suites.
+          - repo: Strata-Boole
+            test: true
+          - repo: Strata-Python
+            test: true
+          # Strata-CLI has no testDriver; mirror its own CI — build, then
+          # exercise the binary + examples via post_build (run below).
+          - repo: Strata-CLI
+            test: false
+            post_build: |
+              lake exe strata --help
+              ./scripts/run_examples.sh
+    # The job name is what reviewers see in the PR's Checks tab:
+    # "Downstream / Strata-Boole", etc.
+    name: ${{ matrix.repo }}
+    steps:
+      - name: Check out PR's Strata
+        uses: actions/checkout@v6
+        with:
+          ref: ${{ github.event.pull_request.head.sha }}
+          path: upstream
+
+      - name: Clone downstream (${{ matrix.repo }})
+        run: git clone --depth 1 https://github.com/strata-org/${{ matrix.repo }}.git downstream
+
+      - name: Override Strata require -> local PR checkout
+        uses: ./upstream/.github/actions/rewrite-require
+        with:
+          lakefile: downstream/lakefile.toml
+          package: Strata
+          path: ../upstream
+
+      - name: Install cvc5
+        uses: ./upstream/.github/actions/install-cvc5
+      - name: Install z3
+        uses: ./upstream/.github/actions/install-z3
+
+      # Install the Lean toolchain (elan/lake) before `lake update`. elan is
+      # installed unconditionally by lean-action; auto-config: false skips its
+      # build/test so this step only provisions the toolchain. The build itself
+      # runs in the "Build downstream" step below.
+      - name: Set up Lean toolchain
+        uses: leanprover/lean-action@v1
+        with:
+          lake-package-directory: downstream
+          auto-config: false
+          use-github-cache: false
+
+      # Cache keyed on upstream head SHA + downstream repo. The restore-keys
+      # fallback lets a new push reuse the previous build for this PR; lake
+      # rebuilds the modules whose (overridden, local) Strata source changed.
+      # Trades a small stale-result risk for ~15-30 min, matching Strata CI's
+      # PR caching posture. This is advisory CI, so the trade is acceptable.
+      - name: Restore lake cache
+        uses: actions/cache/restore@v5
+        with:
+          path: |
+            downstream/.lake
+          key: downstream-${{ matrix.repo }}-${{ runner.os }}-${{ github.event.pull_request.head.sha }}
+          restore-keys: |
+            downstream-${{ matrix.repo }}-${{ runner.os }}-
+
+      - name: lake update Strata
+        working-directory: downstream
+        run: lake update Strata
+
+      - name: Build downstream
+        uses: leanprover/lean-action@v1
+        with:
+          lake-package-directory: downstream
+          use-github-cache: false
+          test: ${{ matrix.test }}
+
+      # Repos without a lake testDriver verify via their own post-build steps.
+      - name: Post-build checks (${{ matrix.repo }})
+        if: matrix.post_build != ''
+        working-directory: downstream
+        run: ${{ matrix.post_build }}
+
+      - name: Save lake cache
+        if: always()
+        uses: actions/cache/save@v5
+        with:
+          path: |
+            downstream/.lake
+          key: downstream-${{ matrix.repo }}-${{ runner.os }}-${{ github.event.pull_request.head.sha }}