diff --git a/.github/workflows/cbmc.yml b/.github/workflows/cbmc.yml
index cc2ed49..2246cdc 100644
--- a/.github/workflows/cbmc.yml
+++ b/.github/workflows/cbmc.yml
@@ -44,7 +44,7 @@ jobs:
           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/Languages/Laurel/CBMC/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
@@ -68,5 +68,5 @@ jobs:
       - name: Run Python CBMC pipeline tests
         shell: bash
         run: |
-          pip install ./Tools/Python-base ./Tools/strata-python
+          pip install ./.lake/packages/StrataDDM/Python/strata ./Python/strata-python
           ./StrataPythonTest/run_py_cbmc_tests.sh
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index be5ce80..0b08b6a 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -21,6 +21,9 @@ jobs:
         uses: strata-org/Strata/.github/actions/install-cvc5@main
       - name: Install z3
         uses: strata-org/Strata/.github/actions/install-z3@main
+      - uses: actions/setup-python@v6
+        with:
+          python-version: '3.14'
       - 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
@@ -28,40 +31,33 @@ jobs:
         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`.
+      - name: Build StrataPython library
+        # Build the library first to resolve git dependencies (populates
+        # .lake/packages/Strata and .lake/packages/StrataDDM).
         uses: leanprover/lean-action@v1
         with:
-          build-args: StrataPython StrataPythonTest
+          build-args: StrataPython
           use-github-cache: false
           test: false
-      - uses: actions/setup-python@v6
-        with:
-          python-version: '3.14'
-      - name: Build using pip
-        # `strata-base` (Tools/Python-base) and `strata-python` (Tools/strata-python)
-        # both live in this repo.
+      - name: Install Python packages
+        # Install after the Lean build so .lake/packages/StrataDDM is available.
+        # StrataPythonTest/CI/InterpretTests.lean calls Python at compile time.
         run: |
-          pip install ./Tools/Python-base
-          pip install ./Tools/strata-python
+          pip install ./.lake/packages/StrataDDM/Python/strata ./Python/strata-python
+      - name: Build compile-time tests
+        # Building StrataPythonTest runs the compile-time test suite: the tests
+        # are `#guard_msgs` / `#eval` checks that execute during elaboration.
+        run: lake build StrataPythonTest
+        env:
+          PYTHON: 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:
@@ -89,8 +85,7 @@ jobs:
         use-restore-keys: "false"
     - name: Build using pip
       run: |
-        pip install ./Tools/Python-base
-        pip install ./Tools/strata-python
+        pip install ./.lake/packages/StrataDDM/Python/strata ./Python/strata-python
     - name: Install Lean
       uses: leanprover/lean-action@v1
       with:
@@ -157,8 +152,7 @@ jobs:
         use-restore-keys: "false"
     - name: Build using pip
       run: |
-        pip install ./Tools/Python-base
-        pip install ./Tools/strata-python
+        pip install ./.lake/packages/StrataDDM/Python/strata ./Python/strata-python
     - name: Install Lean (for lake env)
       uses: leanprover/lean-action@v1
       with:
@@ -183,8 +177,11 @@ jobs:
       # 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
+      run: |
+        VER=${{ matrix.python_version }}
+        git clone https://github.com/python/cpython.git --branch "$VER" --depth 1 "cpython-$VER"
+        FAIL_FAST=1 ./scripts/run_cpython_tests.sh "$VER"
+      working-directory: Python/strata-python
 
   cbmc:
     needs: build_and_test_lean
diff --git a/lake-manifest.json b/lake-manifest.json
index 433741e..0cf9213 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "7b40c42a9f279ef6aaa9000cfd8d728476c953fa",
+   "rev": "7ba6debc4d2e9637c4a8bd86be0ed91126633856",
    "name": "Strata",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "fbd9f71d6f03f56d71dc0ea4c40fcca7f4ebb6f8",
+   "rev": "18c1ade5cd00b4c955d5b9f341ab70d5573f27ba",
    "name": "StrataDDM",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lakefile.toml b/lakefile.toml
index 6c8dbbe..6509741 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -1,7 +1,7 @@
 name = "StrataPython"
 version = "0.1.0"
 defaultTargets = ["StrataPython"]
-testDriver = "StrataTestMain"
+testDriver = "StrataPythonFrontEndTestMain"
 
 [[require]]
 name = "Strata"
@@ -10,7 +10,7 @@ rev = "main"
 
 [[input_file]]
 name = "PythonDialectIon"
-path = "Tools/strata-python/dialects/Python.dialect.st.ion"
+path = "Python/strata-python/dialects/Python.dialect.st.ion"
 text = true
 
 [[lean_lib]]
@@ -26,13 +26,9 @@ name = "StrataPythonTestExtra"
 globs = ["StrataPythonTestExtra.+"]
 
 [[lean_exe]]
-name = "StrataTestMain"
+name = "StrataPythonFrontEndTestMain"
 needs = ["StrataPython", "StrataPythonTest"]
 
-[[lean_exe]]
-name = "DiffTestCore"
-needs = ["StrataPython"]
-
 [[lean_exe]]
 name = "pyAnalyzeLaurel"
 root = "Scripts.pyAnalyzeLaurel"