diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
new file mode 100644
index 0000000..05ec345
--- /dev/null
+++ b/.github/CODEOWNERS
@@ -0,0 +1,3 @@
+# Defaults owners for everything in the repo. unless a later match
+# takes precedence
+*       @strata-org/reviewers
diff --git a/.github/actions/restore-lake-cache/action.yml b/.github/actions/restore-lake-cache/action.yml
new file mode 100644
index 0000000..8c6a33a
--- /dev/null
+++ b/.github/actions/restore-lake-cache/action.yml
@@ -0,0 +1,76 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Restore lake cache
+description: >
+  Thin wrapper around actions/cache/restore@v5 using the cache key
+    lake-<os>-<arch>-<lean-toolchain>-<lake-manifest>-<sha>
+  with two fallback keys dropping each trailing component in turn. The
+  manifest hash covers the cloned Strata dependency.
+inputs:
+  fail-on-cache-miss:
+    description: >
+      If 'true', the step fails when no cache entry matches. Use this in
+      jobs that depend on a cache saved by an upstream job for the same
+      SHA (see https://github.com/strata-org/Strata/issues/952).
+    required: false
+    default: "false"
+  path:
+    description: Cache path(s), newline-separated.
+    required: false
+    default: ".lake"
+  key-prefix:
+    description: >
+      Prefix used in the cache key. The action also hashes the
+      repo-root `lean-toolchain` and `lake-manifest.json`, so changing
+      only this prefix is appropriate for caches keyed on the same
+      root-level Lean build (e.g. distinguishing different artifact
+      names with the same source set). Sub-projects with their own
+      toolchain/manifest do not currently fit this action and should
+      not reuse it as-is.
+    required: false
+    default: "lake"
+  use-restore-keys:
+    description: >
+      Must be the string `'true'` or `'false'`.
+
+      If `'true'` (default), include two fallback `restore-keys` so
+      that a near match (same toolchain/manifest but different SHA) is
+      used when no exact-SHA cache exists.
+
+      Set to `'false'` for downstream jobs that depend on a cache saved
+      by an upstream job for the *same* SHA (typically together with
+      `fail-on-cache-miss: 'true'`); see
+      https://github.com/strata-org/Strata/issues/952. With fallback
+      keys present, `fail-on-cache-miss` only triggers when every
+      fallback also misses, which silently allows stale cross-SHA cache
+      matches and defeats the safety net.
+    required: false
+    default: "true"
+
+outputs:
+  cache-hit:
+    description: Whether a cache entry was restored (see actions/cache/restore@v5).
+    value: ${{ steps.restore-with-fallback.outputs.cache-hit || steps.restore-exact.outputs.cache-hit }}
+
+runs:
+  using: composite
+  steps:
+    - name: Restore lake cache (with fallback keys)
+      id: restore-with-fallback
+      if: inputs.use-restore-keys != 'false'
+      uses: actions/cache/restore@v5
+      with:
+        path: ${{ inputs.path }}
+        key: ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
+        restore-keys: |
+          ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
+          ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}
+        fail-on-cache-miss: ${{ inputs.fail-on-cache-miss }}
+    - name: Restore lake cache (exact SHA only)
+      id: restore-exact
+      if: inputs.use-restore-keys == 'false'
+      uses: actions/cache/restore@v5
+      with:
+        path: ${{ inputs.path }}
+        key: ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
+        fail-on-cache-miss: ${{ inputs.fail-on-cache-miss }}
diff --git a/.github/actions/save-lake-cache/action.yml b/.github/actions/save-lake-cache/action.yml
new file mode 100644
index 0000000..4490e8a
--- /dev/null
+++ b/.github/actions/save-lake-cache/action.yml
@@ -0,0 +1,35 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Save lake cache
+description: >
+  Save the lake build cache.
+  Companion to `restore-lake-cache`: the two actions share the same key
+  construction so downstream jobs that consume the saved cache via
+  `restore-lake-cache` with `use-restore-keys: "false"` will hit it
+  reliably.
+
+  Use this in workflows that produce a fresh build (typically the
+  `build_and_test_lean` job in ci.yml) to share the result with
+  downstream jobs at the same SHA.
+
+inputs:
+  path:
+    description: Cache path(s), newline-separated.
+    required: false
+    default: ".lake"
+  key-prefix:
+    description: >
+      Cache-key prefix; must match the `key-prefix` passed to the
+      companion `restore-lake-cache` action so that the exact-SHA
+      restore keys line up.
+    required: false
+    default: "lake"
+
+runs:
+  using: composite
+  steps:
+    - name: Save lake cache
+      uses: actions/cache/save@v5
+      with:
+        path: ${{ inputs.path }}
+        key: ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
diff --git a/.github/dependabot.yml b/.github/dependabot.yml
new file mode 100644
index 0000000..18d711f
--- /dev/null
+++ b/.github/dependabot.yml
@@ -0,0 +1,8 @@
+# https://docs.github.com/en/code-security/dependabot/dependabot-version-updates/configuration-options-for-the-dependabot.yml-file
+
+version: 2
+updates:
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    schedule:
+      interval: "weekly"
diff --git a/.github/pull_request_template.md b/.github/pull_request_template.md
new file mode 100644
index 0000000..fdcf85f
--- /dev/null
+++ b/.github/pull_request_template.md
@@ -0,0 +1,9 @@
+### Description
+
+<!-- Briefly describe what this PR changes and why. -->
+
+### Checklist
+
+- [ ] `lake build StrataPython StrataPythonTest` succeeds locally
+- [ ] New `.lean` files start with the standard copyright header
+- [ ] No trailing whitespace and files end with a newline
diff --git a/.github/workflows/cbmc.yml b/.github/workflows/cbmc.yml
new file mode 100644
index 0000000..fe7c641
--- /dev/null
+++ b/.github/workflows/cbmc.yml
@@ -0,0 +1,72 @@
+name: CBMC
+
+on:
+  workflow_call:
+
+jobs:
+  cbmc_test:
+    name: Run CBMC tests
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v6
+      - name: Install cvc5
+        uses: strata-org/Strata/.github/actions/install-cvc5@main
+      - name: Install z3
+        uses: strata-org/Strata/.github/actions/install-z3@main
+      - name: Restore lake cache
+        # The cache is safe to use here because we just saved it for this exact
+        # SHA in the build_and_test_lean job from ci.yml. Restoring it also
+        # brings back the cloned Strata dependency under .lake/packages/Strata,
+        # which holds the Laurel/regex/quantifier CBMC patches applied below.
+        # https://github.com/strata-org/Strata/issues/952
+        uses: ./.github/actions/restore-lake-cache
+        with:
+          path: .lake
+          fail-on-cache-miss: "true"
+          use-restore-keys: "false"
+      - name: Prepare ccache
+        uses: actions/cache@v5
+        with:
+          save-always: true
+          path: .ccache
+          key: cbmc-${{ runner.os }}-${{ runner.arch }}-cbmc-${{ github.sha }}
+          restore-keys: |
+            cbmc-${{ runner.os }}-${{ runner.arch }}-cbmc
+      - name: Build CBMC from source (with string support patch)
+        shell: bash
+        run: |
+          sudo apt-get -qq update
+          sudo apt-get -qq install -y cmake ninja-build flex bison ccache
+          git clone --depth 1 --branch cbmc-6.8.0 https://github.com/diffblue/cbmc.git cbmc-src
+          cd cbmc-src
+          STRATA="$GITHUB_WORKSPACE/.lake/packages/Strata"
+          git apply "$GITHUB_WORKSPACE/StrataPythonTest/cbmc-string-support.patch"
+          git apply "$STRATA/StrataTest/Languages/Laurel/cbmc-bounds-check.patch"
+          git apply "$STRATA/StrataTest/Backends/CBMC/cbmc-regex-support.patch"
+          git apply "$STRATA/StrataTest/Backends/CBMC/cbmc-quantifier-simplify.patch"
+          export CCACHE_BASEDIR=$PWD
+          export CCACHE_DIR=$GITHUB_WORKSPACE/.ccache
+          cmake -S . -B build -G Ninja \
+            -DCMAKE_BUILD_TYPE=Release \
+            -DWITH_JBMC=OFF
+          ccache -z --max-size=500M
+          ninja -C build cbmc symtab2gb goto-cc goto-instrument
+          ccache -s
+          echo "$GITHUB_WORKSPACE/cbmc-src/build/bin/" >> $GITHUB_PATH
+      - name: Build StrataPython
+        uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
+          build: true
+          use-github-cache: false
+      - uses: actions/setup-python@v6
+        with:
+          python-version: '3.14'
+      - name: Run Python CBMC pipeline tests
+        shell: bash
+        run: |
+          pip install ./.lake/packages/Strata/Tools/Python-base ./Tools/strata-python
+          ./StrataPythonTest/run_py_cbmc_tests.sh
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 0000000..46a4e4d
--- /dev/null
+++ b/.github/workflows/ci.yml
@@ -0,0 +1,193 @@
+name: Build
+
+on:
+  pull_request:
+  merge_group:
+  push:
+    branches: [main]
+
+jobs:
+  build_and_test_lean:
+    name: Build and test Lean
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        toolchain:
+          - stable
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v6
+      - name: Install cvc5
+        uses: strata-org/Strata/.github/actions/install-cvc5@main
+      - name: Install z3
+        uses: strata-org/Strata/.github/actions/install-z3@main
+      - name: Restore lake cache
+        # Only use the caches on PRs because there is a risk of stale results:
+        # https://github.com/strata-org/Strata/issues/952
+        if: github.event_name == 'pull_request'
+        uses: ./.github/actions/restore-lake-cache
+        with:
+          path: .lake
+      - name: Build StrataPython and compile-time tests
+        # Building StrataPythonTest runs the compile-time test suite: the tests
+        # are `#guard_msgs` / `#eval` checks that execute during elaboration.
+        # This also resolves the `Strata` git dependency, cloning it into
+        # `.lake/packages/Strata`.
+        uses: leanprover/lean-action@v1
+        with:
+          build-args: StrataPython StrataPythonTest
+          use-github-cache: false
+          test: false
+      - uses: actions/setup-python@v6
+        with:
+          python-version: '3.14'
+      - name: Build using pip
+        # `strata-base` lives in the Strata package that lake cloned into
+        # `.lake/packages/Strata`; `strata-python` is in this repo.
+        run: |
+          pip install ./.lake/packages/Strata/Tools/Python-base
+          pip install ./Tools/strata-python
+      - name: Run pyInterpret golden-file tests
+        working-directory: StrataPythonTest
+        shell: bash
+        run: ./run_py_interpret.sh
+      - name: Run pyAnalyze SARIF tests
+        working-directory: StrataPythonTest
+        shell: bash
+        run: python run_py_analyze_sarif.py
+      - name: Run pyAnalyze golden-file tests
+        working-directory: StrataPythonTest
+        shell: bash
+        run: ./run_py_analyze.sh
+      - name: Run regex differential tests
+        working-directory: StrataPythonTest/Regex
+        run: python diff_test.py
+      - name: Save lake cache
+        uses: ./.github/actions/save-lake-cache
+        with:
+          path: .lake
+
+  check_pending_python:
+    needs: build_and_test_lean
+    name: Check pending Python tests
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+    steps:
+    - uses: actions/checkout@v6
+    - uses: actions/setup-python@v6
+      with:
+        python-version: '3.14'
+    - name: Restore Lean build cache
+      # The cache is safe to use here because we just saved it for this exact SHA
+      # in the build_and_test_lean job
+      # https://github.com/strata-org/Strata/issues/952
+      uses: ./.github/actions/restore-lake-cache
+      with:
+        path: .lake
+        fail-on-cache-miss: "true"
+        use-restore-keys: "false"
+    - name: Build using pip
+      run: |
+        pip install ./.lake/packages/Strata/Tools/Python-base
+        pip install ./Tools/strata-python
+    - name: Install Lean
+      uses: leanprover/lean-action@v1
+      with:
+        auto-config: false
+        build: false
+    - name: Install cvc5
+      uses: strata-org/Strata/.github/actions/install-cvc5@main
+      with:
+        install-to: system
+    - name: Check pending tests for newly passing
+      working-directory: StrataPythonTest
+      shell: bash
+      run: ./run_py_analyze.sh --check-pending
+
+  lint_checks:
+    name: Run lint checks
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+    strategy:
+      matrix:
+        toolchain:
+          - stable
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v6
+        with:
+          fetch-depth: 0
+      - name: Check copyright headers
+        uses: strata-org/Strata/.github/actions/check-copyright-headers@main
+      - name: Check for trailing whitespace
+        uses: strata-org/Strata/.github/actions/lint-whitespace@main
+        with:
+          directory: .
+      - name: Check for import Lean
+        uses: strata-org/Strata/.github/actions/check-lean-import@main
+      - name: Check for new panic! usage
+        uses: strata-org/Strata/.github/actions/check-no-panic@main
+        with:
+          base-ref: "origin/${{ github.base_ref || 'main' }}"
+
+  build_python:
+    needs: build_and_test_lean
+    name: Build and test Python
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+    strategy:
+      matrix:
+        python_version: [3.11, 3.12, 3.13, 3.14]
+    steps:
+    - uses: actions/checkout@v6
+    - uses: actions/setup-python@v6
+      with:
+        python-version: ${{ matrix.python_version }}
+    - name: Restore Lean build cache
+      # The cache is safe to use here because we just saved it for this exact SHA
+      # in the build_and_test_lean job
+      # https://github.com/strata-org/Strata/issues/952
+      uses: ./.github/actions/restore-lake-cache
+      with:
+        path: .lake
+        fail-on-cache-miss: "true"
+        use-restore-keys: "false"
+    - name: Build using pip
+      run: |
+        pip install ./.lake/packages/Strata/Tools/Python-base
+        pip install ./Tools/strata-python
+    - name: Install Lean (for lake env)
+      uses: leanprover/lean-action@v1
+      with:
+        auto-config: false
+        build: false
+        use-github-cache: false
+    - name: Install cvc5
+      uses: strata-org/Strata/.github/actions/install-cvc5@main
+      with:
+        install-to: system
+    - name: Install z3
+      uses: strata-org/Strata/.github/actions/install-z3@main
+      with:
+        install-to: system
+    - name: Run PySpec and dispatch tests
+      # Excludes the CPython differential test, which is run separately below
+      # against a full CPython checkout; here it would be a no-op anyway since
+      # CPYTHON_DIR is unset.
+      run: PYTHON=python lake test -- --exclude CpythonDiffTest
+    - name: Run CPython differential tests
+      # Clones CPython at the matrix version and round-trips its whole test
+      # suite through the Strata generator + Ion (de)serializer. The round-trip
+      # check runs in-process inside the StrataPythonTestExtra/CpythonDiffTest
+      # Lean test (driven by this script), so no separate `strata` CLI is built.
+      run: FAIL_FAST=1 ./scripts/run_cpython_tests.sh ${{ matrix.python_version }}
+      working-directory: Tools/strata-python
+
+  cbmc:
+    needs: build_and_test_lean
+    permissions:
+      contents: read
+    uses: ./.github/workflows/cbmc.yml
diff --git a/StrataPythonTestExtra/CpythonDiffTest.lean b/StrataPythonTestExtra/CpythonDiffTest.lean
new file mode 100644
index 0000000..74f7a18
--- /dev/null
+++ b/StrataPythonTestExtra/CpythonDiffTest.lean
@@ -0,0 +1,186 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+meta import StrataPythonTest.Util.Python -- shake: keep
+public meta import StrataDDM
+public meta import StrataPython.PythonDialect
+import StrataPython
+import StrataPython.ReadPython
+
+/-! ## CPython differential test
+
+Round-trips every `.py` file under a directory through the Python generator and
+the Strata Ion (de)serializer, mirroring the old `run_test.sh` shell script.
+
+For each Python file the test:
+
+1. Runs `python -m strata_python.gen py_to_strata` to produce a `.python.st.ion`
+   file (the subject under test is the Python parser/generator).
+2. Reads that Ion file into a `StrataDDM.Program`, re-serializes it to Ion, and
+   reads it back — then asserts the two programs are syntactically equal. This
+   replaces the `strata toIon` + `strata diff` round-trip the shell script ran
+   through the `strata` CLI; here it is an in-process library call, so no
+   separate `StrataCLI` build is required.
+
+Orchestration (cloning CPython at a given version, choosing the version, and
+the list of files expected to fail) stays in the calling shell script. This
+test is driven entirely by environment variables so it stays inert during a
+plain `lake test`:
+
+- `CPYTHON_DIR`   — directory to scan recursively for `*.py` files. When unset
+                    or empty, the test is a no-op and succeeds, so local
+                    `lake test` runs stay green without a CPython checkout.
+- `CPYTHON_EXPECTED_FAILURES` — optional path to a plaintext file listing, one
+                    per line, path suffixes of files that are expected to FAIL
+                    to parse/round-trip. A line matches a discovered file when
+                    the file path ends with that suffix (matching the
+                    substring logic of the original shell script). Blank lines
+                    and lines starting with `#` are ignored.
+- `CPYTHON_FAIL_FAST` — when set to a non-empty value, stop and report on the
+                    first unexpected outcome instead of scanning everything.
+-/
+
+open StrataDDM.Parser (stringInputContext)
+open StrataPython (withPython)
+
+namespace StrataPython.CpythonDiffTest
+
+meta section
+
+/-- Recursively collect all `*.py` files under `dir`. -/
+private partial def findPyFiles (dir : System.FilePath) : IO (Array System.FilePath) := do
+  let mut results := #[]
+  for entry in ← dir.readDir do
+    if ← entry.path.isDir then
+      results := results ++ (← findPyFiles entry.path)
+    else if entry.path.extension == some "py" then
+      results := results.push entry.path
+  return results
+
+/-- Read the expected-failures list: a plaintext file with one path suffix per
+    line. Blank lines and `#` comments are ignored. -/
+private def readExpectedFailures (path : System.FilePath) : IO (Array String) := do
+  let contents ← IO.FS.readFile path
+  let lines := contents.splitOn "\n"
+    |>.map (·.trimAscii.toString)
+    |>.filter (fun l => !l.isEmpty && !l.startsWith "#")
+  return lines.toArray
+
+/-- Is `file` expected to fail? True when its path ends with any listed suffix. -/
+private def isExpectedFailure (expected : Array String) (file : System.FilePath) : Bool :=
+  let s := file.toString
+  expected.any (fun suffix => s.endsWith suffix)
+
+/-- Run the generator on `pyFile`, writing Ion to `ionFile`. Returns `.ok ()` on
+    success or `.error msg` if the generator exits non-zero. -/
+private def runPyToStrata (pythonCmd : System.FilePath)
+    (dialectFile pyFile ionFile : System.FilePath) : IO (Except String Unit) := do
+  let child ← IO.Process.spawn {
+    cmd := pythonCmd.toString
+    args := #["-m", "strata_python.gen", "py_to_strata",
+              "--dialect", dialectFile.toString,
+              pyFile.toString, ionFile.toString]
+    inheritEnv := true
+    stdin := .null, stdout := .null, stderr := .piped
+  }
+  let stderr ← child.stderr.readToEnd
+  let exitCode ← child.wait
+  if exitCode = 0 then
+    return .ok ()
+  else
+    return .error s!"py_to_strata failed (exit code {exitCode}): {stderr}"
+
+/-- The in-process equivalent of `strata toIon` followed by `strata diff`: read
+    the Python Ion program, re-serialize it to Ion, read it back, and require
+    the two programs to be syntactically identical. -/
+private def roundTripIon (ionFile : System.FilePath) : IO (Except String Unit) := do
+  let bytes ← IO.FS.readBinFile ionFile
+  match StrataDDM.Program.fromIon Python_map Python.name bytes with
+  | .error msg => return .error s!"read failed: {msg}"
+  | .ok pgm =>
+    let reBytes := StrataDDM.writeStrataIon pgm
+    match StrataDDM.Program.fromIon Python_map Python.name reBytes with
+    | .error msg => return .error s!"re-read failed: {msg}"
+    | .ok pgm2 =>
+      if pgm.dialect != pgm2.dialect then
+        return .error s!"dialects differ: {pgm.dialect} and {pgm2.dialect}"
+      if pgm.commands.size != pgm2.commands.size then
+        return .error
+          s!"command count differs: {pgm.commands.size} and {pgm2.commands.size}"
+      for (c1, c2) in pgm.commands.zip pgm2.commands do
+        if c1 != c2 then
+          return .error "commands differ after Ion round-trip"
+      return .ok ()
+
+/-- Process a single Python file: generate Ion, then round-trip it. Returns
+    `.ok ()` on a clean round-trip, `.error msg` otherwise. -/
+private def checkFile (pythonCmd dialectFile : System.FilePath) (pyFile : System.FilePath)
+    : IO (Except String Unit) := do
+  IO.FS.withTempDir fun tmpDir => do
+    let ionFile := tmpDir / "out.python.st.ion"
+    match ← runPyToStrata pythonCmd dialectFile pyFile ionFile with
+    | .error msg => return .error msg
+    | .ok () => roundTripIon ionFile
+
+/-- Run the differential test over `dir`. -/
+private def runOn (pythonCmd : System.FilePath) (dir : System.FilePath)
+    (expected : Array String) (failFast : Bool) : IO Unit := do
+  IO.FS.withTempDir fun tmpDir => do
+    -- Write the Python dialect once for the generator to consume.
+    let dialectFile := tmpDir / "Python.dialect.st.ion"
+    IO.FS.writeBinFile dialectFile Python.toIon
+
+    let files ← findPyFiles dir
+    IO.println s!"Found {files.size} Python file(s) under {dir}"
+
+    let mut count := 0
+    let mut failures := 0
+    for pyFile in files do
+      count := count + 1
+      let shouldFail := isExpectedFailure expected pyFile
+      let result ← checkFile pythonCmd dialectFile pyFile
+      match result, shouldFail with
+      | .ok (), false => pure ()
+      | .error _, true =>
+        IO.println s!"  ok (expected failure): {pyFile}"
+      | .ok (), true =>
+        IO.println s!"  UNEXPECTED PASS (expected failure): {pyFile}"
+        failures := failures + 1
+      | .error msg, false =>
+        IO.println s!"  FAIL: {pyFile}\n    {msg}"
+        failures := failures + 1
+      if failFast && failures > 0 then
+        throw <| .userError s!"Failed on {pyFile} (fail-fast)"
+
+    IO.println s!"Checked {count} file(s), {failures} failure(s)."
+    if failures > 0 then
+      throw <| .userError s!"{failures} CPython differential test failure(s)."
+
+/-- Entry point: read configuration from the environment and run, or no-op when
+    `CPYTHON_DIR` is unset. -/
+def main : IO Unit := do
+  match ← IO.getEnv "CPYTHON_DIR" with
+  | none =>
+    IO.println "CPYTHON_DIR not set; skipping CPython differential test."
+  | some dirStr =>
+    if dirStr.trimAscii.toString.isEmpty then
+      IO.println "CPYTHON_DIR empty; skipping CPython differential test."
+      return
+    let dir : System.FilePath := dirStr
+    let expected ← match ← IO.getEnv "CPYTHON_EXPECTED_FAILURES" with
+      | some p => if p.trimAscii.toString.isEmpty then pure #[] else readExpectedFailures p
+      | none => pure #[]
+    let failFast := match ← IO.getEnv "CPYTHON_FAIL_FAST" with
+      | some v => !v.trimAscii.toString.isEmpty
+      | none => false
+    withPython fun pythonCmd => runOn pythonCmd dir expected failFast
+
+end
+
+end StrataPython.CpythonDiffTest
+
+#eval StrataPython.CpythonDiffTest.main
diff --git a/Tools/strata-python/scripts/run_cpython_tests.sh b/Tools/strata-python/scripts/run_cpython_tests.sh
index 409ce57..85b7861 100755
--- a/Tools/strata-python/scripts/run_cpython_tests.sh
+++ b/Tools/strata-python/scripts/run_cpython_tests.sh
@@ -1,22 +1,24 @@
 #!/bin/bash
 set -euo pipefail
 
-# This script run the CPython parser on all the examples for the
-# select CPython version.  If the FAIL_FAST variable is set to a
-# non-empty string, then it will stop on the first failure and print
-# the failure report.  This is predominantly used in CI.
-
-if [ ! -f "scripts/run_test.sh" ]; then
-  >@2 echo "File does not exist: scripts/run_test.sh"
-  exit 1
-elif [ ! -f "scripts/gen_dialect.sh" ]; then
-  >@2 echo "File does not exist: scripts/gen_dialect.sh"
-  exit 1
-fi
+# Clone the CPython sources for a given version and run the Strata Python
+# generator over every file in its test suite, checking that each round-trips
+# through Strata's Ion (de)serializer.
+#
+# This script handles orchestration only: cloning CPython, selecting the
+# interpreter, and computing the list of files expected to fail. The actual
+# per-file work (running `strata_python.gen py_to_strata` and verifying the Ion
+# round-trip) is done by the Lean test `StrataPythonTestExtra/CpythonDiffTest`,
+# which we drive here by setting environment variables and running `lake test`.
+# Doing the round-trip in Lean means we no longer need a separate `strata` CLI
+# build.
+#
+# If the FAIL_FAST variable is set to a non-empty string, the Lean test stops
+# on the first unexpected outcome. This is predominantly used in CI.
 
 if [ "$#" -ne 1 ]; then
     >&2 echo "Missing CPython version to test"
-    exit
+    exit 1
 fi
 
 VER="$1"
@@ -24,88 +26,57 @@ prefix="cpython-$VER"
 if [ -d "$prefix" ]; then
   echo "Skipping download: $prefix already exists"
 else
-  git clone https://github.com/python/cpython.git --branch $VER --depth 1 $prefix
-fi
-
-if [ ! -f "dialects/Python.dialect.st.ion" ]; then
-  >@2 echo "Missing Python dialect.  Run ./scripts/gen_dialect.sh with Python 3.13 or later"
-  exit 1
+  git clone https://github.com/python/cpython.git --branch "$VER" --depth 1 "$prefix"
 fi
 
-if [ "$VER" == "3.14" ]; then
-  expected_failures="/tokenizedata/bad_coding.py"
-  expected_failures="$expected_failures;/tokenizedata/bad_coding2.py"
-  expected_failures="$expected_failures;/tokenizedata/badsyntax_3131.py"
-  expected_failures="$expected_failures;/tokenizedata/badsyntax_pep3120.py"
-elif [ "$VER" == "3.13" ]; then
-  expected_failures="/tokenizedata/bad_coding.py"
-  expected_failures="$expected_failures;/tokenizedata/bad_coding2.py"
-  expected_failures="$expected_failures;/tokenizedata/badsyntax_3131.py"
-  expected_failures="$expected_failures;/tokenizedata/badsyntax_pep3120.py"
-elif [ "$VER" == "3.12" ]; then
-  expected_failures="/tokenizedata/bad_coding.py"
-  expected_failures="$expected_failures;/tokenizedata/bad_coding2.py"
-  expected_failures="$expected_failures;/tokenizedata/badsyntax_3131.py"
-  expected_failures="$expected_failures;/tokenizedata/badsyntax_pep3120.py"
-  expected_failures="$expected_failures;/test_lib2to3/data/different_encoding.py"
-  expected_failures="$expected_failures;/test_lib2to3/data/false_encoding.py"
-  expected_failures="$expected_failures;/test_lib2to3/data/bom.py"
-  expected_failures="$expected_failures;/test_lib2to3/data/py2_test_grammar.py"
-  expected_failures="$expected_failures;/test_lib2to3/data/crlf.py"
-elif [ "$VER" == "3.11" ]; then
-  expected_failures="/tokenizedata/bad_coding.py"
-  expected_failures="$expected_failures;/tokenizedata/bad_coding2.py"
-  expected_failures="$expected_failures;/tokenizedata/badsyntax_3131.py"
-  expected_failures="$expected_failures;/tokenizedata/badsyntax_pep3120.py"
-else
-  expected_failures=""
-fi
+# Files in the CPython test suite that are expected to fail to parse (and so
+# should fail the round-trip). Listed as path suffixes, one per line; the Lean
+# test matches a discovered file when its path ends with one of these.
+expected_failures=""
+case "$VER" in
+  3.14|3.13|3.11)
+    expected_failures="/tokenizedata/bad_coding.py
+/tokenizedata/bad_coding2.py
+/tokenizedata/badsyntax_3131.py
+/tokenizedata/badsyntax_pep3120.py"
+    ;;
+  3.12)
+    expected_failures="/tokenizedata/bad_coding.py
+/tokenizedata/bad_coding2.py
+/tokenizedata/badsyntax_3131.py
+/tokenizedata/badsyntax_pep3120.py
+/test_lib2to3/data/different_encoding.py
+/test_lib2to3/data/false_encoding.py
+/test_lib2to3/data/bom.py
+/test_lib2to3/data/py2_test_grammar.py
+/test_lib2to3/data/crlf.py"
+    ;;
+esac
 
-if command -v mise >/dev/null 2>&1; then
-  python="mise x python@$VER -- python"
+# Select the interpreter. Prefer the requested version via mise, falling back to
+# python3; export it as PYTHON so the Lean test's `withPython` picks it up.
+if command -v mise >/dev/null 2>&1 && mise where "python@$VER" >/dev/null 2>&1; then
+  PYTHON="$(mise where "python@$VER")/bin/python"
 else
-  python="python3"
+  PYTHON="python3"
 fi
+export PYTHON
 
-report="report.$VER.txt"
+# Directories used by the Lean test.
+SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"
+STRATA_PYTHON_PKG="$(cd "$SCRIPT_DIR/../../.." && pwd)"  # repo root (lake package)
+TOOLS_DIR="$(cd "$SCRIPT_DIR/.." && pwd)"
 
-echo "Generating report in $report" | tee $report
-count=1
-failures=0
-for i in `find $prefix/Lib/test -name "*.py"`; do
-  if [[ "$expected_failures" == *"${i#$prefix/Lib/test}"* ]]; then
-    should_fail=1
-    echo "$count : $i (expecting failure)" | tee -a "$report"
-  else
-    should_fail=0
-    echo "$count : $i" | tee -a "$report"
-  fi
-  count=$((count + 1))
+# Write the expected-failures list to a plaintext file the Lean test reads.
+expected_file="$(mktemp)"
+trap 'rm -f "$expected_file"' EXIT
+printf '%s\n' "$expected_failures" > "$expected_file"
 
-  set +e
-  PYTHON="$python" ./scripts/run_test.sh $i >> "$report" 2>&1
-  status=$?
-  set -e
-  if [ $should_fail -ne 0 ]; then
-    if [ "$status" -eq 0 ]; then
-      failures=$((failures + 1))
-    fi
-  else
-    if [ "$status" -ne 0 ]; then
-      failures=$((failures + 1))
-    fi
-  fi
-  # See FAIL_FAST note above
-  if [[ -n "${FAIL_FAST-}" ]]; then
-    if [ "$failures" -ne 0 ]; then
-      >&2 echo "Failed"
-      >&2 cat "$report"
-      exit 1
-    fi
-  fi
-done
-
-if [ "$failures" -ne 0 ]; then
-  echo "$failures failure(s).  See $report"
-  exit 1
+export CPYTHON_DIR="$TOOLS_DIR/$prefix/Lib/test"
+export CPYTHON_EXPECTED_FAILURES="$expected_file"
+if [ -n "${FAIL_FAST-}" ]; then
+  export CPYTHON_FAIL_FAST=1
 fi
+
+echo "Running CPython differential test over $CPYTHON_DIR with PYTHON=$PYTHON"
+(cd "$STRATA_PYTHON_PKG" && lake test -- CpythonDiffTest)
diff --git a/Tools/strata-python/scripts/run_test.sh b/Tools/strata-python/scripts/run_test.sh
deleted file mode 100755
index 57897f1..0000000
--- a/Tools/strata-python/scripts/run_test.sh
+++ /dev/null
@@ -1,33 +0,0 @@
-#!/bin/sh
-# Script to run basic test of strata generator.
-set -e
-
-if [ "$#" -ne 1 ] ; then
-  echo "run_test.sh <input python file>"
-  exit 1
-fi
-
-if [ ! -f "dialects/Python.dialect.st.ion" ] ; then
-  echo "Cannot find Python dialect"
-  exit 1
-fi
-
-test_dir="$PWD/test_results"
-
-strata=../../../StrataCLI/.lake/build/bin/strata
-
-# Dialect files:
-# dialects/Python.dialect.st.ion
-
-input_path=$1
-input_dir=`dirname "$input_path"`
-filename=`basename "$input_path"`
-mkdir -p $test_dir/$input_dir
-
-python=${PYTHON:-python3}
-$python -m strata_python.gen py_to_strata --dialect "dialects/Python.dialect.st.ion" $input_path "$test_dir/$input_dir/$filename.st.ion"
-
-$strata toIon --include "dialects" "$test_dir/$input_dir/$filename.st.ion" "$test_dir/$input_dir/$filename.st.ion2"
-
-# Check whether 'strata toIon' worked ok
-$strata diff --include "dialects" "$test_dir/$input_dir/$filename.st.ion" "$test_dir/$input_dir/$filename.st.ion2"
\ No newline at end of file
diff --git a/lake-manifest.json b/lake-manifest.json
index 8d7c426..c667694 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,12 +1,15 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"type": "path",
+ [{"url": "https://github.com/strata-org/Strata.git",
+   "type": "git",
+   "subDir": null,
    "scope": "",
+   "rev": "e115b8ec9b8be239626cea09eb74ba1103bfc71d",
    "name": "Strata",
    "manifestFile": "lake-manifest.json",
+   "inputRev": null,
    "inherited": false,
-   "dir": "..",
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/plausible.git",
    "type": "git",
@@ -23,7 +26,7 @@
    "name": "StrataDDM",
    "manifestFile": "lake-manifest.json",
    "inherited": true,
-   "dir": "../StrataDDM",
+   "dir": ".lake/packages/Strata/StrataDDM",
    "configFile": "lakefile.toml"}],
  "name": "StrataPython",
  "lakeDir": ".lake"}
diff --git a/lakefile.toml b/lakefile.toml
index 1a229d9..3ca85f5 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -5,7 +5,7 @@ testDriver = "StrataTestMain"
 
 [[require]]
 name = "Strata"
-path = ".."
+git = "https://github.com/strata-org/Strata.git"
 
 [[input_file]]
 name = "PythonDialectIon"