From bb74b52daca9200e5bb375108bbf30aae85ebd80 Mon Sep 17 00:00:00 2001
From: Joe Hendrix <joehx@amazon.com>
Date: Mon, 8 Jun 2026 23:45:34 -0700
Subject: [PATCH 1/4] Add CI for standalone StrataPython repo

Port the Python-specific CI from the Strata monorepo into this standalone
repository, adapted for its layout (StrataPython is the repo root).

Fix the Strata dependency: the lakefile required `Strata` at `..`, which
does not exist in the standalone repo. Change it to a git require so lake
clones Strata; the manifest pins the current Strata SHA.

Workflows:
- ci.yml: build_and_test_lean (Python steps), check_pending_python,
  lint_checks, and the build_python matrix (3.11-3.14).
- cbmc.yml: build CBMC from source with the in-repo string-support patch
  plus the Laurel/regex/quantifier patches from the cloned Strata package,
  then run the Python CBMC pipeline tests.

Port the composite actions (install-cvc5/z3, lint actions, lake cache) and
lint scripts, plus CODEOWNERS, dependabot, and a PR template.

Remove the StrataCLI dependency from the CPython differential test: the old
run_test.sh used the `strata` CLI only for an Ion round-trip check. Move
that work into a new Lean test, StrataPythonTestExtra/CpythonDiffTest, which
does the round-trip in-process via the Strata library. run_cpython_tests.sh
keeps the orchestration (clone CPython, pick the version, compute expected
failures) and drives the Lean test; run_test.sh is removed.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 .github/CODEOWNERS                            |   3 +
 .../check-copyright-headers/action.yml        |  20 ++
 .github/actions/check-lean-import/action.yml  |  20 ++
 .github/actions/check-no-panic/action.yml     |  24 +++
 .github/actions/install-cvc5/action.yml       |  52 +++++
 .github/actions/install-z3/action.yml         |  55 +++++
 .github/actions/lint-whitespace/action.yml    |  19 ++
 .github/actions/restore-lake-cache/action.yml |  82 ++++++++
 .github/actions/save-lake-cache/action.yml    |  35 +++
 .github/dependabot.yml                        |   8 +
 .github/pull_request_template.md              |   9 +
 .github/scripts/checkLeanImport.sh            |   7 +
 .github/scripts/checkNoPanic.sh               |  50 +++++
 .github/scripts/check_copyright_headers.py    |  74 +++++++
 .github/scripts/lintWhitespace.sh             |  28 +++
 .github/workflows/cbmc.yml                    |  72 +++++++
 .github/workflows/ci.yml                      | 199 ++++++++++++++++++
 StrataPythonTestExtra/CpythonDiffTest.lean    | 186 ++++++++++++++++
 .../scripts/run_cpython_tests.sh              | 149 ++++++-------
 Tools/strata-python/scripts/run_test.sh       |  33 ---
 lake-manifest.json                            |   9 +-
 lakefile.toml                                 |   2 +-
 22 files changed, 1010 insertions(+), 126 deletions(-)
 create mode 100644 .github/CODEOWNERS
 create mode 100644 .github/actions/check-copyright-headers/action.yml
 create mode 100644 .github/actions/check-lean-import/action.yml
 create mode 100644 .github/actions/check-no-panic/action.yml
 create mode 100644 .github/actions/install-cvc5/action.yml
 create mode 100644 .github/actions/install-z3/action.yml
 create mode 100644 .github/actions/lint-whitespace/action.yml
 create mode 100644 .github/actions/restore-lake-cache/action.yml
 create mode 100644 .github/actions/save-lake-cache/action.yml
 create mode 100644 .github/dependabot.yml
 create mode 100644 .github/pull_request_template.md
 create mode 100755 .github/scripts/checkLeanImport.sh
 create mode 100755 .github/scripts/checkNoPanic.sh
 create mode 100644 .github/scripts/check_copyright_headers.py
 create mode 100755 .github/scripts/lintWhitespace.sh
 create mode 100644 .github/workflows/cbmc.yml
 create mode 100644 .github/workflows/ci.yml
 create mode 100644 StrataPythonTestExtra/CpythonDiffTest.lean
 delete mode 100755 Tools/strata-python/scripts/run_test.sh

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/check-copyright-headers/action.yml b/.github/actions/check-copyright-headers/action.yml
new file mode 100644
index 0000000..bb353b0
--- /dev/null
+++ b/.github/actions/check-copyright-headers/action.yml
@@ -0,0 +1,20 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Check copyright headers
+description: >
+  Verify that all .lean files have the expected copyright header.
+  Downstream repos can add their own checks for other file types.
+
+inputs:
+  directory:
+    description: Root directory to scan (relative to the workspace).
+    required: false
+    default: "."
+
+runs:
+  using: composite
+  steps:
+    - name: Check copyright headers
+      shell: bash
+      run: |
+        python3 "${{ github.action_path }}/../../scripts/check_copyright_headers.py" "${{ inputs.directory }}"
diff --git a/.github/actions/check-lean-import/action.yml b/.github/actions/check-lean-import/action.yml
new file mode 100644
index 0000000..b577722
--- /dev/null
+++ b/.github/actions/check-lean-import/action.yml
@@ -0,0 +1,20 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Check Lean import
+description: >
+  Ensure no .lean file uses a bare "import Lean" statement. Encourages
+  importing only the specific parts of Lean that are needed.
+
+inputs:
+  directory:
+    description: Directory to scan for .lean files (relative to the workspace).
+    required: false
+    default: "."
+
+runs:
+  using: composite
+  steps:
+    - name: Check for bare import Lean
+      shell: bash
+      run: |
+        "${{ github.action_path }}/../../scripts/checkLeanImport.sh" "${{ inputs.directory }}"
diff --git a/.github/actions/check-no-panic/action.yml b/.github/actions/check-no-panic/action.yml
new file mode 100644
index 0000000..1b79e62
--- /dev/null
+++ b/.github/actions/check-no-panic/action.yml
@@ -0,0 +1,24 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Check no panic
+description: >
+  Detect net-new panic! calls introduced in a PR. Only fails when more
+  panics are added than removed. Suppression: add "-- nopanic:ok" on a line.
+  Requires actions/checkout with fetch-depth: 0 (needs full git history to
+  compute the merge base).
+
+inputs:
+  base-ref:
+    description: >
+      Git ref to diff against (e.g. "origin/main"). The script computes
+      the merge base automatically.
+    required: false
+    default: "origin/main"
+
+runs:
+  using: composite
+  steps:
+    - name: Check for new panic! usage
+      shell: bash
+      run: |
+        "${{ github.action_path }}/../../scripts/checkNoPanic.sh" "${{ inputs.base-ref }}"
diff --git a/.github/actions/install-cvc5/action.yml b/.github/actions/install-cvc5/action.yml
new file mode 100644
index 0000000..3ba8055
--- /dev/null
+++ b/.github/actions/install-cvc5/action.yml
@@ -0,0 +1,52 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Install cvc5
+description: >
+  Download a static cvc5 build and put it on the PATH. Supports both
+  x86_64 and aarch64 Linux runners. Consolidates the cvc5 install logic
+  previously duplicated across ci.yml and cbmc.yml; intended to also be
+  adopted by the python-fuzz workflow once that lands (see
+  https://github.com/strata-org/Strata/pull/984).
+
+inputs:
+  version:
+    description: cvc5 release tag (e.g. "1.2.1").
+    required: false
+    default: "1.2.1"
+  install-to:
+    description: >
+      Where to make the cvc5 binary available. One of:
+        "path"    (default) — prepend the unpacked bin/ directory to $GITHUB_PATH.
+        "system"  — sudo cp the cvc5 binary into /usr/local/bin/.
+    required: false
+    default: "path"
+
+runs:
+  using: composite
+  steps:
+    - name: Download cvc5
+      shell: bash
+      run: |
+        set -eu
+        ARCH=$(uname -m)
+        case "$ARCH" in
+          x86_64)         ARCH_NAME="x86_64" ;;
+          aarch64|arm64)  ARCH_NAME="arm64" ;;
+          *) echo "Unsupported architecture: $ARCH" >&2; exit 1 ;;
+        esac
+        URL="https://github.com/cvc5/cvc5/releases/download/cvc5-${{ inputs.version }}/cvc5-Linux-${ARCH_NAME}-static.zip"
+        wget -q "$URL"
+        unzip -q "cvc5-Linux-${ARCH_NAME}-static.zip"
+        chmod +x "cvc5-Linux-${ARCH_NAME}-static/bin/cvc5"
+        case "${{ inputs.install-to }}" in
+          path)
+            echo "$GITHUB_WORKSPACE/cvc5-Linux-${ARCH_NAME}-static/bin/" >> "$GITHUB_PATH"
+            ;;
+          system)
+            sudo cp "cvc5-Linux-${ARCH_NAME}-static/bin/cvc5" /usr/local/bin/
+            ;;
+          *)
+            echo "Unknown install-to value: ${{ inputs.install-to }}" >&2
+            exit 2
+            ;;
+        esac
diff --git a/.github/actions/install-z3/action.yml b/.github/actions/install-z3/action.yml
new file mode 100644
index 0000000..86d6c52
--- /dev/null
+++ b/.github/actions/install-z3/action.yml
@@ -0,0 +1,55 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Install z3
+description: >
+  Download a z3 release and put it on the PATH. Supports x86_64 and
+  aarch64 Linux runners. Consolidates the z3 install logic previously
+  duplicated across ci.yml and cbmc.yml.
+
+inputs:
+  version:
+    description: z3 release tag (e.g. "4.15.2").
+    required: false
+    default: "4.15.2"
+  install-to:
+    description: >
+      Where to make the z3 binary available. One of:
+        "path"    (default) — prepend the unpacked bin/ directory to $GITHUB_PATH.
+        "system"  — sudo cp the z3 binary into /usr/local/bin/.
+    required: false
+    default: "path"
+
+runs:
+  using: composite
+  steps:
+    - name: Download z3
+      shell: bash
+      run: |
+        set -eu
+        ARCH=$(uname -m)
+        case "$ARCH" in
+          x86_64)
+            URL="https://github.com/Z3Prover/z3/releases/download/z3-${{ inputs.version }}/z3-${{ inputs.version }}-x64-glibc-2.39.zip"
+            ARCHIVE_NAME="z3-${{ inputs.version }}-x64-glibc-2.39"
+            ;;
+          aarch64|arm64)
+            URL="https://github.com/Z3Prover/z3/releases/download/z3-${{ inputs.version }}/z3-${{ inputs.version }}-arm64-glibc-2.34.zip"
+            ARCHIVE_NAME="z3-${{ inputs.version }}-arm64-glibc-2.34"
+            ;;
+          *) echo "Unsupported architecture: $ARCH" >&2; exit 1 ;;
+        esac
+        wget -q "$URL"
+        unzip -q "${ARCHIVE_NAME}.zip"
+        chmod +x "${ARCHIVE_NAME}/bin/z3"
+        case "${{ inputs.install-to }}" in
+          path)
+            echo "$GITHUB_WORKSPACE/${ARCHIVE_NAME}/bin/" >> "$GITHUB_PATH"
+            ;;
+          system)
+            sudo cp "${ARCHIVE_NAME}/bin/z3" /usr/local/bin/
+            ;;
+          *)
+            echo "Unknown install-to value: ${{ inputs.install-to }}" >&2
+            exit 2
+            ;;
+        esac
diff --git a/.github/actions/lint-whitespace/action.yml b/.github/actions/lint-whitespace/action.yml
new file mode 100644
index 0000000..0137a3f
--- /dev/null
+++ b/.github/actions/lint-whitespace/action.yml
@@ -0,0 +1,19 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Lint whitespace
+description: >
+  Check .lean files for trailing whitespace and missing final newlines.
+
+inputs:
+  directory:
+    description: Directory to scan for .lean files (relative to the workspace).
+    required: false
+    default: "."
+
+runs:
+  using: composite
+  steps:
+    - name: Check for trailing whitespace
+      shell: bash
+      run: |
+        "${{ github.action_path }}/../../scripts/lintWhitespace.sh" "${{ inputs.directory }}"
diff --git a/.github/actions/restore-lake-cache/action.yml b/.github/actions/restore-lake-cache/action.yml
new file mode 100644
index 0000000..9151866
--- /dev/null
+++ b/.github/actions/restore-lake-cache/action.yml
@@ -0,0 +1,82 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Restore lake cache
+description: >
+  Thin wrapper around actions/cache/restore@v5 that uses the standard
+  Strata cache-key pattern:
+    lake-<os>-<arch>-<lean-toolchain>-<lake-manifest>-<all .st files>-<sha>
+  with three fallback keys dropping each trailing component in turn.
+  Consolidates the ~15-line cache block previously duplicated across
+  ci.yml's build_and_test_lean, check_pending_python, build_python and
+  cbmc.yml; intended to also be adopted by the python-fuzz workflow once
+  that lands (see https://github.com/strata-org/Strata/pull/984).
+
+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 three fallback `restore-keys` so
+      that a near match (same toolchain/manifest/.st files 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') }}-${{ hashFiles('**/*.st') }}-${{ github.sha }}
+        restore-keys: |
+          ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('**/*.st') }}
+          ${{ 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') }}-${{ hashFiles('**/*.st') }}-${{ 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..5754371
--- /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 using the canonical Strata cache-key pattern.
+  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') }}-${{ hashFiles('**/*.st') }}-${{ 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/scripts/checkLeanImport.sh b/.github/scripts/checkLeanImport.sh
new file mode 100755
index 0000000..b3f9063
--- /dev/null
+++ b/.github/scripts/checkLeanImport.sh
@@ -0,0 +1,7 @@
+#!/bin/sh
+# Check to identify modules that inadvertently import all of Lean.
+# We want to encourage only importing parts of Lean when needed.
+
+LINT_DIR="${1:-.}"
+
+! (find "$LINT_DIR" -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Lean$')
\ No newline at end of file
diff --git a/.github/scripts/checkNoPanic.sh b/.github/scripts/checkNoPanic.sh
new file mode 100755
index 0000000..cfeee64
--- /dev/null
+++ b/.github/scripts/checkNoPanic.sh
@@ -0,0 +1,50 @@
+#!/bin/bash
+# Check that new code does not introduce net-new panic! calls.
+# Only raises an error if more panics are added than removed in this PR.
+# To suppress a specific line, add a "-- nopanic:ok" comment on that line.
+
+set -euo pipefail
+
+BASE_REF="${1:-origin/main}"
+
+# Find the merge base so we only inspect lines new to this branch
+MERGE_BASE=$(git merge-base HEAD "$BASE_REF" 2>/dev/null || echo "$BASE_REF")
+
+# Get added lines ('+' prefix) from the diff, restricted to .lean files.
+# Output format: <file>:<line_number>:<content>
+HITS=$(git diff "$MERGE_BASE"...HEAD --unified=0 --diff-filter=ACMR -- '*.lean' \
+  | awk '
+    /^--- /    { next }
+    /^\+\+\+ / { file = substr($0, 7); next }
+    /^@@/      { split($3, a, /[,+]/); lineno = a[2]; next }
+    /^\+/      { print file ":" lineno ":" substr($0, 2); lineno++ }
+  ' \
+  | { \
+      grep -F 'panic!' | \
+      grep -v -- '-- nopanic:ok'; grep_status=$?; \
+      if [ "$grep_status" -gt 1 ]; then exit "$grep_status"; else exit 0; fi; })
+
+if [ -z "$HITS" ]; then
+  echo "OK: No new panic! usage found."
+  exit 0
+fi
+
+ADDED=$(echo "$HITS" | wc -l | tr -d ' ')
+
+# Count removed panic! lines from the same diff
+REMOVED=$(git diff "$MERGE_BASE"...HEAD --unified=0 --diff-filter=ACMR -- '*.lean' \
+  | grep -E '^-[^-]' \
+  | grep -cF 'panic!' || true)
+
+NET=$((ADDED - REMOVED))
+
+if [ "$NET" -gt 0 ]; then
+  echo "ERROR: Net increase of $NET panic! call(s) — use Except/throw instead."
+  echo "  (added: $ADDED, removed: $REMOVED)"
+  echo "To suppress a specific occurrence, add '-- nopanic:ok' on that line."
+  echo ""
+  echo "$HITS"
+  exit 1
+fi
+
+echo "OK: No net increase in panic! usage (added: $ADDED, removed: $REMOVED)."
diff --git a/.github/scripts/check_copyright_headers.py b/.github/scripts/check_copyright_headers.py
new file mode 100644
index 0000000..e983f34
--- /dev/null
+++ b/.github/scripts/check_copyright_headers.py
@@ -0,0 +1,74 @@
+import sys
+from pathlib import Path
+
+def file_starts_with_header(path : Path, header: str) -> bool:
+    with path.open("r") as f:
+        contents = f.read()
+    return contents.startswith(header)
+
+def check_all_source_files(directory: Path, ext: str, header: str) -> bool:
+    """
+    Recursively check all files with extension `ext` in the given directory for copyright headers.
+    
+    Args:
+        directory_path: Path to the directory to check
+        
+    Returns:
+        True if all files have the correct header, False otherwise
+    """
+
+    if not directory.exists():
+        print(f"Error: Directory '{directory}' does not exist")
+        return False
+
+    if not directory.is_dir():
+        print(f"Error: '{directory}' is not a directory")
+        return False
+
+    # Find all .lean files recursively
+    source_files = list(directory.rglob(f"*{ext}"))
+
+    if not source_files:
+        print(f"No {ext} files found in '{directory}'")
+        return True
+
+    print(f"Checking {len(source_files)} {ext} files in '{directory}'...")
+
+    files_without_header = []
+
+    for path in source_files:
+        try:
+            if not file_starts_with_header(path, header):
+                files_without_header.append(path)
+        except Exception as e:
+            print(f"Error reading file '{path}': {e}")
+            files_without_header.append(path)
+
+    if files_without_header:
+        print(f"\nFound {len(files_without_header)} files without proper copyright header:")
+        for file_path in files_without_header:
+            print(f"  - {file_path}")
+        return False
+    else:
+        print(f"All {ext} files have the correct copyright header!")
+        return True
+
+lean_copyright_header = """/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/"""
+
+def main():
+    """Main function to handle command line arguments"""
+    if len(sys.argv) != 2:
+        print("Usage: python check_copyright_headers.py <directory_path>")
+        print("Example: python check_copyright_headers.py /path/to/lean/project")
+        sys.exit(1)
+
+    directory_path = Path(sys.argv[1])
+    success = check_all_source_files(directory_path, ext=".lean", header=lean_copyright_header)
+    sys.exit(0 if success else 1)
+
+if __name__ == "__main__":
+    main()
diff --git a/.github/scripts/lintWhitespace.sh b/.github/scripts/lintWhitespace.sh
new file mode 100755
index 0000000..bd2d692
--- /dev/null
+++ b/.github/scripts/lintWhitespace.sh
@@ -0,0 +1,28 @@
+#!/bin/bash
+set -e
+
+LINT_DIR="${1:-Strata}"
+
+tmpfile=$(mktemp)
+issues_found=0
+
+find "$LINT_DIR" -type f -name "*.lean" | while IFS= read -r file; do
+    # Check for trailing whitespace and print line number if found
+    while IFS=: read -r line_num line; do
+        echo "Trailing whitespace found in $file at line $line_num: $line"
+        echo 1 > "$tmpfile"
+    done < <(grep -n "[[:blank:]]$" "$file")
+
+    # Check if the last line ends with a new line
+    if [ "$(tail -c 1 "$file" | od -c | awk 'NR==1 {print $2}')" != "\n" ]; then
+        echo "Last line does not end with a new line in: $file"
+        echo 1 > "$tmpfile"
+    fi
+done
+
+if [ -f "$tmpfile" ]; then
+    issues_found=$(<"$tmpfile")
+fi
+rm -f "$tmpfile"
+
+exit $issues_found
\ No newline at end of file
diff --git a/.github/workflows/cbmc.yml b/.github/workflows/cbmc.yml
new file mode 100644
index 0000000..1b15bb0
--- /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: ./.github/actions/install-cvc5
+      - name: Install z3
+        uses: ./.github/actions/install-z3
+      - 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..7e8f124
--- /dev/null
+++ b/.github/workflows/ci.yml
@@ -0,0 +1,199 @@
+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: ./.github/actions/install-cvc5
+      - name: Install z3
+        uses: ./.github/actions/install-z3
+      - 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: ./.github/actions/install-cvc5
+      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: ./.github/actions/check-copyright-headers
+      - name: Check for trailing whitespace
+        uses: ./.github/actions/lint-whitespace
+      - name: Check for import Lean
+        uses: ./.github/actions/check-lean-import
+      - name: Check for new panic! usage
+        uses: ./.github/actions/check-no-panic
+        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: ./.github/actions/install-cvc5
+      with:
+        install-to: system
+    - name: Install z3
+      shell: bash
+      run: |
+            pip install z3-solver
+            Z3_PATH=$(python -c "import z3; import os; print(os.path.join(os.path.dirname(z3.__file__), 'lib', 'z3'))")
+            sudo cp "$Z3_PATH" /usr/local/bin/z3 || true
+            # Fallback: install from GitHub release
+            if ! command -v z3 &> /dev/null; then
+              wget https://github.com/Z3Prover/z3/releases/download/z3-4.13.4/z3-4.13.4-x64-glibc-2.35.zip
+              unzip z3-4.13.4-x64-glibc-2.35.zip
+              sudo cp z3-4.13.4-x64-glibc-2.35/bin/z3 /usr/local/bin/
+            fi
+    - 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..a2a6ded 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"

From 5a3bb230a79648d43cbfe1f6ca6441b5de36854f Mon Sep 17 00:00:00 2001
From: Joe Hendrix <joehx@amazon.com>
Date: Tue, 9 Jun 2026 09:42:47 -0700
Subject: [PATCH 2/4] Fix lake cache key instability across jobs

The cache key included hashFiles('**/*.st'), which is empty at restore
(downstream jobs run before .lake exists) but non-empty at save (the
build_and_test_lean job populates .lake, and the cloned Strata git
dependency brings .st files under it). The mismatched keys made every
downstream job fail at restore with fail-on-cache-miss.

Drop the **/*.st component from both restore-lake-cache and
save-lake-cache. This repo has no committed .st files, and the cloned
dependency is already pinned by the lake-manifest.json hash in the key.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 .github/actions/restore-lake-cache/action.yml | 24 +++++++------------
 .github/actions/save-lake-cache/action.yml    |  4 ++--
 2 files changed, 11 insertions(+), 17 deletions(-)

diff --git a/.github/actions/restore-lake-cache/action.yml b/.github/actions/restore-lake-cache/action.yml
index 9151866..8c6a33a 100644
--- a/.github/actions/restore-lake-cache/action.yml
+++ b/.github/actions/restore-lake-cache/action.yml
@@ -2,15 +2,10 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 name: Restore lake cache
 description: >
-  Thin wrapper around actions/cache/restore@v5 that uses the standard
-  Strata cache-key pattern:
-    lake-<os>-<arch>-<lean-toolchain>-<lake-manifest>-<all .st files>-<sha>
-  with three fallback keys dropping each trailing component in turn.
-  Consolidates the ~15-line cache block previously duplicated across
-  ci.yml's build_and_test_lean, check_pending_python, build_python and
-  cbmc.yml; intended to also be adopted by the python-fuzz workflow once
-  that lands (see https://github.com/strata-org/Strata/pull/984).
-
+  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: >
@@ -38,9 +33,9 @@ inputs:
     description: >
       Must be the string `'true'` or `'false'`.
 
-      If `'true'` (default), include three fallback `restore-keys` so
-      that a near match (same toolchain/manifest/.st files but different
-      SHA) is used when no exact-SHA cache exists.
+      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
@@ -66,9 +61,8 @@ runs:
       uses: actions/cache/restore@v5
       with:
         path: ${{ inputs.path }}
-        key: ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('**/*.st') }}-${{ github.sha }}
+        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') }}-${{ hashFiles('**/*.st') }}
           ${{ 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 }}
@@ -78,5 +72,5 @@ runs:
       uses: actions/cache/restore@v5
       with:
         path: ${{ inputs.path }}
-        key: ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('**/*.st') }}-${{ github.sha }}
+        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
index 5754371..4490e8a 100644
--- a/.github/actions/save-lake-cache/action.yml
+++ b/.github/actions/save-lake-cache/action.yml
@@ -2,7 +2,7 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 name: Save lake cache
 description: >
-  Save the lake build cache using the canonical Strata cache-key pattern.
+  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
@@ -32,4 +32,4 @@ runs:
       uses: actions/cache/save@v5
       with:
         path: ${{ inputs.path }}
-        key: ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('**/*.st') }}-${{ github.sha }}
+        key: ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}

From 26d693bf58ec7ff5d3c9825724f944dc09f3f0fa Mon Sep 17 00:00:00 2001
From: Joe Hendrix <joehx@amazon.com>
Date: Tue, 9 Jun 2026 14:11:15 -0700
Subject: [PATCH 3/4] Address PR review: dedup z3 install, lowercase mise tool
 name

- build_python: replace the hand-rolled z3 install (pip + pinned 4.13.4
  wget fallback) with the install-z3 action (install-to: system),
  matching the cvc5 step and removing version drift. Only the z3 binary
  is needed; nothing imports the z3 Python module.
- run_cpython_tests.sh: use mise's lowercase `python@<ver>` tool name so
  it resolves for local dev (CI is unaffected; mise isn't installed
  there and it falls back to python3).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 .github/workflows/ci.yml                         | 14 +++-----------
 Tools/strata-python/scripts/run_cpython_tests.sh |  4 ++--
 2 files changed, 5 insertions(+), 13 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 7e8f124..b98489b 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -168,17 +168,9 @@ jobs:
       with:
         install-to: system
     - name: Install z3
-      shell: bash
-      run: |
-            pip install z3-solver
-            Z3_PATH=$(python -c "import z3; import os; print(os.path.join(os.path.dirname(z3.__file__), 'lib', 'z3'))")
-            sudo cp "$Z3_PATH" /usr/local/bin/z3 || true
-            # Fallback: install from GitHub release
-            if ! command -v z3 &> /dev/null; then
-              wget https://github.com/Z3Prover/z3/releases/download/z3-4.13.4/z3-4.13.4-x64-glibc-2.35.zip
-              unzip z3-4.13.4-x64-glibc-2.35.zip
-              sudo cp z3-4.13.4-x64-glibc-2.35/bin/z3 /usr/local/bin/
-            fi
+      uses: ./.github/actions/install-z3
+      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
diff --git a/Tools/strata-python/scripts/run_cpython_tests.sh b/Tools/strata-python/scripts/run_cpython_tests.sh
index a2a6ded..85b7861 100755
--- a/Tools/strata-python/scripts/run_cpython_tests.sh
+++ b/Tools/strata-python/scripts/run_cpython_tests.sh
@@ -55,8 +55,8 @@ esac
 
 # 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"
+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"
 fi

From db152db6785d4120c960f567b555500266697632 Mon Sep 17 00:00:00 2001
From: Joe Hendrix <joehx@amazon.com>
Date: Tue, 9 Jun 2026 14:44:56 -0700
Subject: [PATCH 4/4] Reference shared actions from Strata repo instead of
 vendoring

Replace the vendored composite actions (install-cvc5, install-z3,
check-copyright-headers, lint-whitespace, check-lean-import,
check-no-panic) with strata-org/Strata/.github/actions/<name>@main
references, and delete the local copies and their backing scripts. This
removes the duplication called out in review.

lint-whitespace gets an explicit `directory: .` since its Strata default
is `Strata`, which does not exist in this repo's layout.

Keep restore-lake-cache and save-lake-cache local: the Strata versions
hash `**/*.st` in the cache key, which is unstable here because the
cloned Strata dependency drops .st files under .lake between restore and
save, breaking fail-on-cache-miss.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 .../check-copyright-headers/action.yml        | 20 -----
 .github/actions/check-lean-import/action.yml  | 20 -----
 .github/actions/check-no-panic/action.yml     | 24 ------
 .github/actions/install-cvc5/action.yml       | 52 -------------
 .github/actions/install-z3/action.yml         | 55 --------------
 .github/actions/lint-whitespace/action.yml    | 19 -----
 .github/scripts/checkLeanImport.sh            |  7 --
 .github/scripts/checkNoPanic.sh               | 50 -------------
 .github/scripts/check_copyright_headers.py    | 74 -------------------
 .github/scripts/lintWhitespace.sh             | 28 -------
 .github/workflows/cbmc.yml                    |  4 +-
 .github/workflows/ci.yml                      | 20 ++---
 12 files changed, 13 insertions(+), 360 deletions(-)
 delete mode 100644 .github/actions/check-copyright-headers/action.yml
 delete mode 100644 .github/actions/check-lean-import/action.yml
 delete mode 100644 .github/actions/check-no-panic/action.yml
 delete mode 100644 .github/actions/install-cvc5/action.yml
 delete mode 100644 .github/actions/install-z3/action.yml
 delete mode 100644 .github/actions/lint-whitespace/action.yml
 delete mode 100755 .github/scripts/checkLeanImport.sh
 delete mode 100755 .github/scripts/checkNoPanic.sh
 delete mode 100644 .github/scripts/check_copyright_headers.py
 delete mode 100755 .github/scripts/lintWhitespace.sh

diff --git a/.github/actions/check-copyright-headers/action.yml b/.github/actions/check-copyright-headers/action.yml
deleted file mode 100644
index bb353b0..0000000
--- a/.github/actions/check-copyright-headers/action.yml
+++ /dev/null
@@ -1,20 +0,0 @@
-# Copyright Strata Contributors
-# SPDX-License-Identifier: Apache-2.0 OR MIT
-name: Check copyright headers
-description: >
-  Verify that all .lean files have the expected copyright header.
-  Downstream repos can add their own checks for other file types.
-
-inputs:
-  directory:
-    description: Root directory to scan (relative to the workspace).
-    required: false
-    default: "."
-
-runs:
-  using: composite
-  steps:
-    - name: Check copyright headers
-      shell: bash
-      run: |
-        python3 "${{ github.action_path }}/../../scripts/check_copyright_headers.py" "${{ inputs.directory }}"
diff --git a/.github/actions/check-lean-import/action.yml b/.github/actions/check-lean-import/action.yml
deleted file mode 100644
index b577722..0000000
--- a/.github/actions/check-lean-import/action.yml
+++ /dev/null
@@ -1,20 +0,0 @@
-# Copyright Strata Contributors
-# SPDX-License-Identifier: Apache-2.0 OR MIT
-name: Check Lean import
-description: >
-  Ensure no .lean file uses a bare "import Lean" statement. Encourages
-  importing only the specific parts of Lean that are needed.
-
-inputs:
-  directory:
-    description: Directory to scan for .lean files (relative to the workspace).
-    required: false
-    default: "."
-
-runs:
-  using: composite
-  steps:
-    - name: Check for bare import Lean
-      shell: bash
-      run: |
-        "${{ github.action_path }}/../../scripts/checkLeanImport.sh" "${{ inputs.directory }}"
diff --git a/.github/actions/check-no-panic/action.yml b/.github/actions/check-no-panic/action.yml
deleted file mode 100644
index 1b79e62..0000000
--- a/.github/actions/check-no-panic/action.yml
+++ /dev/null
@@ -1,24 +0,0 @@
-# Copyright Strata Contributors
-# SPDX-License-Identifier: Apache-2.0 OR MIT
-name: Check no panic
-description: >
-  Detect net-new panic! calls introduced in a PR. Only fails when more
-  panics are added than removed. Suppression: add "-- nopanic:ok" on a line.
-  Requires actions/checkout with fetch-depth: 0 (needs full git history to
-  compute the merge base).
-
-inputs:
-  base-ref:
-    description: >
-      Git ref to diff against (e.g. "origin/main"). The script computes
-      the merge base automatically.
-    required: false
-    default: "origin/main"
-
-runs:
-  using: composite
-  steps:
-    - name: Check for new panic! usage
-      shell: bash
-      run: |
-        "${{ github.action_path }}/../../scripts/checkNoPanic.sh" "${{ inputs.base-ref }}"
diff --git a/.github/actions/install-cvc5/action.yml b/.github/actions/install-cvc5/action.yml
deleted file mode 100644
index 3ba8055..0000000
--- a/.github/actions/install-cvc5/action.yml
+++ /dev/null
@@ -1,52 +0,0 @@
-# Copyright Strata Contributors
-# SPDX-License-Identifier: Apache-2.0 OR MIT
-name: Install cvc5
-description: >
-  Download a static cvc5 build and put it on the PATH. Supports both
-  x86_64 and aarch64 Linux runners. Consolidates the cvc5 install logic
-  previously duplicated across ci.yml and cbmc.yml; intended to also be
-  adopted by the python-fuzz workflow once that lands (see
-  https://github.com/strata-org/Strata/pull/984).
-
-inputs:
-  version:
-    description: cvc5 release tag (e.g. "1.2.1").
-    required: false
-    default: "1.2.1"
-  install-to:
-    description: >
-      Where to make the cvc5 binary available. One of:
-        "path"    (default) — prepend the unpacked bin/ directory to $GITHUB_PATH.
-        "system"  — sudo cp the cvc5 binary into /usr/local/bin/.
-    required: false
-    default: "path"
-
-runs:
-  using: composite
-  steps:
-    - name: Download cvc5
-      shell: bash
-      run: |
-        set -eu
-        ARCH=$(uname -m)
-        case "$ARCH" in
-          x86_64)         ARCH_NAME="x86_64" ;;
-          aarch64|arm64)  ARCH_NAME="arm64" ;;
-          *) echo "Unsupported architecture: $ARCH" >&2; exit 1 ;;
-        esac
-        URL="https://github.com/cvc5/cvc5/releases/download/cvc5-${{ inputs.version }}/cvc5-Linux-${ARCH_NAME}-static.zip"
-        wget -q "$URL"
-        unzip -q "cvc5-Linux-${ARCH_NAME}-static.zip"
-        chmod +x "cvc5-Linux-${ARCH_NAME}-static/bin/cvc5"
-        case "${{ inputs.install-to }}" in
-          path)
-            echo "$GITHUB_WORKSPACE/cvc5-Linux-${ARCH_NAME}-static/bin/" >> "$GITHUB_PATH"
-            ;;
-          system)
-            sudo cp "cvc5-Linux-${ARCH_NAME}-static/bin/cvc5" /usr/local/bin/
-            ;;
-          *)
-            echo "Unknown install-to value: ${{ inputs.install-to }}" >&2
-            exit 2
-            ;;
-        esac
diff --git a/.github/actions/install-z3/action.yml b/.github/actions/install-z3/action.yml
deleted file mode 100644
index 86d6c52..0000000
--- a/.github/actions/install-z3/action.yml
+++ /dev/null
@@ -1,55 +0,0 @@
-# Copyright Strata Contributors
-# SPDX-License-Identifier: Apache-2.0 OR MIT
-name: Install z3
-description: >
-  Download a z3 release and put it on the PATH. Supports x86_64 and
-  aarch64 Linux runners. Consolidates the z3 install logic previously
-  duplicated across ci.yml and cbmc.yml.
-
-inputs:
-  version:
-    description: z3 release tag (e.g. "4.15.2").
-    required: false
-    default: "4.15.2"
-  install-to:
-    description: >
-      Where to make the z3 binary available. One of:
-        "path"    (default) — prepend the unpacked bin/ directory to $GITHUB_PATH.
-        "system"  — sudo cp the z3 binary into /usr/local/bin/.
-    required: false
-    default: "path"
-
-runs:
-  using: composite
-  steps:
-    - name: Download z3
-      shell: bash
-      run: |
-        set -eu
-        ARCH=$(uname -m)
-        case "$ARCH" in
-          x86_64)
-            URL="https://github.com/Z3Prover/z3/releases/download/z3-${{ inputs.version }}/z3-${{ inputs.version }}-x64-glibc-2.39.zip"
-            ARCHIVE_NAME="z3-${{ inputs.version }}-x64-glibc-2.39"
-            ;;
-          aarch64|arm64)
-            URL="https://github.com/Z3Prover/z3/releases/download/z3-${{ inputs.version }}/z3-${{ inputs.version }}-arm64-glibc-2.34.zip"
-            ARCHIVE_NAME="z3-${{ inputs.version }}-arm64-glibc-2.34"
-            ;;
-          *) echo "Unsupported architecture: $ARCH" >&2; exit 1 ;;
-        esac
-        wget -q "$URL"
-        unzip -q "${ARCHIVE_NAME}.zip"
-        chmod +x "${ARCHIVE_NAME}/bin/z3"
-        case "${{ inputs.install-to }}" in
-          path)
-            echo "$GITHUB_WORKSPACE/${ARCHIVE_NAME}/bin/" >> "$GITHUB_PATH"
-            ;;
-          system)
-            sudo cp "${ARCHIVE_NAME}/bin/z3" /usr/local/bin/
-            ;;
-          *)
-            echo "Unknown install-to value: ${{ inputs.install-to }}" >&2
-            exit 2
-            ;;
-        esac
diff --git a/.github/actions/lint-whitespace/action.yml b/.github/actions/lint-whitespace/action.yml
deleted file mode 100644
index 0137a3f..0000000
--- a/.github/actions/lint-whitespace/action.yml
+++ /dev/null
@@ -1,19 +0,0 @@
-# Copyright Strata Contributors
-# SPDX-License-Identifier: Apache-2.0 OR MIT
-name: Lint whitespace
-description: >
-  Check .lean files for trailing whitespace and missing final newlines.
-
-inputs:
-  directory:
-    description: Directory to scan for .lean files (relative to the workspace).
-    required: false
-    default: "."
-
-runs:
-  using: composite
-  steps:
-    - name: Check for trailing whitespace
-      shell: bash
-      run: |
-        "${{ github.action_path }}/../../scripts/lintWhitespace.sh" "${{ inputs.directory }}"
diff --git a/.github/scripts/checkLeanImport.sh b/.github/scripts/checkLeanImport.sh
deleted file mode 100755
index b3f9063..0000000
--- a/.github/scripts/checkLeanImport.sh
+++ /dev/null
@@ -1,7 +0,0 @@
-#!/bin/sh
-# Check to identify modules that inadvertently import all of Lean.
-# We want to encourage only importing parts of Lean when needed.
-
-LINT_DIR="${1:-.}"
-
-! (find "$LINT_DIR" -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Lean$')
\ No newline at end of file
diff --git a/.github/scripts/checkNoPanic.sh b/.github/scripts/checkNoPanic.sh
deleted file mode 100755
index cfeee64..0000000
--- a/.github/scripts/checkNoPanic.sh
+++ /dev/null
@@ -1,50 +0,0 @@
-#!/bin/bash
-# Check that new code does not introduce net-new panic! calls.
-# Only raises an error if more panics are added than removed in this PR.
-# To suppress a specific line, add a "-- nopanic:ok" comment on that line.
-
-set -euo pipefail
-
-BASE_REF="${1:-origin/main}"
-
-# Find the merge base so we only inspect lines new to this branch
-MERGE_BASE=$(git merge-base HEAD "$BASE_REF" 2>/dev/null || echo "$BASE_REF")
-
-# Get added lines ('+' prefix) from the diff, restricted to .lean files.
-# Output format: <file>:<line_number>:<content>
-HITS=$(git diff "$MERGE_BASE"...HEAD --unified=0 --diff-filter=ACMR -- '*.lean' \
-  | awk '
-    /^--- /    { next }
-    /^\+\+\+ / { file = substr($0, 7); next }
-    /^@@/      { split($3, a, /[,+]/); lineno = a[2]; next }
-    /^\+/      { print file ":" lineno ":" substr($0, 2); lineno++ }
-  ' \
-  | { \
-      grep -F 'panic!' | \
-      grep -v -- '-- nopanic:ok'; grep_status=$?; \
-      if [ "$grep_status" -gt 1 ]; then exit "$grep_status"; else exit 0; fi; })
-
-if [ -z "$HITS" ]; then
-  echo "OK: No new panic! usage found."
-  exit 0
-fi
-
-ADDED=$(echo "$HITS" | wc -l | tr -d ' ')
-
-# Count removed panic! lines from the same diff
-REMOVED=$(git diff "$MERGE_BASE"...HEAD --unified=0 --diff-filter=ACMR -- '*.lean' \
-  | grep -E '^-[^-]' \
-  | grep -cF 'panic!' || true)
-
-NET=$((ADDED - REMOVED))
-
-if [ "$NET" -gt 0 ]; then
-  echo "ERROR: Net increase of $NET panic! call(s) — use Except/throw instead."
-  echo "  (added: $ADDED, removed: $REMOVED)"
-  echo "To suppress a specific occurrence, add '-- nopanic:ok' on that line."
-  echo ""
-  echo "$HITS"
-  exit 1
-fi
-
-echo "OK: No net increase in panic! usage (added: $ADDED, removed: $REMOVED)."
diff --git a/.github/scripts/check_copyright_headers.py b/.github/scripts/check_copyright_headers.py
deleted file mode 100644
index e983f34..0000000
--- a/.github/scripts/check_copyright_headers.py
+++ /dev/null
@@ -1,74 +0,0 @@
-import sys
-from pathlib import Path
-
-def file_starts_with_header(path : Path, header: str) -> bool:
-    with path.open("r") as f:
-        contents = f.read()
-    return contents.startswith(header)
-
-def check_all_source_files(directory: Path, ext: str, header: str) -> bool:
-    """
-    Recursively check all files with extension `ext` in the given directory for copyright headers.
-    
-    Args:
-        directory_path: Path to the directory to check
-        
-    Returns:
-        True if all files have the correct header, False otherwise
-    """
-
-    if not directory.exists():
-        print(f"Error: Directory '{directory}' does not exist")
-        return False
-
-    if not directory.is_dir():
-        print(f"Error: '{directory}' is not a directory")
-        return False
-
-    # Find all .lean files recursively
-    source_files = list(directory.rglob(f"*{ext}"))
-
-    if not source_files:
-        print(f"No {ext} files found in '{directory}'")
-        return True
-
-    print(f"Checking {len(source_files)} {ext} files in '{directory}'...")
-
-    files_without_header = []
-
-    for path in source_files:
-        try:
-            if not file_starts_with_header(path, header):
-                files_without_header.append(path)
-        except Exception as e:
-            print(f"Error reading file '{path}': {e}")
-            files_without_header.append(path)
-
-    if files_without_header:
-        print(f"\nFound {len(files_without_header)} files without proper copyright header:")
-        for file_path in files_without_header:
-            print(f"  - {file_path}")
-        return False
-    else:
-        print(f"All {ext} files have the correct copyright header!")
-        return True
-
-lean_copyright_header = """/-
-  Copyright Strata Contributors
-
-  SPDX-License-Identifier: Apache-2.0 OR MIT
--/"""
-
-def main():
-    """Main function to handle command line arguments"""
-    if len(sys.argv) != 2:
-        print("Usage: python check_copyright_headers.py <directory_path>")
-        print("Example: python check_copyright_headers.py /path/to/lean/project")
-        sys.exit(1)
-
-    directory_path = Path(sys.argv[1])
-    success = check_all_source_files(directory_path, ext=".lean", header=lean_copyright_header)
-    sys.exit(0 if success else 1)
-
-if __name__ == "__main__":
-    main()
diff --git a/.github/scripts/lintWhitespace.sh b/.github/scripts/lintWhitespace.sh
deleted file mode 100755
index bd2d692..0000000
--- a/.github/scripts/lintWhitespace.sh
+++ /dev/null
@@ -1,28 +0,0 @@
-#!/bin/bash
-set -e
-
-LINT_DIR="${1:-Strata}"
-
-tmpfile=$(mktemp)
-issues_found=0
-
-find "$LINT_DIR" -type f -name "*.lean" | while IFS= read -r file; do
-    # Check for trailing whitespace and print line number if found
-    while IFS=: read -r line_num line; do
-        echo "Trailing whitespace found in $file at line $line_num: $line"
-        echo 1 > "$tmpfile"
-    done < <(grep -n "[[:blank:]]$" "$file")
-
-    # Check if the last line ends with a new line
-    if [ "$(tail -c 1 "$file" | od -c | awk 'NR==1 {print $2}')" != "\n" ]; then
-        echo "Last line does not end with a new line in: $file"
-        echo 1 > "$tmpfile"
-    fi
-done
-
-if [ -f "$tmpfile" ]; then
-    issues_found=$(<"$tmpfile")
-fi
-rm -f "$tmpfile"
-
-exit $issues_found
\ No newline at end of file
diff --git a/.github/workflows/cbmc.yml b/.github/workflows/cbmc.yml
index 1b15bb0..fe7c641 100644
--- a/.github/workflows/cbmc.yml
+++ b/.github/workflows/cbmc.yml
@@ -13,9 +13,9 @@ jobs:
       - name: Checkout
         uses: actions/checkout@v6
       - name: Install cvc5
-        uses: ./.github/actions/install-cvc5
+        uses: strata-org/Strata/.github/actions/install-cvc5@main
       - name: Install z3
-        uses: ./.github/actions/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
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index b98489b..46a4e4d 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -18,9 +18,9 @@ jobs:
       - name: Checkout
         uses: actions/checkout@v6
       - name: Install cvc5
-        uses: ./.github/actions/install-cvc5
+        uses: strata-org/Strata/.github/actions/install-cvc5@main
       - name: Install z3
-        uses: ./.github/actions/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
@@ -97,7 +97,7 @@ jobs:
         auto-config: false
         build: false
     - name: Install cvc5
-      uses: ./.github/actions/install-cvc5
+      uses: strata-org/Strata/.github/actions/install-cvc5@main
       with:
         install-to: system
     - name: Check pending tests for newly passing
@@ -120,13 +120,15 @@ jobs:
         with:
           fetch-depth: 0
       - name: Check copyright headers
-        uses: ./.github/actions/check-copyright-headers
+        uses: strata-org/Strata/.github/actions/check-copyright-headers@main
       - name: Check for trailing whitespace
-        uses: ./.github/actions/lint-whitespace
+        uses: strata-org/Strata/.github/actions/lint-whitespace@main
+        with:
+          directory: .
       - name: Check for import Lean
-        uses: ./.github/actions/check-lean-import
+        uses: strata-org/Strata/.github/actions/check-lean-import@main
       - name: Check for new panic! usage
-        uses: ./.github/actions/check-no-panic
+        uses: strata-org/Strata/.github/actions/check-no-panic@main
         with:
           base-ref: "origin/${{ github.base_ref || 'main' }}"
 
@@ -164,11 +166,11 @@ jobs:
         build: false
         use-github-cache: false
     - name: Install cvc5
-      uses: ./.github/actions/install-cvc5
+      uses: strata-org/Strata/.github/actions/install-cvc5@main
       with:
         install-to: system
     - name: Install z3
-      uses: ./.github/actions/install-z3
+      uses: strata-org/Strata/.github/actions/install-z3@main
       with:
         install-to: system
     - name: Run PySpec and dispatch tests