diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 2b3c11a..ca30944 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -78,3 +78,46 @@ jobs:
                 body,
               });
             }
+
+  # In-browser TLC regression suite: runs every lesson (that declares an
+  # `expect` outcome) through the real CheerpJ worker and asserts the result.
+  # Needs a real browser + network (CheerpJ CDN). Runs on PRs (so changes can
+  # be validated before merge) and on merges to main.
+  e2e:
+    runs-on: ubuntu-latest
+    timeout-minutes: 25
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v4
+
+      - name: Checkout Examples repo
+        uses: actions/checkout@v4
+        with:
+          repository: tlaplus/Examples
+          path: Examples
+
+      - name: Setup Node.js
+        uses: actions/setup-node@v4
+        with:
+          node-version: '20'
+          cache: 'npm'
+
+      - name: Download latest TLC JAR
+        run: curl -fSL -o public/tlaplus-web-cheerpj.jar https://github.com/FedericoPonzi/tlaplus-web/releases/latest/download/tlaplus-web-cheerpj.jar
+
+      - name: Install dependencies
+        run: npm ci
+
+      - name: Install Playwright browser
+        run: npx playwright install --with-deps chromium
+
+      - name: Run lesson regression suite
+        run: npm run test:e2e
+
+      - name: Upload Playwright report on failure
+        if: failure()
+        uses: actions/upload-artifact@v4
+        with:
+          name: playwright-report
+          path: playwright-report/
+          retention-days: 14
diff --git a/.gitignore b/.gitignore
index 9e89908..b944e03 100644
--- a/.gitignore
+++ b/.gitignore
@@ -4,3 +4,5 @@ out/
 Examples/
 *.tsbuildinfo
 next-env.d.ts
+test-results/
+playwright-report/
diff --git a/e2e/lessons.spec.ts b/e2e/lessons.spec.ts
new file mode 100644
index 0000000..3bddd56
--- /dev/null
+++ b/e2e/lessons.spec.ts
@@ -0,0 +1,47 @@
+import { test, expect } from "@playwright/test";
+import { introLessons } from "@/content/intro";
+import { blockingQueueLessons } from "@/content/blocking-queue";
+import { runTlcInBrowser, classifyTlcOutput } from "./tlc-runner";
+
+/**
+ * Pluggable, per-lesson in-browser TLC regression suite.
+ *
+ * Every lesson that declares an `expect` field in its markdown frontmatter
+ * (see src/lib/lessons.ts) is model-checked in a real browser via the CheerpJ
+ * worker, and its outcome is asserted:
+ *
+ *   expect: success    -> TLC completes with no error
+ *   expect: violation  -> TLC reports a counterexample (invariant / deadlock)
+ *
+ * To add coverage for a lesson, add `expect: success` or `expect: violation`
+ * to its frontmatter — no test code changes required. Lessons without an
+ * `expect` (e.g. animation-only lessons, lessons with no spec/cfg, or very
+ * large models such as `intro/records` whose state space is impractical to
+ * explore in-browser) are skipped automatically.
+ *
+ * This guards against the class of CheerpJ regression where in-browser TLC
+ * silently stops after computing initial states and misses counterexamples.
+ */
+
+const lessons = [...introLessons, ...blockingQueueLessons].filter((l) => l.expect);
+
+test.describe("Lesson TLC regression", () => {
+  test("at least one lesson declares an expected outcome", () => {
+    expect(lessons.length).toBeGreaterThan(0);
+  });
+
+  for (const lesson of lessons) {
+    test(`${lesson.section}/${lesson.slug} -> ${lesson.expect}`, async ({ page }) => {
+      await page.goto("/");
+      const output = await runTlcInBrowser(page, lesson.spec, lesson.cfg);
+      const { violated, completed } = classifyTlcOutput(output);
+
+      if (lesson.expect === "violation") {
+        expect(violated, `expected a counterexample but none was reported:\n${output}`).toBe(true);
+      } else {
+        expect(violated, `unexpected counterexample:\n${output}`).toBe(false);
+        expect(completed, `expected model checking to complete:\n${output}`).toBe(true);
+      }
+    });
+  }
+});
diff --git a/e2e/tlc-runner.ts b/e2e/tlc-runner.ts
new file mode 100644
index 0000000..0428a0a
--- /dev/null
+++ b/e2e/tlc-runner.ts
@@ -0,0 +1,59 @@
+import type { Page } from "@playwright/test";
+
+/**
+ * Drives the real in-browser TLC worker (`public/tlc-worker.html`) — the same
+ * CheerpJ runtime + jar the app uses — from within the app origin.
+ *
+ * `page` must already be navigated to the app (e.g. `await page.goto("/")`) so
+ * that the worker iframe is same-origin. Returns the raw TLC output string.
+ *
+ * A fresh Playwright page should be used per call: CheerpJ does not reliably
+ * support many runtime initialisations within a single page.
+ */
+export async function runTlcInBrowser(page: Page, spec: string, cfg: string): Promise<string> {
+  return page.evaluate(
+    ({ spec, cfg }) =>
+      new Promise<string>((resolve) => {
+        const iframe = document.createElement("iframe");
+        iframe.style.display = "none";
+        let done = false;
+        function onMsg(ev: MessageEvent) {
+          if (ev.source !== iframe.contentWindow) return; // ignore the app's own worker
+          const d = ev.data;
+          if (!d || !d.type) return;
+          if (d.type === "ready") {
+            iframe.contentWindow!.postMessage(
+              { type: "run", spec, cfg, workers: 1, checkDeadlock: true, extraModules: [] },
+              "*",
+            );
+          } else if (d.type === "result") {
+            if (done) return;
+            done = true;
+            window.removeEventListener("message", onMsg);
+            iframe.remove();
+            resolve(d.output as string);
+          } else if (d.type === "error") {
+            if (done) return;
+            done = true;
+            window.removeEventListener("message", onMsg);
+            iframe.remove();
+            resolve("INIT ERROR: " + d.message);
+          }
+        }
+        window.addEventListener("message", onMsg);
+        iframe.src = "/tlc-worker.html";
+        document.body.appendChild(iframe);
+      }),
+    { spec, cfg },
+  );
+}
+
+/** Classify a raw TLC output string into the outcome dimensions the suite asserts on. */
+export function classifyTlcOutput(output: string): { violated: boolean; completed: boolean } {
+  return {
+    // A counterexample: an invariant/property violation or a deadlock.
+    violated: /is violated|Deadlock reached/.test(output),
+    // A clean, exhaustive exploration with no error.
+    completed: /Model checking completed/.test(output),
+  };
+}
diff --git a/jest.config.js b/jest.config.js
index 6bba712..51ab16d 100644
--- a/jest.config.js
+++ b/jest.config.js
@@ -18,4 +18,5 @@ module.exports = {
   moduleNameMapper: {
     "^@/(.*)$": "<rootDir>/src/$1",
   },
+  testPathIgnorePatterns: ["/node_modules/", "/e2e/"],
 };
diff --git a/package.json b/package.json
index f877fc7..0fb119c 100644
--- a/package.json
+++ b/package.json
@@ -7,7 +7,8 @@
     "build": "next build",
     "start": "next start",
     "lint": "next lint",
-    "test": "jest"
+    "test": "jest",
+    "test:e2e": "playwright test"
   },
   "dependencies": {
     "@codemirror/lang-javascript": "^6.2.4",
diff --git a/playwright.config.ts b/playwright.config.ts
new file mode 100644
index 0000000..0126afa
--- /dev/null
+++ b/playwright.config.ts
@@ -0,0 +1,31 @@
+import { defineConfig, devices } from "@playwright/test";
+
+/**
+ * E2E config for the in-browser TLC checker.
+ *
+ * These tests run TLC inside a real browser via CheerpJ, so they need a browser
+ * and network access (CheerpJ downloads its runtime from a CDN at load time).
+ * They are intentionally kept separate from the jsdom `npm test` unit suite.
+ */
+export default defineConfig({
+  testDir: "./e2e",
+  timeout: 5 * 60 * 1000,
+  expect: { timeout: 4 * 60 * 1000 },
+  fullyParallel: false,
+  workers: 1,
+  reporter: [["list"], ["html", { open: "never" }]],
+  use: {
+    baseURL: "http://localhost:3000",
+    headless: true,
+    trace: "retain-on-failure",
+  },
+  projects: [
+    { name: "chromium", use: { ...devices["Desktop Chrome"] } },
+  ],
+  webServer: {
+    command: "npm run dev",
+    url: "http://localhost:3000",
+    reuseExistingServer: !process.env.CI,
+    timeout: 120 * 1000,
+  },
+});
diff --git a/src/content/blocking-queue/01-introduction.md b/src/content/blocking-queue/01-introduction.md
index 1303f88..d308d84 100644
--- a/src/content/blocking-queue/01-introduction.md
+++ b/src/content/blocking-queue/01-introduction.md
@@ -1,5 +1,6 @@
 ---
 slug: introduction
+expect: success
 title: Introduction
 section: blocking-queue
 commitSha: "11410864"
diff --git a/src/content/blocking-queue/02-state-graph.md b/src/content/blocking-queue/02-state-graph.md
index 9be9653..d6a8c1f 100644
--- a/src/content/blocking-queue/02-state-graph.md
+++ b/src/content/blocking-queue/02-state-graph.md
@@ -1,5 +1,6 @@
 ---
 slug: state-graph
+expect: success
 title: "State Graph (Minimum Config)"
 section: blocking-queue
 commitSha: "d21cd0fa"
diff --git a/src/content/blocking-queue/03-larger-config.md b/src/content/blocking-queue/03-larger-config.md
index 833baa8..7c2f2e2 100644
--- a/src/content/blocking-queue/03-larger-config.md
+++ b/src/content/blocking-queue/03-larger-config.md
@@ -1,5 +1,6 @@
 ---
 slug: larger-config
+expect: violation
 title: "Larger Configuration"
 section: blocking-queue
 commitSha: "7d05fdfa"
diff --git a/src/content/blocking-queue/04-debug-config.md b/src/content/blocking-queue/04-debug-config.md
index ad0246b..ebaa0da 100644
--- a/src/content/blocking-queue/04-debug-config.md
+++ b/src/content/blocking-queue/04-debug-config.md
@@ -1,5 +1,6 @@
 ---
 slug: debug-config
+expect: violation
 title: "Debug State Graph"
 section: blocking-queue
 commitSha: "534f3928"
diff --git a/src/content/blocking-queue/05-safety.md b/src/content/blocking-queue/05-safety.md
index c808267..ba9cb09 100644
--- a/src/content/blocking-queue/05-safety.md
+++ b/src/content/blocking-queue/05-safety.md
@@ -1,5 +1,6 @@
 ---
 slug: safety
+expect: violation
 title: "Safety - Detecting Deadlocks"
 section: blocking-queue
 commitSha: "ce99d16a"
diff --git a/src/content/blocking-queue/06-variables.md b/src/content/blocking-queue/06-variables.md
index ae76bfa..82bbb91 100644
--- a/src/content/blocking-queue/06-variables.md
+++ b/src/content/blocking-queue/06-variables.md
@@ -1,5 +1,6 @@
 ---
 slug: variables
+expect: violation
 title: "Constants to Variables"
 section: blocking-queue
 commitSha: "d48bd86a"
diff --git a/src/content/blocking-queue/07-symmetry.md b/src/content/blocking-queue/07-symmetry.md
index b7146e3..72ae3ad 100644
--- a/src/content/blocking-queue/07-symmetry.md
+++ b/src/content/blocking-queue/07-symmetry.md
@@ -1,5 +1,6 @@
 ---
 slug: symmetry
+expect: violation
 title: "Symmetry Sets"
 section: blocking-queue
 commitSha: "553287fd"
diff --git a/src/content/blocking-queue/08-inequation.md b/src/content/blocking-queue/08-inequation.md
index a35d8c3..3201bf4 100644
--- a/src/content/blocking-queue/08-inequation.md
+++ b/src/content/blocking-queue/08-inequation.md
@@ -1,5 +1,6 @@
 ---
 slug: inequation
+expect: violation
 title: "Deadlock-Free Inequation"
 section: blocking-queue
 commitSha: "8e536cba"
diff --git a/src/content/blocking-queue/09-view.md b/src/content/blocking-queue/09-view.md
index 36290cb..84639c2 100644
--- a/src/content/blocking-queue/09-view.md
+++ b/src/content/blocking-queue/09-view.md
@@ -1,5 +1,6 @@
 ---
 slug: view
+expect: violation
 title: "View Abstraction"
 section: blocking-queue
 commitSha: "02119f46"
diff --git a/src/content/intro/basic-operators.md b/src/content/intro/basic-operators.md
index d20552d..3579b1e 100644
--- a/src/content/intro/basic-operators.md
+++ b/src/content/intro/basic-operators.md
@@ -1,5 +1,6 @@
 ---
 slug: basic-operators
+expect: success
 title: Basic Operators
 section: intro
 ---
diff --git a/src/content/intro/functions.md b/src/content/intro/functions.md
index 95d8b8c..2a7d052 100644
--- a/src/content/intro/functions.md
+++ b/src/content/intro/functions.md
@@ -1,5 +1,6 @@
 ---
 slug: functions
+expect: violation
 title: Functions
 section: intro
 ---
diff --git a/src/content/intro/module-structure.md b/src/content/intro/module-structure.md
index c50cc46..85fcee9 100644
--- a/src/content/intro/module-structure.md
+++ b/src/content/intro/module-structure.md
@@ -1,5 +1,6 @@
 ---
 slug: module-structure
+expect: violation
 title: Module Structure
 section: intro
 ---
diff --git a/src/content/intro/platform.md b/src/content/intro/platform.md
index 0735577..056ab5c 100644
--- a/src/content/intro/platform.md
+++ b/src/content/intro/platform.md
@@ -1,5 +1,6 @@
 ---
 slug: platform
+expect: violation
 title: Welcome
 section: intro
 ---
diff --git a/src/content/intro/sequences.md b/src/content/intro/sequences.md
index 1ac0e77..ea19a30 100644
--- a/src/content/intro/sequences.md
+++ b/src/content/intro/sequences.md
@@ -1,5 +1,6 @@
 ---
 slug: sequences
+expect: success
 title: Sequences
 section: intro
 ---
diff --git a/src/content/intro/sets.md b/src/content/intro/sets.md
index 38a4b14..0cc59fb 100644
--- a/src/content/intro/sets.md
+++ b/src/content/intro/sets.md
@@ -1,5 +1,6 @@
 ---
 slug: sets
+expect: success
 title: Sets
 section: intro
 ---
diff --git a/src/content/intro/tlc-config.md b/src/content/intro/tlc-config.md
index b5b174c..a22047b 100644
--- a/src/content/intro/tlc-config.md
+++ b/src/content/intro/tlc-config.md
@@ -1,5 +1,6 @@
 ---
 slug: tlc-config
+expect: success
 title: TLC Configuration
 section: intro
 ---
diff --git a/src/content/intro/variables-constants.md b/src/content/intro/variables-constants.md
index d062f18..0bd552a 100644
--- a/src/content/intro/variables-constants.md
+++ b/src/content/intro/variables-constants.md
@@ -1,5 +1,6 @@
 ---
 slug: variables-constants
+expect: violation
 title: "Variables & Constants"
 section: intro
 ---
diff --git a/src/lib/lessons.ts b/src/lib/lessons.ts
index a56b45b..3ef0ca4 100644
--- a/src/lib/lessons.ts
+++ b/src/lib/lessons.ts
@@ -15,8 +15,25 @@ export interface Lesson {
   extraTabs?: ExtraTab[];
   commitSha?: string;
   commitUrl?: string;
+  /**
+   * Expected TLC outcome when running this lesson's spec+cfg in the playground.
+   * Consumed by the browser regression suite (e2e/lessons.spec.ts).
+   * Omit for lessons that are not meant to be model-checked standalone
+   * (e.g. animation-only lessons or lessons without a spec/cfg).
+   */
+  expect?: TlcExpectation;
 }
 
+/**
+ * `success`   - TLC explores the whole state space and finds no error
+ *               ("Model checking completed").
+ * `violation` - TLC finds a counterexample: an invariant violation or a
+ *               deadlock ("is violated" / "Deadlock reached"). In this tutorial
+ *               a violation is often the intended teaching outcome
+ *               (e.g. DieHard, or the BlockingQueue deadlock bug stages).
+ */
+export type TlcExpectation = "success" | "violation";
+
 export interface LessonNavInfo {
   slug: string;
   title: string;
diff --git a/src/lib/parse-lesson.ts b/src/lib/parse-lesson.ts
index fe94d6e..1e1fb31 100644
--- a/src/lib/parse-lesson.ts
+++ b/src/lib/parse-lesson.ts
@@ -69,6 +69,7 @@ export function parseLesson(markdown: string): Lesson {
 
   if (data.commitSha) lesson.commitSha = data.commitSha;
   if (data.commitUrl) lesson.commitUrl = data.commitUrl;
+  if (data.expect) lesson.expect = data.expect;
   if (extraTabs.length > 0) lesson.extraTabs = extraTabs;
 
   return lesson;