diff --git a/.github/workflows/python-fuzz.yml b/.github/workflows/python-fuzz.yml
new file mode 100644
index 0000000000..0a363fe569
--- /dev/null
+++ b/.github/workflows/python-fuzz.yml
@@ -0,0 +1,325 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+#
+# =============================================================================
+# Python Front-End Fuzz Testing
+# =============================================================================
+#
+# This workflow fuzz-tests Strata's Python front-end by generating random
+# Python programs and running them through the Strata pipeline. It is inspired
+# by CBMC's use of CSmith (see .github/workflows/csmith.yaml in the CBMC
+# repository) and by the hypothesmith project (https://github.com/Zac-HD/
+# hypothesmith), which generates syntactically valid Python programs using
+# the Hypothesis property-based testing framework.
+#
+# ## Trigger
+#
+# Runs on pull_request only — not on merge_group or push to main. This is
+# intentional: fuzz tests are non-deterministic and are meant to catch
+# regressions in PRs, not to gate merges or post-merge builds.
+#
+# ## What it tests
+#
+# Two modes run in sequence:
+#
+# 1. **Syntax mode** — Uses hypothesmith to generate syntactically valid
+#    Python from the grammar. Each program is parsed into Strata's Ion
+#    format, round-tripped through `strata toIon`, and diffed. This tests
+#    that the parser pipeline doesn't crash on arbitrary valid Python.
+#
+# 2. **Semantic mode** — Uses a custom generator to produce typed Python
+#    programs with assertions whose expected values are computed by CPython
+#    at generation time (analogous to CSmith computing a checksum). Each
+#    program is first validated with CPython, then run through
+#    `pyAnalyzeLaurel`. If Strata reports a failing assertion on a program
+#    that CPython runs correctly, that's a semantic modelling bug.
+#
+# The `--unrestricted` flag is used, which includes generators for Python
+# constructs beyond what Strata supports today (classes, generators,
+# comprehensions, try/except, match, async, decorators, etc.). Programs
+# that hit unsupported constructs are reported as SKIP, not failures.
+#
+# ## Failure analysis
+#
+# When fuzz tests fail on the PR, the workflow performs a bisection-style
+# analysis by re-running the same tests (same seed) against the merge base:
+#
+#   Pick random seed
+#           │
+#           ▼
+#   Run 10 fuzz tests on PR branch
+#           │
+#       ┌───┴───┐
+#     PASS    FAIL
+#       │       │
+#       ▼       ▼
+#     Done   Save fuzz scripts, checkout merge base,
+#            rebuild strata, re-run with same seed
+#               │
+#           ┌───┴──────────┐
+#       Base FAILS      Base PASSES
+#           │                │
+#           ▼                ▼
+#     Create GitHub      CI FAILS
+#     issue labeled      (regression
+#     'fuzz-bug'          from PR)
+#     (pre-existing
+#      bug, PR not
+#      blocked)
+#
+# ## Reproducibility
+#
+# Every run uses a random seed derived from the current timestamp. The seed
+# is reported in the step name, in the logs, and in all failure messages.
+# To reproduce a failure locally:
+#
+#   cd Tools/Python
+#   ./scripts/hypothesmith.sh 10 <SEED> both --unrestricted
+#
+# The seed controls both the Hypothesis engine (syntax mode) and Python's
+# random module (semantic mode), so identical seeds produce identical
+# programs.
+#
+# ## Files
+#
+# - Tools/Python/scripts/hypothesmith.sh    — Main driver script
+# - Tools/Python/scripts/gen_random_python.py — Program generator
+# - Tools/Python/scripts/gen_unrestricted.py  — Extended generators
+# =============================================================================
+
+name: Python Fuzz
+
+on:
+  pull_request:
+    branches: [main]
+
+jobs:
+  fuzz_python:
+    name: Fuzz-test Python front-end
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      # Needed to create issues for pre-existing bugs.
+      issues: write
+    steps:
+      - name: Checkout PR
+        uses: actions/checkout@v6
+        with:
+          # Full history is needed to find the merge base for failure analysis.
+          fetch-depth: 0
+
+      # Generate a seed from the current nanosecond timestamp. This is
+      # reported in the step name and all log output so that any failure
+      # can be reproduced deterministically.
+      - name: Pick random seed
+        id: seed
+        run: echo "value=$(date +%s%N | cut -c1-10)" >> $GITHUB_OUTPUT
+
+      - name: Install cvc5
+        shell: bash
+        run: |
+          ARCH=$(uname -m)
+          if [ "$ARCH" = "x86_64" ]; then ARCH_NAME="x86_64"
+          elif [ "$ARCH" = "aarch64" ] || [ "$ARCH" = "arm64" ]; then ARCH_NAME="arm64"
+          else echo "Unsupported architecture: $ARCH"; exit 1; fi
+          wget -q https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.1/cvc5-Linux-${ARCH_NAME}-static.zip
+          unzip -q cvc5-Linux-${ARCH_NAME}-static.zip
+          chmod +x cvc5-Linux-${ARCH_NAME}-static/bin/cvc5
+          echo "$GITHUB_WORKSPACE/cvc5-Linux-${ARCH_NAME}-static/bin/" >> $GITHUB_PATH
+
+      # Try to restore a cached Lean build to avoid rebuilding from scratch.
+      - name: Restore lake cache
+        uses: actions/cache/restore@v5
+        with:
+          path: .lake
+          key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('**/*.st') }}-${{ github.sha }}
+          restore-keys: |
+            lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('**/*.st') }}
+            lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
+            lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}
+
+      # Build only the strata executable — skip proofs and other targets
+      # to keep the job fast.
+      - name: Build Strata executables
+        uses: leanprover/lean-action@v1
+        with:
+          use-github-cache: false
+          build-args: 'strata:exe strata'
+          test: false
+
+      - uses: actions/setup-python@v6
+        with:
+          python-version: '3.14'
+
+      # Install the Strata Python bindings (for py_to_strata) and
+      # hypothesmith (for grammar-based program generation).
+      - name: Install Python dependencies
+        run: |
+          python -m venv Tools/Python/.venv
+          Tools/Python/.venv/bin/pip install --quiet -e Tools/Python
+          Tools/Python/.venv/bin/pip install --quiet hypothesmith
+
+      # Run 10 fuzz tests in both syntax and semantic modes with
+      # --unrestricted. The seed is shown in the step name for easy
+      # identification in the GitHub Actions UI.
+      - name: Run fuzz tests on PR (seed=${{ steps.seed.outputs.value }})
+        id: fuzz_pr
+        working-directory: Tools/Python
+        run: |
+          echo "::group::Fuzz test output"
+          set +e
+          ./scripts/hypothesmith.sh 10 ${{ steps.seed.outputs.value }} both --unrestricted 2>&1 | tee /tmp/fuzz_pr.log
+          echo "exit_code=${PIPESTATUS[0]}" >> $GITHUB_OUTPUT
+          echo "::endgroup::"
+
+      # --- Failure analysis ---
+      # If the PR fuzz tests failed, check whether the same failure exists
+      # at the merge base. This distinguishes regressions (PR broke it)
+      # from pre-existing bugs (already broken on main).
+      #
+      # The fuzz scripts are saved before checking out the merge base
+      # because they may not exist there (e.g., if this PR is the one
+      # that introduces the fuzz infrastructure).
+      - name: Analyse failure against merge base
+        id: analyse
+        if: steps.fuzz_pr.outputs.exit_code != '0'
+        run: |
+          echo "PR fuzz tests failed with seed ${{ steps.seed.outputs.value }}"
+          echo ""
+
+          # Save the fuzz scripts from the PR branch — they may not exist
+          # at the merge base.
+          cp -r Tools/Python/scripts /tmp/fuzz_scripts
+
+          # Find and check out the merge base (the common ancestor of the
+          # PR branch and the target branch).
+          MERGE_BASE=$(git merge-base HEAD origin/${{ github.base_ref }})
+          echo "Merge base: $MERGE_BASE"
+          git checkout "$MERGE_BASE"
+
+          # Restore the fuzz scripts into the merge-base working tree.
+          cp /tmp/fuzz_scripts/gen_random_python.py Tools/Python/scripts/
+          cp /tmp/fuzz_scripts/gen_unrestricted.py Tools/Python/scripts/
+          cp /tmp/fuzz_scripts/hypothesmith.sh Tools/Python/scripts/
+          chmod +x Tools/Python/scripts/hypothesmith.sh
+
+          # Rebuild strata at the merge base. This may fail if the Lean
+          # toolchain or dependencies changed significantly between the
+          # merge base and the PR. In that case, we can't determine
+          # whether this is a regression, so we report "inconclusive".
+          if ! lake build strata:exe strata 2>&1 | tail -10; then
+            echo "result=inconclusive" >> $GITHUB_OUTPUT
+            echo "⚠️  Could not build merge base. Cannot determine if this is a regression."
+            exit 0
+          fi
+
+          # Re-run the exact same fuzz tests (same seed, same count, same
+          # modes) against the merge-base build.
+          echo "::group::Merge-base fuzz test output"
+          set +e
+          cd Tools/Python
+          ./scripts/hypothesmith.sh 10 ${{ steps.seed.outputs.value }} both --unrestricted 2>&1 | tee /tmp/fuzz_base.log
+          BASE_EXIT=${PIPESTATUS[0]}
+          echo "::endgroup::"
+
+          if [ $BASE_EXIT -ne 0 ]; then
+            echo "result=pre-existing" >> $GITHUB_OUTPUT
+            echo ""
+            echo "⚠️  Merge base ALSO fails with the same seed."
+            echo "This is a pre-existing bug, not a regression from this PR."
+          else
+            echo "result=regression" >> $GITHUB_OUTPUT
+            echo ""
+            echo "❌ Merge base passes but PR fails."
+            echo "This PR introduced a regression."
+          fi
+
+      # --- Pre-existing bug: file an issue ---
+      # If the merge base also fails, this is a bug that already exists on
+      # main. We create a GitHub issue (with deduplication by seed) so it
+      # gets tracked, but we do NOT fail the CI — the PR author shouldn't
+      # be blocked by a pre-existing bug.
+      - name: Create issue for pre-existing bug
+        if: steps.analyse.outputs.result == 'pre-existing' && github.event.pull_request.head.repo.full_name == github.repository
+        continue-on-error: true
+        uses: actions/github-script@v7
+        with:
+          script: |
+            const seed = '${{ steps.seed.outputs.value }}';
+            const title = `[fuzz] Pre-existing Python front-end bug (seed ${seed})`;
+            // Deduplicate: don't create a second issue for the same seed.
+            const existing = await github.rest.issues.listForRepo({
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              state: 'open',
+              labels: 'fuzz-bug',
+              per_page: 100,
+            });
+            if (existing.data.some(i => i.title.includes(`seed ${seed}`))) {
+              console.log('Issue already exists for this seed, skipping.');
+              return;
+            }
+            // Extract failing source code from the fuzz log (between "--- Source code ---" markers)
+            const fs = require('fs');
+            let sourceSnippet = '';
+            try {
+              const log = fs.readFileSync('/tmp/fuzz_pr.log', 'utf8');
+              const sourceMatch = log.match(/--- Source code ---\n([\s\S]*?)(?=\n---)/);
+              if (sourceMatch) {
+                sourceSnippet = sourceMatch[1].substring(0, 2000);
+              }
+            } catch (e) { /* log not available */ }
+            const sourceSection = sourceSnippet
+              ? [`### Generated program`, '```python', sourceSnippet, '```', '']
+              : [];
+            await github.rest.issues.create({
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              title: title,
+              labels: ['fuzz-bug'],
+              body: [
+                `A fuzz test found a pre-existing failure in the Python front-end.`,
+                ``,
+                `**Seed:** \`${seed}\``,
+                `**PR:** #${context.issue.number}`,
+                `**Merge base also fails:** yes`,
+                ``,
+                ...sourceSection,
+                `### Reproduce`,
+                `\`\`\`bash`,
+                `cd Tools/Python`,
+                `./scripts/hypothesmith.sh 10 ${seed} both --unrestricted`,
+                `\`\`\``,
+                ``,
+                `This bug exists on \`main\` and was not introduced by the PR.`,
+              ].join('\n'),
+            });
+
+      # --- Regression: fail CI ---
+      # The merge base passes but the PR fails — this PR broke something.
+      - name: Fail if PR introduced a regression
+        if: steps.analyse.outputs.result == 'regression'
+        run: |
+          echo "::error::Fuzz test regression detected (seed=${{ steps.seed.outputs.value }}). The merge base passes but this PR fails."
+          echo ""
+          echo "Reproduce locally:"
+          echo "  cd Tools/Python"
+          echo "  ./scripts/hypothesmith.sh 10 ${{ steps.seed.outputs.value }} both --unrestricted"
+          exit 1
+
+      # --- Inconclusive: fail CI conservatively ---
+      # We couldn't build the merge base, so we can't tell if this is a
+      # regression or pre-existing. Fail to be safe.
+      - name: Fail if analysis was inconclusive
+        if: steps.analyse.outputs.result == 'inconclusive'
+        run: |
+          echo "::warning::Fuzz test failed (seed=${{ steps.seed.outputs.value }}) but could not build merge base to determine if this is a regression."
+          echo ""
+          echo "Reproduce locally:"
+          echo "  cd Tools/Python"
+          echo "  ./scripts/hypothesmith.sh 10 ${{ steps.seed.outputs.value }} both --unrestricted"
+          exit 1
+
+      - name: Report seed on success
+        if: steps.fuzz_pr.outputs.exit_code == '0'
+        run: echo "✅ All fuzz tests passed (seed=${{ steps.seed.outputs.value }})"
diff --git a/StrataTest/Fuzz/HypotheSmith.lean b/StrataTest/Fuzz/HypotheSmith.lean
new file mode 100644
index 0000000000..eb02ceaaf8
--- /dev/null
+++ b/StrataTest/Fuzz/HypotheSmith.lean
@@ -0,0 +1,39 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import StrataTest.Util.Python
+
+/-!
+# Lightweight fuzz test via hypothesmith
+
+Runs a small deterministic batch of fuzz tests when the Python tooling
+is available. Skips gracefully otherwise. The full random-seed fuzzing
+lives in `.github/workflows/python-fuzz.yml`.
+-/
+
+open Strata.Python in
+#eval do
+  -- Skip gracefully when Python or strata.gen is not available (e.g. in the
+  -- "Build and test Lean" CI job which doesn't install Python libraries).
+  let pythonCmd ← try findPython3 (minVersion := 11) (maxVersion := 14)
+    catch _ => IO.eprintln "⚠ Fuzz test skipped: Python 3 not found"; return
+  unless ← pythonCheckModule pythonCmd "strata.gen" do
+    IO.eprintln "⚠ Fuzz test skipped: strata.gen not installed"; return
+  unless ← pythonCheckModule pythonCmd "hypothesmith" do
+    IO.eprintln "⚠ Fuzz test skipped: hypothesmith not installed"; return
+
+  -- Run a small deterministic batch (3 tests, fixed seed, both modes)
+  let script := "Tools/Python/scripts/hypothesmith.sh"
+  let result ← IO.Process.output {
+    cmd := "bash"
+    args := #[script, "3", "20260423", "both"]
+    env := #[("PYTHON", pythonCmd.toString)]
+    inheritEnv := true
+  }
+  IO.print result.stdout
+  if result.exitCode != 0 then
+    IO.eprint result.stderr
+    throw <| IO.userError s!"Fuzz test failed (exit code {result.exitCode})"
diff --git a/Tools/Python/scripts/gen_random_python.py b/Tools/Python/scripts/gen_random_python.py
new file mode 100644
index 0000000000..224b6999e5
--- /dev/null
+++ b/Tools/Python/scripts/gen_random_python.py
@@ -0,0 +1,406 @@
+# Copyright Strata Contributors
+#
+#  SPDX-License-Identifier: Apache-2.0 OR MIT
+"""
+Generate random Python programs for fuzz-testing Strata's Python front-end.
+
+This script is the program generator used by hypothesmith.sh. It produces
+Python source files that can be fed through Strata's pipeline to find bugs.
+
+## Modes
+
+### Syntax mode (--mode syntax)
+
+Uses the hypothesmith library (https://github.com/Zac-HD/hypothesmith) to
+generate syntactically valid Python programs from the Python grammar. The
+Hypothesis property-based testing framework drives generation, using its
+grammar-inversion strategy to produce programs that pass CPython's
+``compile()`` function.
+
+Generated programs are filtered by AST node count (--max-nodes) to keep
+them small and debuggable. Programs with fewer than 2 AST nodes (empty
+or trivial) are discarded.
+
+### Semantic mode (--mode semantic)
+
+Uses a custom generator to produce typed Python programs with assertions
+whose expected values are computed by CPython at generation time. This is
+analogous to CSmith computing a checksum: the generated program contains
+its own expected output, so any disagreement between CPython and Strata
+indicates a semantic modelling bug.
+
+Each program is structured as:
+
+    def main():
+        <block 1>
+        <block 2>
+        ...
+    main()
+
+where each block declares typed variables, performs operations, and asserts
+the expected result. For example:
+
+    def main():
+        a: int = 89
+        b: int = -30
+        r: int = a + b
+        assert r == 59, "int add"
+    main()
+
+## Generators
+
+The **base generators** (always included) cover constructs known to work
+in Strata today:
+  - Integer arithmetic (+, -, *)
+  - Integer comparisons (<, <=, >, >=, ==, !=)
+  - Boolean logic (and, or, not)
+  - String concatenation
+  - If/else branching
+  - Floor division (//) and modulo (%)
+  - Unary negation
+
+The **unrestricted generators** (--unrestricted flag) add ~60 generators
+for constructs that may be beyond Strata's current support. See
+gen_unrestricted.py for the full list. Programs using unsupported
+constructs will be reported as SKIP by hypothesmith.sh, not as failures.
+
+## Reproducibility
+
+Both modes are fully deterministic given the same --seed value:
+  - Syntax mode: sets HYPOTHESIS_SEED and uses derandomize=True
+  - Semantic mode: seeds Python's random module
+
+## Usage
+
+    python gen_random_python.py --mode syntax --output-dir /tmp/fuzz --seed 42
+    python gen_random_python.py --mode semantic --output-dir /tmp/fuzz --seed 42
+    python gen_random_python.py --mode semantic --output-dir /tmp/fuzz --seed 42 --unrestricted
+
+## Options
+
+    --mode {syntax,semantic}   Generation mode (required)
+    --output-dir DIR           Directory for generated .py files (required)
+    --max-examples N           Number of programs to generate (default: 100)
+    --max-nodes N              Max AST nodes per program, syntax mode only (default: 50)
+    --seed S                   Random seed for reproducibility
+    --unrestricted             Include generators beyond what Strata supports today
+"""
+
+import argparse
+import ast
+import os
+import random
+import sys
+from pathlib import Path
+
+
+# =============================================================================
+# Syntax mode
+# =============================================================================
+
+def gen_syntax(args):
+    """Generate syntactically valid Python via hypothesmith.
+
+    Uses hypothesmith's ``from_grammar()`` strategy, which inverts the Python
+    grammar to produce random valid source code. The ``auto_target=True``
+    option enables Hypothesis's hill-climbing search to drive toward larger
+    and more complex programs over time.
+
+    Programs are filtered to have between 2 and ``max_nodes`` AST nodes.
+    This keeps them small enough to debug while still being non-trivial.
+    """
+    import hypothesmith
+    from hypothesis import given, settings, HealthCheck, Phase
+
+    out = Path(args.output_dir)
+    out.mkdir(parents=True, exist_ok=True)
+    count = [0]
+
+    @settings(
+        max_examples=args.max_examples,
+        suppress_health_check=[HealthCheck.too_slow, HealthCheck.filter_too_much],
+        database=None,
+        # When a seed is provided, use derandomize mode so that the same
+        # seed always produces the same sequence of examples.
+        derandomize=args.seed is not None,
+        phases=[Phase.generate],
+    )
+    @given(source_code=hypothesmith.from_grammar(auto_target=True))
+    def collect(source_code):
+        try:
+            tree = ast.parse(source_code)
+            nodes = len(list(ast.walk(tree)))
+        except SyntaxError:
+            return
+        # Skip trivial programs (empty files, bare comments).
+        if nodes < 2:
+            return
+        # Skip programs that are too large to debug easily.
+        if nodes > args.max_nodes:
+            return
+        idx = count[0]
+        count[0] += 1
+        p = out / f"fuzz_syntax_{idx:04d}.py"
+        p.write_text(source_code)
+
+    if args.seed is not None:
+        os.environ["HYPOTHESIS_SEED"] = str(args.seed)
+    collect()
+    print(f"Generated {count[0]} syntax-mode programs in {out}")
+
+
+# =============================================================================
+# Semantic mode — base generators
+# =============================================================================
+# Each generator function returns a string containing one or more indented
+# Python statements (at 4-space indent) that declare variables, perform
+# operations, and assert the expected result. The expected values are
+# computed by CPython at generation time, so any disagreement with Strata
+# indicates a bug in Strata's semantic model.
+
+def _rand_int():
+    """Random integer in [-100, 100]."""
+    return random.randint(-100, 100)
+
+def _rand_bool():
+    """Random boolean."""
+    return random.choice([True, False])
+
+def _rand_str():
+    """Random short string from a fixed vocabulary."""
+    return random.choice(["hello", "world", "foo", "bar", "", "abc", "x"])
+
+def _gen_int_arithmetic():
+    """Integer addition, subtraction, or multiplication."""
+    a, b = _rand_int(), _rand_int()
+    op_name, op_sym, result_fn = random.choice([
+        ("add", "+", lambda a, b: a + b),
+        ("sub", "-", lambda a, b: a - b),
+        ("mul", "*", lambda a, b: a * b),
+    ])
+    result = result_fn(a, b)
+    return (
+        f"    a: int = {a}\n"
+        f"    b: int = {b}\n"
+        f"    r: int = a {op_sym} b\n"
+        f'    assert r == {result}, "int {op_name}"\n'
+    )
+
+def _gen_int_comparison():
+    """Integer comparison with all six operators."""
+    a, b = _rand_int(), _rand_int()
+    op_sym, result = random.choice([
+        ("<", a < b), ("<=", a <= b), (">", a > b),
+        (">=", a >= b), ("==", a == b), ("!=", a != b),
+    ])
+    return (
+        f"    a: int = {a}\n"
+        f"    b: int = {b}\n"
+        f'    assert (a {op_sym} b) == {result}, "int cmp"\n'
+    )
+
+def _gen_bool_logic():
+    """Boolean and/or."""
+    a, b = _rand_bool(), _rand_bool()
+    op_name, op_sym, result_fn = random.choice([
+        ("and", "and", lambda a, b: a and b),
+        ("or", "or", lambda a, b: a or b),
+    ])
+    result = result_fn(a, b)
+    return (
+        f"    a: bool = {a}\n"
+        f"    b: bool = {b}\n"
+        f"    r: bool = a {op_sym} b\n"
+        f'    assert r == {result}, "bool {op_name}"\n'
+    )
+
+def _gen_str_concat():
+    """String concatenation."""
+    a, b = _rand_str(), _rand_str()
+    result = a + b
+    return (
+        f"    a: str = {a!r}\n"
+        f"    b: str = {b!r}\n"
+        f"    r: str = a + b\n"
+        f'    assert r == {result!r}, "str concat"\n'
+    )
+
+def _gen_if_else():
+    """If/else with a known branch outcome, using compound boolean conditions."""
+    a, b = _rand_int(), _rand_int()
+    # Pick a random condition style
+    style = random.choice(["simple", "and", "or", "not", "none_check"])
+    if style == "simple":
+        cond_val = _rand_bool()
+        cond_expr = str(cond_val)
+    elif style == "and":
+        x, y = _rand_bool(), _rand_bool()
+        cond_val = x and y
+        cond_expr = f"{x} and {y}"
+    elif style == "or":
+        x, y = _rand_bool(), _rand_bool()
+        cond_val = x or y
+        cond_expr = f"{x} or {y}"
+    elif style == "not":
+        x = _rand_bool()
+        cond_val = not x
+        cond_expr = f"not {x}"
+    else:  # none_check
+        use_none = _rand_bool()
+        if use_none:
+            cond_val = False
+            cond_expr = "None is not None"
+        else:
+            cond_val = True
+            cond_expr = "None is None"
+    expected = a if cond_val else b
+    return (
+        f"    if {cond_expr}:\n"
+        f"        r: int = {a}\n"
+        f"    else:\n"
+        f"        r: int = {b}\n"
+        f'    assert r == {expected}, "if_else"\n'
+    )
+
+def _gen_floor_div():
+    """Floor division (Python's // operator)."""
+    a = _rand_int()
+    b = random.choice([x for x in range(-10, 11) if x != 0])
+    result = a // b
+    return (
+        f"    a: int = {a}\n"
+        f"    b: int = {b}\n"
+        f"    r: int = a // b\n"
+        f'    assert r == {result}, "floor div"\n'
+    )
+
+def _gen_modulo():
+    """Modulo (Python's % operator, which uses floored division)."""
+    a = _rand_int()
+    b = random.choice([x for x in range(-10, 11) if x != 0])
+    result = a % b
+    return (
+        f"    a: int = {a}\n"
+        f"    b: int = {b}\n"
+        f"    r: int = a % b\n"
+        f'    assert r == {result}, "modulo"\n'
+    )
+
+def _gen_negation():
+    """Unary negation."""
+    a = _rand_int()
+    return (
+        f"    a: int = {a}\n"
+        f"    r: int = -a\n"
+        f'    assert r == {-a}, "negation"\n'
+    )
+
+def _gen_not():
+    """Boolean not."""
+    a = _rand_bool()
+    return (
+        f"    a: bool = {a}\n"
+        f"    r: bool = not a\n"
+        f'    assert r == {not a}, "bool not"\n'
+    )
+
+# The base generator list — only constructs known to work in Strata today.
+GENERATORS = [
+    _gen_int_arithmetic,
+    _gen_int_comparison,
+    _gen_bool_logic,
+    _gen_str_concat,
+    _gen_if_else,
+    _gen_floor_div,
+    _gen_modulo,
+    _gen_negation,
+    _gen_not,
+]
+
+
+def _get_generators(unrestricted):
+    """Return the list of generators to use.
+
+    With --unrestricted, loads the extended generators from
+    gen_unrestricted.py (in the same directory) and appends them to the
+    base list. This produces programs using Python constructs that Strata
+    may not support yet, which is useful for discovering coverage gaps.
+    """
+    if not unrestricted:
+        return GENERATORS
+    import importlib.util
+    spec = importlib.util.spec_from_file_location(
+        "gen_unrestricted",
+        os.path.join(os.path.dirname(__file__), "gen_unrestricted.py"))
+    mod = importlib.util.module_from_spec(spec)
+    spec.loader.exec_module(mod)
+    return GENERATORS + mod.UNRESTRICTED_GENERATORS
+
+
+# =============================================================================
+# Semantic mode — program assembly
+# =============================================================================
+
+def gen_semantic(args):
+    """Generate typed Python programs with known-true assertions.
+
+    Each program contains 1–5 randomly chosen blocks, wrapped in a
+    ``def main(): ... main()`` structure to match Strata's test convention.
+    The blocks are independent — each declares its own variables and asserts
+    its own expected result.
+    """
+    out = Path(args.output_dir)
+    out.mkdir(parents=True, exist_ok=True)
+
+    if args.seed is not None:
+        random.seed(args.seed)
+
+    generators = _get_generators(args.unrestricted)
+
+    for i in range(args.max_examples):
+        # Pick 1–5 random blocks per program.
+        n_blocks = random.randint(1, 5)
+        blocks = [random.choice(generators)() for _ in range(n_blocks)]
+
+        # Wrap in a function and call it (matches Strata test convention).
+        body = "\n".join(blocks)
+        program = f"def main():\n{body}\nmain()\n"
+
+        p = out / f"fuzz_semantic_{i:04d}.py"
+        p.write_text(program)
+
+    print(f"Generated {args.max_examples} semantic-mode programs in {out}")
+
+
+# =============================================================================
+# CLI
+# =============================================================================
+
+def main():
+    parser = argparse.ArgumentParser(
+        description=__doc__,
+        formatter_class=argparse.RawDescriptionHelpFormatter)
+    parser.add_argument("--mode", choices=["syntax", "semantic"], required=True,
+                        help="Generation mode: 'syntax' for grammar-based, "
+                             "'semantic' for typed programs with assertions")
+    parser.add_argument("--output-dir", required=True,
+                        help="Directory for generated .py files (created if needed)")
+    parser.add_argument("--max-examples", type=int, default=100,
+                        help="Number of programs to generate (default: 100)")
+    parser.add_argument("--max-nodes", type=int, default=50,
+                        help="Max AST nodes per program, syntax mode only (default: 50)")
+    parser.add_argument("--seed", type=int, default=None,
+                        help="Random seed for reproducibility")
+    parser.add_argument("--unrestricted", action="store_true",
+                        help="Include generators for Python constructs beyond "
+                             "what Strata supports today")
+    args = parser.parse_args()
+
+    if args.mode == "syntax":
+        gen_syntax(args)
+    else:
+        gen_semantic(args)
+
+
+if __name__ == "__main__":
+    main()
diff --git a/Tools/Python/scripts/gen_unrestricted.py b/Tools/Python/scripts/gen_unrestricted.py
new file mode 100644
index 0000000000..07e3cf984f
--- /dev/null
+++ b/Tools/Python/scripts/gen_unrestricted.py
@@ -0,0 +1,820 @@
+# Copyright Strata Contributors
+#
+#  SPDX-License-Identifier: Apache-2.0 OR MIT
+"""Unrestricted Python program generators for fuzz testing.
+
+This module contains ~60 generators that produce Python code blocks using
+constructs that may be beyond what Strata supports today. It is loaded by
+gen_random_python.py when the --unrestricted flag is passed.
+
+Each generator function returns a string of indented Python statements
+(4-space indent) that can be placed inside a ``def main():`` body. Every
+block includes at least one ``assert`` whose expected value is computed by
+CPython at generation time. If Strata's verifier disagrees with CPython
+on any of these assertions, that indicates a semantic modelling bug.
+
+## Categories of generators
+
+### Operators
+  - Bitwise: &, |, ^, ~ (gen_bitwise, gen_bitnot)
+  - Shifts: <<, >> (gen_shift)
+  - Power: ** (gen_power)
+  - Augmented assignment: +=, -=, *= (gen_augmented_assign)
+
+### Expressions
+  - Ternary: x if cond else y (gen_ternary)
+  - Chained comparisons: a <= b <= c (gen_chained_cmp)
+  - F-strings (gen_fstring)
+  - Lambda (gen_lambda)
+  - Walrus operator := (gen_walrus, gen_walrus_while)
+
+### Data structures
+  - Lists: create, index, slice, concat, in, append (gen_list_*)
+  - Dicts: create, access, in (gen_dict_*)
+  - Sets: union, intersection (gen_set_ops)
+  - Tuple unpacking, star unpacking (gen_tuple_unpack, gen_star_unpack)
+  - Multiple assignment / swap (gen_multi_assign)
+
+### Strings
+  - len, indexing, multiply, methods (upper/lower/strip), format
+
+### Control flow
+  - For loops over lists and range (gen_for_sum, gen_for_range)
+  - While loops (gen_while_countdown)
+  - Break (gen_break)
+  - Nested if, elif chains (gen_nested_if, gen_elif)
+  - Nested loops (gen_nested_loop)
+
+### Functions
+  - Nested calls (gen_nested_call)
+  - Default arguments (gen_default_args)
+  - *args, **kwargs (gen_varargs, gen_kwargs)
+  - Recursion (gen_recursion)
+  - Decorators (gen_decorator)
+  - Generators / yield (gen_generator)
+
+### Classes
+  - Basic class with __init__ (gen_class_basic)
+  - Class with methods (gen_class_method)
+
+### Exception handling
+  - try/except (gen_try_except)
+  - try/except/else (gen_try_except_else)
+  - try/finally (gen_try_finally)
+  - Multiple except clauses (gen_multi_except)
+  - raise (gen_raise)
+
+### Other
+  - None checks, Optional type (gen_none_check, gen_optional)
+  - isinstance (gen_isinstance)
+  - Type conversions: int(), str(), bool(), float(), list() (gen_type_conv)
+  - With statement / context managers (gen_with_stmt)
+  - Nonlocal (gen_nonlocal)
+  - Pass, del (gen_pass, gen_del)
+  - Async def / asyncio.run (gen_async_def)
+  - Match statement, Python 3.10+ (gen_match)
+
+## Adding new generators
+
+To add a new generator:
+1. Write a function that returns a string of 4-space-indented Python
+   statements including at least one assert with a CPython-computed
+   expected value.
+2. Test it: ``python3 -c "exec('def main():\\n' + gen_your_thing() + 'main()')"``
+3. Add it to the UNRESTRICTED_GENERATORS list at the bottom.
+"""
+
+import random
+
+# ---------------------------------------------------------------------------
+# Helpers — shared random value generators
+# ---------------------------------------------------------------------------
+
+def _rand_int():
+    """Random integer in [-100, 100]."""
+    return random.randint(-100, 100)
+
+def _rand_bool():
+    """Random boolean."""
+    return random.choice([True, False])
+
+def _rand_str():
+    """Random short string from a fixed vocabulary."""
+    return random.choice(["hello", "world", "foo", "bar", "", "abc", "x"])
+
+def _nonzero():
+    """Random non-zero integer in [-10, 10]."""
+    return random.choice([x for x in range(-10, 11) if x != 0])
+
+def _rand_var(prefix="v"):
+    """Random variable name like v42."""
+    return f"{prefix}{random.randint(0, 99)}"
+
+# ---------------------------------------------------------------------------
+# Operators
+# ---------------------------------------------------------------------------
+
+def gen_bitwise():
+    a, b = _rand_int(), _rand_int()
+    op, sym = random.choice([("and", "&"), ("or", "|"), ("xor", "^")])
+    r = eval(f"{a} {sym} {b}")
+    return f"    assert ({a} {sym} {b}) == {r}, \"bitwise {op}\"\n"
+
+def gen_shift():
+    a = random.randint(0, 100)
+    b = random.randint(0, 8)
+    op, sym = random.choice([("lshift", "<<"), ("rshift", ">>")])
+    r = eval(f"{a} {sym} {b}")
+    return f"    assert ({a} {sym} {b}) == {r}, \"{op}\"\n"
+
+def gen_bitnot():
+    """Bitwise NOT (~)."""
+    a = _rand_int()
+    return f"    assert ~{a} == {~a}, \"bitnot\"\n"
+
+# --- Power ---
+
+def gen_power():
+    """Exponentiation (**). Uses non-negative base to avoid precedence issues
+    with unary minus (``-2 ** 2`` is ``-(2**2)`` in Python)."""
+    base = random.randint(0, 5)
+    exp = random.randint(0, 4)
+    r = base ** exp
+    return f"    assert {base} ** {exp} == {r}, \"power\"\n"
+
+# --- Augmented assignment ---
+
+def gen_augmented_assign():
+    a = _rand_int()
+    b = _rand_int()
+    op, sym = random.choice([("+", "+="), ("-", "-="), ("*", "*=")])
+    r = eval(f"{a} {op} {b}")
+    return (
+        f"    x: int = {a}\n"
+        f"    x {sym} {b}\n"
+        f'    assert x == {r}, "augmented {sym}"\n'
+    )
+
+# --- Ternary expression ---
+
+def gen_ternary():
+    cond = _rand_bool()
+    a, b = _rand_int(), _rand_int()
+    r = a if cond else b
+    return f"    assert ({a} if {cond} else {b}) == {r}, \"ternary\"\n"
+
+# --- Multiple assignment / swap ---
+
+def gen_multi_assign():
+    a, b = _rand_int(), _rand_int()
+    return (
+        f"    x: int = {a}\n"
+        f"    y: int = {b}\n"
+        f"    x, y = y, x\n"
+        f'    assert x == {b} and y == {a}, "swap"\n'
+    )
+
+# --- List operations ---
+
+def gen_list_create():
+    elems = [_rand_int() for _ in range(random.randint(1, 5))]
+    return (
+        f"    lst: list = {elems}\n"
+        f'    assert len(lst) == {len(elems)}, "list len"\n'
+    )
+
+def gen_list_index():
+    elems = [_rand_int() for _ in range(random.randint(2, 5))]
+    idx = random.randint(0, len(elems) - 1)
+    return (
+        f"    lst: list = {elems}\n"
+        f'    assert lst[{idx}] == {elems[idx]}, "list index"\n'
+    )
+
+def gen_list_concat():
+    a = [_rand_int() for _ in range(random.randint(1, 3))]
+    b = [_rand_int() for _ in range(random.randint(1, 3))]
+    return (
+        f"    a: list = {a}\n"
+        f"    b: list = {b}\n"
+        f'    assert a + b == {a + b}, "list concat"\n'
+    )
+
+def gen_list_slice():
+    elems = [_rand_int() for _ in range(random.randint(3, 6))]
+    i = random.randint(0, len(elems) - 2)
+    j = random.randint(i + 1, len(elems))
+    return (
+        f"    lst: list = {elems}\n"
+        f'    assert lst[{i}:{j}] == {elems[i:j]}, "list slice"\n'
+    )
+
+def gen_list_in():
+    elems = [_rand_int() for _ in range(random.randint(2, 5))]
+    target = random.choice(elems)
+    return (
+        f"    lst: list = {elems}\n"
+        f'    assert {target} in lst, "list in"\n'
+    )
+
+def gen_list_append():
+    elems = [_rand_int() for _ in range(random.randint(1, 3))]
+    v = _rand_int()
+    return (
+        f"    lst: list = {elems}\n"
+        f"    lst.append({v})\n"
+        f'    assert lst == {elems + [v]}, "list append"\n'
+    )
+
+# --- Dict operations ---
+
+def gen_dict_create():
+    keys = random.sample(["a", "b", "c", "d", "e"], random.randint(1, 4))
+    d = {k: _rand_int() for k in keys}
+    # {len(d)} is evaluated at generation time, producing e.g. "assert len(d) == 3"
+    return (
+        f"    d: dict = {d}\n"
+        f'    assert len(d) == {len(d)}, "dict len"\n'
+    )
+
+def gen_dict_access():
+    keys = random.sample(["a", "b", "c", "d"], random.randint(2, 4))
+    d = {k: _rand_int() for k in keys}
+    k = random.choice(keys)
+    return (
+        f"    d: dict = {d}\n"
+        f'    assert d[{k!r}] == {d[k]}, "dict access"\n'
+    )
+
+def gen_dict_in():
+    keys = random.sample(["a", "b", "c", "d"], random.randint(2, 4))
+    d = {k: _rand_int() for k in keys}
+    k = random.choice(keys)
+    return (
+        f"    d: dict = {d}\n"
+        f'    assert {k!r} in d, "dict in"\n'
+    )
+
+# --- String operations ---
+
+def gen_str_len():
+    s = _rand_str()
+    return f'    assert len({s!r}) == {len(s)}, "str len"\n'
+
+def gen_str_index():
+    s = random.choice(["hello", "world", "foobar", "abc"])
+    i = random.randint(0, len(s) - 1)
+    return f'    assert {s!r}[{i}] == {s[i]!r}, "str index"\n'
+
+def gen_str_multiply():
+    s = random.choice(["ab", "x", "hi"])
+    n = random.randint(0, 4)
+    return f'    assert {s!r} * {n} == {(s * n)!r}, "str mul"\n'
+
+def gen_str_methods():
+    s = random.choice(["Hello", "WORLD", "foo Bar", "abc"])
+    method = random.choice(["upper", "lower", "strip"])
+    r = getattr(s, method)()
+    return f'    assert {s!r}.{method}() == {r!r}, "str {method}"\n'
+
+# --- For loops ---
+
+def gen_for_sum():
+    elems = [random.randint(0, 20) for _ in range(random.randint(2, 5))]
+    return (
+        f"    total: int = 0\n"
+        f"    for x in {elems}:\n"
+        f"        total = total + x\n"
+        f'    assert total == {sum(elems)}, "for sum"\n'
+    )
+
+def gen_for_range():
+    n = random.randint(1, 10)
+    return (
+        f"    total: int = 0\n"
+        f"    for i in range({n}):\n"
+        f"        total = total + i\n"
+        f'    assert total == {sum(range(n))}, "for range"\n'
+    )
+
+# --- While loops ---
+
+def gen_while_countdown():
+    n = random.randint(1, 10)
+    return (
+        f"    n: int = {n}\n"
+        f"    count: int = 0\n"
+        f"    while n > 0:\n"
+        f"        count = count + 1\n"
+        f"        n = n - 1\n"
+        f'    assert count == {n}, "while countdown"\n'
+    )
+
+# --- Break / continue ---
+
+def gen_break():
+    elems = list(range(1, random.randint(4, 8)))
+    stop = random.choice(elems[1:])
+    expected = sum(x for x in elems if x < stop)
+    return (
+        f"    total: int = 0\n"
+        f"    for x in {elems}:\n"
+        f"        if x == {stop}:\n"
+        f"            break\n"
+        f"        total = total + x\n"
+        f'    assert total == {expected}, "break"\n'
+    )
+
+# --- Nested if ---
+
+def gen_nested_if():
+    a, b = _rand_int(), _rand_int()
+    if a > 0:
+        if b > 0:
+            r = 1
+        else:
+            r = 2
+    else:
+        r = 3
+    return (
+        f"    a: int = {a}\n"
+        f"    b: int = {b}\n"
+        f"    if a > 0:\n"
+        f"        if b > 0:\n"
+        f"            r: int = 1\n"
+        f"        else:\n"
+        f"            r: int = 2\n"
+        f"    else:\n"
+        f"        r: int = 3\n"
+        f'    assert r == {r}, "nested if"\n'
+    )
+
+# --- Elif chains ---
+
+def gen_elif():
+    a = _rand_int()
+    if a > 0:
+        r = "pos"
+    elif a < 0:
+        r = "neg"
+    else:
+        r = "zero"
+    return (
+        f"    a: int = {a}\n"
+        f"    if a > 0:\n"
+        f"        r: str = \"pos\"\n"
+        f"    elif a < 0:\n"
+        f"        r: str = \"neg\"\n"
+        f"    else:\n"
+        f"        r: str = \"zero\"\n"
+        f'    assert r == {r!r}, "elif"\n'
+    )
+
+# --- Multiple return values / tuple unpacking ---
+
+def gen_tuple_unpack():
+    a, b, c = _rand_int(), _rand_int(), _rand_int()
+    return (
+        f"    a, b, c = {a}, {b}, {c}\n"
+        f'    assert a == {a} and b == {b} and c == {c}, "tuple unpack"\n'
+    )
+
+# --- Chained comparisons ---
+
+def gen_chained_cmp():
+    a, b, c = sorted([_rand_int() for _ in range(3)])
+    return f'    assert {a} <= {b} <= {c}, "chained cmp"\n'
+
+# --- None checks ---
+
+def gen_none_check():
+    use_none = _rand_bool()
+    val = "None" if use_none else str(_rand_int())
+    is_none = use_none
+    return (
+        f"    x = {val}\n"
+        f'    assert (x is None) == {is_none}, "none check"\n'
+    )
+
+# --- Optional type ---
+
+def gen_optional():
+    from typing import Optional
+    use_none = _rand_bool()
+    if use_none:
+        return (
+            f"    from typing import Optional\n"
+            f"    x: Optional[int] = None\n"
+            f'    assert x is None, "optional none"\n'
+        )
+    else:
+        v = _rand_int()
+        return (
+            f"    from typing import Optional\n"
+            f"    x: Optional[int] = {v}\n"
+            f'    assert x == {v}, "optional value"\n'
+        )
+
+# --- Classes ---
+
+def gen_class_basic():
+    x = _rand_int()
+    return (
+        f"    class Pt:\n"
+        f"        def __init__(self):\n"
+        f"            self.x: int = {x}\n"
+        f"    p = Pt()\n"
+        f'    assert p.x == {x}, "class field"\n'
+    )
+
+def gen_class_method():
+    a, b = _rand_int(), _rand_int()
+    return (
+        f"    class Adder:\n"
+        f"        def __init__(self):\n"
+        f"            self.val: int = {a}\n"
+        f"        def add(self, n: int) -> int:\n"
+        f"            return self.val + n\n"
+        f"    obj = Adder()\n"
+        f'    assert obj.add({b}) == {a + b}, "class method"\n'
+    )
+
+# --- Nested function calls ---
+
+def gen_nested_call():
+    a, b = _rand_int(), _rand_int()
+    return (
+        f"    def add(x: int, y: int) -> int:\n"
+        f"        return x + y\n"
+        f"    def double(x: int) -> int:\n"
+        f"        return x * 2\n"
+        f'    assert double(add({a}, {b})) == {(a + b) * 2}, "nested call"\n'
+    )
+
+# --- Lambda ---
+
+def gen_lambda():
+    a, b = _rand_int(), _rand_int()
+    return (
+        f"    f = lambda x, y: x + y\n"
+        f'    assert f({a}, {b}) == {a + b}, "lambda"\n'
+    )
+
+# --- List comprehension ---
+
+def gen_list_comp():
+    n = random.randint(2, 6)
+    return (
+        f"    lst = [x * 2 for x in range({n})]\n"
+        f'    assert lst == {[x * 2 for x in range(n)]}, "list comp"\n'
+    )
+
+def gen_list_comp_filter():
+    n = random.randint(3, 8)
+    return (
+        f"    lst = [x for x in range({n}) if x % 2 == 0]\n"
+        f'    assert lst == {[x for x in range(n) if x % 2 == 0]}, "list comp filter"\n'
+    )
+
+# --- Dict comprehension ---
+
+def gen_dict_comp():
+    n = random.randint(2, 5)
+    expected = {str(i): i * i for i in range(n)}
+    return (
+        f"    d = {{str(i): i * i for i in range({n})}}\n"
+        f'    assert d == {expected}, "dict comp"\n'
+    )
+
+# --- Try/except ---
+
+def gen_try_except():
+    return (
+        f"    caught: bool = False\n"
+        f"    try:\n"
+        f"        x: int = 1 // 0\n"
+        f"    except ZeroDivisionError:\n"
+        f"        caught = True\n"
+        f'    assert caught, "try except"\n'
+    )
+
+def gen_try_except_else():
+    return (
+        f"    result: int = 0\n"
+        f"    try:\n"
+        f"        result = 42\n"
+        f"    except Exception:\n"
+        f"        result = -1\n"
+        f"    else:\n"
+        f"        result = result + 1\n"
+        f'    assert result == 43, "try else"\n'
+    )
+
+def gen_try_finally():
+    return (
+        f"    cleanup: bool = False\n"
+        f"    try:\n"
+        f"        x: int = 10\n"
+        f"    finally:\n"
+        f"        cleanup = True\n"
+        f'    assert cleanup, "try finally"\n'
+    )
+
+# --- With statement (context manager) ---
+
+def gen_with_stmt():
+    # Use a simple class-based context manager
+    return (
+        f"    class CM:\n"
+        f"        def __enter__(self):\n"
+        f"            return 42\n"
+        f"        def __exit__(self, *args):\n"
+        f"            pass\n"
+        f"    with CM() as v:\n"
+        f"        r: int = v\n"
+        f'    assert r == 42, "with stmt"\n'
+    )
+
+# --- Global / nonlocal ---
+
+def gen_nonlocal():
+    return (
+        f"    x: int = 0\n"
+        f"    def inner():\n"
+        f"        nonlocal x\n"
+        f"        x = 99\n"
+        f"    inner()\n"
+        f'    assert x == 99, "nonlocal"\n'
+    )
+
+# --- Walrus operator ---
+
+def gen_walrus():
+    v = _rand_int()
+    return (
+        f"    lst = [{v}]\n"
+        f"    if (n := len(lst)) > 0:\n"
+        f'        assert n == 1, "walrus"\n'
+    )
+
+# --- F-strings ---
+
+def gen_fstring():
+    a = random.randint(0, 50)
+    return (
+        f"    a = {a}\n"
+        f'    assert f"val={{a}}" == "val={a}", "fstring"\n'
+    )
+
+# --- Star unpacking ---
+
+def gen_star_unpack():
+    elems = [_rand_int() for _ in range(random.randint(3, 5))]
+    return (
+        f"    first, *rest = {elems}\n"
+        f'    assert first == {elems[0]}, "star unpack first"\n'
+        f'    assert rest == {elems[1:]}, "star unpack rest"\n'
+    )
+
+# --- Nested loops ---
+
+def gen_nested_loop():
+    n, m = random.randint(1, 4), random.randint(1, 4)
+    return (
+        f"    total: int = 0\n"
+        f"    for i in range({n}):\n"
+        f"        for j in range({m}):\n"
+        f"            total = total + 1\n"
+        f'    assert total == {n * m}, "nested loop"\n'
+    )
+
+# --- Type conversions ---
+
+def gen_type_conv():
+    conv = random.choice([
+        ("int(3.7)", 3, "float to int"),
+        ("str(42)", "42", "int to str"),
+        ("int('17')", 17, "str to int"),
+        ("bool(0)", False, "int to bool false"),
+        ("bool(1)", True, "int to bool true"),
+        ("float(5)", 5.0, "int to float"),
+        ("list(range(3))", [0, 1, 2], "range to list"),
+    ])
+    expr, expected, label = conv
+    return f'    assert {expr} == {expected!r}, "{label}"\n'
+
+# --- String formatting ---
+
+def gen_str_format():
+    a = _rand_int()
+    return f'    assert "x={{}}".format({a}) == "x={a}", "str format"\n'
+
+# --- Multiple except clauses ---
+
+def gen_multi_except():
+    return (
+        f"    result: str = \"\"\n"
+        f"    try:\n"
+        f"        x = 1 // 0\n"
+        f"    except TypeError:\n"
+        f"        result = \"type\"\n"
+        f"    except ZeroDivisionError:\n"
+        f"        result = \"zero\"\n"
+        f'    assert result == "zero", "multi except"\n'
+    )
+
+# --- Raise / re-raise ---
+
+def gen_raise():
+    return (
+        f"    caught: bool = False\n"
+        f"    try:\n"
+        f"        raise ValueError(\"test\")\n"
+        f"    except ValueError as e:\n"
+        f"        caught = True\n"
+        f'        assert str(e) == "test", "raise msg"\n'
+        f'    assert caught, "raise caught"\n'
+    )
+
+# --- Pass statement ---
+
+def gen_pass():
+    return (
+        f"    if True:\n"
+        f"        pass\n"
+        f'    assert True, "pass"\n'
+    )
+
+# --- Delete ---
+
+def gen_del():
+    return (
+        f"    lst = [1, 2, 3]\n"
+        f"    del lst[1]\n"
+        f'    assert lst == [1, 3], "del"\n'
+    )
+
+# --- Set operations ---
+
+def gen_set_ops():
+    a = list(set([random.randint(0, 10) for _ in range(4)]))
+    b = list(set([random.randint(0, 10) for _ in range(4)]))
+    sa, sb = set(a), set(b)
+    op = random.choice(["union", "intersection"])
+    if op == "union":
+        r = sorted(sa | sb)
+        return f"    assert sorted(set({a}) | set({b})) == {r}, \"set {op}\"\n"
+    else:
+        r = sorted(sa & sb)
+        return f"    assert sorted(set({a}) & set({b})) == {r}, \"set {op}\"\n"
+
+# --- Isinstance ---
+
+def gen_isinstance():
+    return random.choice([
+        f'    assert isinstance(42, int), "isinstance int"\n',
+        f'    assert isinstance("hi", str), "isinstance str"\n',
+        f'    assert isinstance(True, bool), "isinstance bool"\n',
+        f'    assert isinstance([1], list), "isinstance list"\n',
+        f'    assert not isinstance(42, str), "isinstance neg"\n',
+    ])
+
+# --- Recursive function ---
+
+def gen_recursion():
+    n = random.randint(1, 8)
+    def fact(n):
+        return 1 if n <= 1 else n * fact(n - 1)
+    return (
+        f"    def factorial(n: int) -> int:\n"
+        f"        if n <= 1:\n"
+        f"            return 1\n"
+        f"        return n * factorial(n - 1)\n"
+        f'    assert factorial({n}) == {fact(n)}, "recursion"\n'
+    )
+
+# --- Default arguments ---
+
+def gen_default_args():
+    d = _rand_int()
+    return (
+        f"    def f(x: int, y: int = {d}) -> int:\n"
+        f"        return x + y\n"
+        f'    assert f(10) == {10 + d}, "default arg"\n'
+        f'    assert f(10, 20) == 30, "override default"\n'
+    )
+
+# --- *args / **kwargs ---
+
+def gen_varargs():
+    return (
+        f"    def f(*args):\n"
+        f"        return sum(args)\n"
+        f'    assert f(1, 2, 3) == 6, "varargs"\n'
+    )
+
+def gen_kwargs():
+    return (
+        f"    def f(**kwargs):\n"
+        f"        return kwargs.get(\"x\", 0)\n"
+        f'    assert f(x=42) == 42, "kwargs"\n'
+    )
+
+# --- Yield / generator ---
+
+def gen_generator():
+    n = random.randint(2, 5)
+    return (
+        f"    def gen():\n"
+        f"        for i in range({n}):\n"
+        f"            yield i\n"
+        f'    assert list(gen()) == {list(range(n))}, "generator"\n'
+    )
+
+# --- Decorator ---
+
+def gen_decorator():
+    return (
+        f"    def my_dec(fn):\n"
+        f"        def wrapper(*a):\n"
+        f"            return fn(*a) + 1\n"
+        f"        return wrapper\n"
+        f"    @my_dec\n"
+        f"    def f(x: int) -> int:\n"
+        f"        return x\n"
+        f'    assert f(10) == 11, "decorator"\n'
+    )
+
+# --- Async (syntax only, not awaited) ---
+
+def gen_async_def():
+    return (
+        f"    import asyncio\n"
+        f"    async def coro():\n"
+        f"        return 42\n"
+        f'    assert asyncio.run(coro()) == 42, "async"\n'
+    )
+
+# --- Walrus in while ---
+
+def gen_walrus_while():
+    return (
+        f"    data = [1, 2, 3, 0, 4]\n"
+        f"    total: int = 0\n"
+        f"    idx: int = 0\n"
+        f"    while (v := data[idx]) != 0:\n"
+        f"        total = total + v\n"
+        f"        idx = idx + 1\n"
+        f'    assert total == 6, "walrus while"\n'
+    )
+
+# --- Match statement (Python 3.10+) ---
+
+def gen_match():
+    v = random.choice([1, 2, 3, "other"])
+    if v == 1:
+        r = "one"
+    elif v == 2:
+        r = "two"
+    else:
+        r = "other"
+    return (
+        f"    val = {v!r}\n"
+        f"    match val:\n"
+        f"        case 1:\n"
+        f"            r = \"one\"\n"
+        f"        case 2:\n"
+        f"            r = \"two\"\n"
+        f"        case _:\n"
+        f"            r = \"other\"\n"
+        f'    assert r == {r!r}, "match"\n'
+    )
+
+
+# ---------------------------------------------------------------------------
+# Registry
+# ---------------------------------------------------------------------------
+# All unrestricted generators, imported by gen_random_python.py when
+# --unrestricted is passed. The order doesn't matter — generators are
+# chosen uniformly at random.
+
+UNRESTRICTED_GENERATORS = [
+    gen_bitwise, gen_shift, gen_bitnot, gen_power,
+    gen_augmented_assign, gen_ternary, gen_multi_assign,
+    gen_list_create, gen_list_index, gen_list_concat, gen_list_slice,
+    gen_list_in, gen_list_append,
+    gen_dict_create, gen_dict_access, gen_dict_in,
+    gen_str_len, gen_str_index, gen_str_multiply, gen_str_methods,
+    gen_for_sum, gen_for_range, gen_while_countdown, gen_break,
+    gen_nested_if, gen_elif, gen_tuple_unpack, gen_chained_cmp,
+    gen_none_check, gen_optional,
+    gen_class_basic, gen_class_method, gen_nested_call,
+    gen_lambda, gen_list_comp, gen_list_comp_filter, gen_dict_comp,
+    gen_try_except, gen_try_except_else, gen_try_finally,
+    gen_with_stmt, gen_nonlocal, gen_walrus, gen_fstring,
+    gen_star_unpack, gen_nested_loop, gen_type_conv, gen_str_format,
+    gen_multi_except, gen_raise, gen_pass, gen_del, gen_set_ops,
+    gen_isinstance, gen_recursion, gen_default_args,
+    gen_varargs, gen_kwargs, gen_generator, gen_decorator,
+    gen_async_def, gen_walrus_while, gen_match,
+]
diff --git a/Tools/Python/scripts/hypothesmith.sh b/Tools/Python/scripts/hypothesmith.sh
new file mode 100755
index 0000000000..ca41602c6a
--- /dev/null
+++ b/Tools/Python/scripts/hypothesmith.sh
@@ -0,0 +1,362 @@
+#!/bin/bash
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+#
+# =============================================================================
+# hypothesmith.sh — Fuzz-test Strata's Python front-end
+# =============================================================================
+#
+# This script generates random Python programs and runs them through Strata's
+# Python front-end pipeline to find crashes, round-trip failures, and semantic
+# modelling bugs. It is analogous to CBMC's scripts/csmith.sh, which uses
+# CSmith to generate random C programs for testing CBMC.
+#
+# ## Background
+#
+# The approach is inspired by:
+# - CSmith (https://embed.cs.utah.edu/csmith/) for random C program generation
+# - hypothesmith (https://github.com/Zac-HD/hypothesmith) for random Python
+#   program generation using the Hypothesis property-based testing framework
+# - The discussion at https://bugs.python.org/issue42109 about using Hypothesis
+#   and hypothesmith for testing CPython itself
+#
+# ## Modes
+#
+# **Syntax mode** — Uses hypothesmith's `from_grammar()` strategy to generate
+# syntactically valid Python programs from the Python grammar. Each program is:
+#   1. Parsed into Strata's Ion format via `python -m strata.gen py_to_strata`
+#   2. Round-tripped through `strata toIon`
+#   3. Diffed against the original Ion to check for round-trip fidelity
+#
+# This tests that the parser pipeline doesn't crash or lose information on
+# arbitrary valid Python. Programs that fail to parse are SKIPped (hypothesmith
+# may generate constructs the Strata parser doesn't support yet).
+#
+# **Semantic mode** — Uses a custom generator (gen_random_python.py) to produce
+# typed Python programs with assertions whose expected values are computed by
+# CPython at generation time. This is the CSmith checksum analogy:
+#   1. CPython runs the program to confirm all assertions pass (reference)
+#   2. The program is parsed into Ion format
+#   3. `pyAnalyzeLaurel` verifies the program via the Laurel pipeline
+#   4. If Strata reports a failing assertion on a program that CPython runs
+#      correctly, that indicates a semantic modelling bug in the
+#      Python → Laurel → Core translation pipeline
+#
+# ## Result classification
+#
+# Each test program gets one of these outcomes:
+#   OK                — Pipeline completed successfully, all checks passed
+#   SKIP (parse)      — Strata's parser couldn't handle the syntax (expected)
+#   SKIP (unsupported)— pyAnalyzeLaurel hit an unsupported construct (expected)
+#   TIMEOUT           — Analysis exceeded the time limit (not counted as failure)
+#   FAIL (toIon)      — Ion round-trip produced different output (bug)
+#   FAIL (diff)       — Ion diff detected a mismatch (bug)
+#   FAIL (internal)   — Strata panicked or leaked memory (bug)
+#   FAIL (verification)— Strata says assertion fails but CPython says it passes
+#                        (semantic modelling bug)
+#   BUG (generator)   — The generated program itself fails under CPython
+#                        (bug in our generator, not in Strata)
+#
+# ## Reproducibility
+#
+# Every run uses a seed that controls both the Hypothesis engine (syntax mode)
+# and Python's random module (semantic mode). Given the same seed, the same
+# programs are generated. The seed is printed at the start and end of every
+# run. To reproduce a failure:
+#
+#   cd Tools/Python
+#   ./scripts/hypothesmith.sh 10 <SEED> both --unrestricted
+#
+# ## Usage
+#
+#   ./hypothesmith.sh [N [SEED [MODE [--unrestricted]]]]
+#
+#   N              Number of programs to generate per mode (default: 10)
+#   SEED           Random seed for reproducibility (default: current timestamp)
+#   MODE           "syntax", "semantic", or "both" (default: both)
+#   --unrestricted Include generators for Python constructs beyond what Strata
+#                  supports today (classes, generators, comprehensions,
+#                  try/except, match, async, decorators, etc.)
+#
+# ## Prerequisites
+#
+#   - Python venv at Tools/Python/.venv with hypothesmith and strata installed:
+#       python3 -m venv Tools/Python/.venv
+#       Tools/Python/.venv/bin/pip install -e Tools/Python hypothesmith
+#   - Strata built: lake build strata
+#   - Python dialect file at Tools/Python/dialects/Python.dialect.st.ion
+#
+# ## Exit codes
+#
+#   0  All tests passed (or only SKIPs/TIMEOUTs)
+#   1  At least one FAIL detected (source code is printed for reproduction)
+#
+# =============================================================================
+
+set -euo pipefail
+
+# ---------------------------------------------------------------------------
+# Configuration
+# ---------------------------------------------------------------------------
+
+SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"
+REPO_ROOT="$(cd "$SCRIPT_DIR/../../.." && pwd)"
+TOOLS_PY="$REPO_ROOT/Tools/Python"
+PYTHON="${PYTHON:-$TOOLS_PY/.venv/bin/python3}"
+STRATA="$REPO_ROOT/.lake/build/bin/strata"
+DIALECT="$TOOLS_PY/dialects/Python.dialect.st.ion"
+
+# Command-line arguments with defaults.
+N="${1:-10}"
+SEED="${2:-$(date +%s)}"
+MODE="${3:-both}"
+UNRESTRICTED=""
+if [ "${4:-}" = "--unrestricted" ]; then
+  UNRESTRICTED="--unrestricted"
+fi
+
+# Timeouts (seconds) for individual pipeline steps.
+# Parse timeout covers py_to_strata and toIon; analyse timeout covers
+# pyAnalyzeLaurel which invokes the SMT solver.
+PARSE_TIMEOUT=30
+ANALYZE_TIMEOUT=90
+
+# ---------------------------------------------------------------------------
+# Prerequisite checks
+# ---------------------------------------------------------------------------
+
+if ! command -v "$PYTHON" &>/dev/null; then
+  echo "ERROR: Python venv not found at $TOOLS_PY/.venv"
+  echo "Set up with:"
+  echo "  python3 -m venv $TOOLS_PY/.venv"
+  echo "  $TOOLS_PY/.venv/bin/pip install -e $TOOLS_PY hypothesmith"
+  exit 1
+fi
+
+if [ ! -f "$STRATA" ]; then
+  echo "ERROR: strata not built. Run: lake build strata"
+  exit 1
+fi
+
+if [ ! -f "$DIALECT" ]; then
+  echo "ERROR: Python dialect not found at $DIALECT"
+  exit 1
+fi
+
+# ---------------------------------------------------------------------------
+# Working directory (cleaned up on exit)
+# ---------------------------------------------------------------------------
+
+workdir=$(mktemp -d /tmp/strata-fuzz.XXX)
+trap 'rm -rf "$workdir"' EXIT
+
+failures=0
+
+# ---------------------------------------------------------------------------
+# Syntax mode
+# ---------------------------------------------------------------------------
+# Generate random syntactically-valid Python via hypothesmith, then test
+# the parse → Ion → round-trip pipeline.
+
+run_syntax_tests() {
+  local gen_dir="$workdir/syntax"
+  echo "=== Syntax mode: generating $N programs (seed=$SEED) ==="
+  timeout 120 "$PYTHON" "$SCRIPT_DIR/gen_random_python.py" \
+    --mode syntax --output-dir "$gen_dir" \
+    --max-examples "$N" --max-nodes 50 --seed "$SEED" 2>&1
+
+  local count=0
+  for pyfile in "$gen_dir"/fuzz_syntax_*.py; do
+    [ -f "$pyfile" ] || continue
+    count=$((count + 1))
+    local base
+    base=$(basename "$pyfile" .py)
+    local ion="$gen_dir/${base}.python.st.ion"
+    local ion2="$gen_dir/${base}.python.st.ion2"
+
+    # Step 1: Parse Python → Ion via the external Python tool.
+    # Parse failures are acceptable — hypothesmith may generate constructs
+    # that the Strata parser doesn't support yet.
+    if ! timeout "$PARSE_TIMEOUT" "$PYTHON" -m strata.gen py_to_strata \
+        --dialect "$DIALECT" "$pyfile" "$ion" 2>/dev/null; then
+      echo "  SKIP (parse): $base"
+      continue
+    fi
+
+    # Step 2: Round-trip the Ion through strata toIon.
+    # This re-serialises the Ion file; a failure here means the Lean-side
+    # reader or writer has a bug.
+    if ! timeout "$PARSE_TIMEOUT" "$STRATA" toIon \
+        --include "$TOOLS_PY/dialects" "$ion" "$ion2" 2>/dev/null; then
+      echo "  FAIL (toIon): $base"
+      echo "--- Source code ---"
+      cat "$pyfile"
+      echo "---"
+      failures=$((failures + 1))
+      continue
+    fi
+
+    # Step 3: Diff the original and round-tripped Ion files.
+    # Any difference means information was lost or corrupted.
+    if ! "$STRATA" diff --include "$TOOLS_PY/dialects" "$ion" "$ion2" 2>/dev/null; then
+      echo "  FAIL (diff): $base"
+      echo "--- Source code ---"
+      cat "$pyfile"
+      echo "---"
+      failures=$((failures + 1))
+      continue
+    fi
+
+    echo "  OK: $base"
+  done
+  echo "Syntax tests: $count processed, $failures failures"
+}
+
+# ---------------------------------------------------------------------------
+# Semantic mode
+# ---------------------------------------------------------------------------
+# Generate typed Python programs with known-true assertions, validate them
+# with CPython, then verify with pyAnalyzeLaurel. A verification failure
+# on a CPython-passing program indicates a semantic modelling bug.
+
+run_semantic_tests() {
+  local gen_dir="$workdir/semantic"
+  echo "=== Semantic mode: generating $N programs (seed=$SEED) ==="
+  "$PYTHON" "$SCRIPT_DIR/gen_random_python.py" \
+    --mode semantic --output-dir "$gen_dir" \
+    --max-examples "$N" --seed "$SEED" $UNRESTRICTED 2>&1
+
+  local count=0
+  local sem_failures=0
+  for pyfile in "$gen_dir"/fuzz_semantic_*.py; do
+    [ -f "$pyfile" ] || continue
+    count=$((count + 1))
+    local base
+    base=$(basename "$pyfile" .py)
+    local ion="$gen_dir/${base}.python.st.ion"
+
+    # Step 1: Sanity check — run with CPython to confirm assertions pass.
+    # This is the "reference execution" (analogous to CSmith's GCC run
+    # that computes the reference checksum). If CPython fails, the bug
+    # is in our generator, not in Strata.
+    if ! timeout 10 "$PYTHON" "$pyfile" 2>/dev/null; then
+      echo "  BUG (generator): $base fails under CPython!"
+      cat "$pyfile"
+      sem_failures=$((sem_failures + 1))
+      continue
+    fi
+
+    # Step 2: Parse Python → Ion.
+    # Parse failures are acceptable — the generator may produce constructs
+    # that the Strata parser doesn't support yet (same as syntax mode).
+    if ! timeout "$PARSE_TIMEOUT" "$PYTHON" -m strata.gen py_to_strata \
+        --dialect "$DIALECT" "$pyfile" "$ion" 2>/dev/null; then
+      echo "  SKIP (parse): $base"
+      continue
+    fi
+
+    # Step 3: Run pyAnalyzeLaurel — the full Python → Laurel → Core → SMT
+    # verification pipeline.
+    local output
+    local ec=0
+    output=$(timeout "$ANALYZE_TIMEOUT" "$STRATA" pyAnalyzeLaurel "$ion" 2>&1) || ec=$?
+
+    # Handle timeouts (exit 124 from timeout, 137 from SIGKILL).
+    if [ $ec -eq 124 ] || [ $ec -eq 137 ]; then
+      echo "  TIMEOUT: $base"
+      continue
+    fi
+
+    # Non-zero exit from pyAnalyzeLaurel. Distinguish between:
+    # - Internal errors (panics, memory leaks) → real bugs, count as FAIL
+    # - Translation failures → unsupported constructs, count as SKIP
+    if [ $ec -ne 0 ]; then
+      if echo "$output" | grep -qi "panic\|LEAK"; then
+        echo "  FAIL (internal error): $base"
+        echo "--- Source code ---"
+        cat "$pyfile"
+        echo "--- Output ---"
+        echo "$output" | head -20
+        echo "---"
+        sem_failures=$((sem_failures + 1))
+        continue
+      fi
+      if echo "$output" | grep -q "RESULT: Failures found"; then
+        echo "  FAIL (verification, exit $ec): $base"
+        echo "--- Source code ---"
+        cat "$pyfile"
+        echo "--- pyAnalyzeLaurel output ---"
+        echo "$output"
+        echo "---"
+        sem_failures=$((sem_failures + 1))
+        continue
+      fi
+      if echo "$output" | grep -q "RESULT: Internal error"; then
+        echo "  FAIL (internal error): $base"
+        echo "--- Source code ---"
+        cat "$pyfile"
+        echo "--- Output ---"
+        echo "$output" | head -20
+        echo "---"
+        sem_failures=$((sem_failures + 1))
+        continue
+      fi
+      # Translation failures and other non-zero exits are unsupported
+      # constructs — expected when using --unrestricted.
+      echo "  SKIP (unsupported): $base"
+      continue
+    fi
+
+    # Step 4: Check verification results. If pyAnalyzeLaurel reports any
+    # failed assertions, but CPython ran the program successfully (Step 1),
+    # then Strata's semantic model disagrees with CPython. This is the
+    # most interesting kind of bug to find — analogous to CBMC finding a
+    # counterexample to the CSmith checksum assertion.
+    #
+    # The grep matches "N failed" in the DETAIL line, which means the solver
+    # *proved* the assertion does not hold (found a counterexample). This is
+    # distinct from "inconclusive" (solver couldn't determine either way),
+    # which is not treated as a failure here.
+    # TODO: Once pyInterpret (#869) is available, use it for concrete
+    # pass/fail comparison with CPython (no unknown middle ground).
+    if echo "$output" | grep -qE '[1-9][0-9]* failed'; then
+      echo "  FAIL (verification): $base"
+      echo "  Strata reports a failing assertion on a program that CPython"
+      echo "  runs correctly. This indicates a semantic modelling bug in"
+      echo "  the Python → Laurel → Core translation pipeline."
+      echo "--- Source code ---"
+      cat "$pyfile"
+      echo "--- pyAnalyzeLaurel output ---"
+      echo "$output"
+      echo "---"
+      sem_failures=$((sem_failures + 1))
+      continue
+    fi
+
+    echo "  OK: $base"
+  done
+  failures=$((failures + sem_failures))
+  echo "Semantic tests: $count processed, $sem_failures failures"
+}
+
+# ---------------------------------------------------------------------------
+# Main
+# ---------------------------------------------------------------------------
+
+echo "Strata Python front-end fuzz test"
+echo "Seed: $SEED  N: $N  Mode: $MODE  Unrestricted: ${UNRESTRICTED:-no}"
+echo ""
+
+case "$MODE" in
+  syntax)   run_syntax_tests ;;
+  semantic) run_semantic_tests ;;
+  both)     run_syntax_tests; echo ""; run_semantic_tests ;;
+  *)        echo "Unknown mode: $MODE"; exit 1 ;;
+esac
+
+echo ""
+if [ $failures -ne 0 ]; then
+  echo "FAILED: $failures failure(s). Seed was: $SEED"
+  exit 1
+fi
+echo "ALL PASSED. Seed was: $SEED"