diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 8cec5f7..395fafb 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -79,6 +79,17 @@ jobs:
           sudo apt-get update
           sudo apt-get install --yes --no-install-recommends texlive-latex-base
 
+      - name: Set up the documented demo
+        run: make demo-setup
+
+      - name: Run the narrated checks and a new-input PDF demo
+        env:
+          UV_OFFLINE: "1"
+          UV_PYTHON_DOWNLOADS: never
+        run: |
+          make demo-check
+          make demo INPUT=tests/instances/demo_sat.cm13 TIMEOUT=300
+
       - name: Compile opt-in run dossier without shell escape
         run: make run-dossier-smoke
 
diff --git a/Makefile b/Makefile
index 150e789..dc6c95a 100644
--- a/Makefile
+++ b/Makefile
@@ -6,6 +6,11 @@ VALGRIND ?= valgrind
 PAGES_BUILD_DIR ?= build/pages
 UV_CACHE_DIR ?= $(CURDIR)/.uv-cache
 export UV_CACHE_DIR
+# Set the default before unexport, which otherwise defines an empty variable.
+TIMEOUT ?= 300
+# Command-line values are otherwise expanded for Make's implicit environment,
+# even by parse-time $(shell ...) calls. Export only the raw demo copies below.
+unexport INPUT TIMEOUT
 
 CPPFLAGS ?= -Iinclude
 CFLAGS ?= -std=c17 -Wall -Wextra -Wpedantic -O2
@@ -84,7 +89,7 @@ SERIAL_LIBRARY := $(LIB_DIR)/libwang.a
 SHARED_LIBRARY := $(LIB_DIR)/libwang.so
 OPENMP_LIBRARY := $(LIB_DIR)/libwang_openmp.a
 
-.PHONY: all setup serial shared openmp check c-check python-check pages-check \
+.PHONY: all setup demo-setup demo demo-check serial shared openmp check c-check python-check pages-check \
 	generated-pages-check \
 	strict-check sanitizer-check analyzer-check valgrind-check \
 	cachegrind-check benchmark benchmark-smoke benchmark-compare \
@@ -97,6 +102,26 @@ all: serial shared
 setup:
 	$(UV) sync --frozen
 
+# Keep these steps in one recipe: missing prerequisites must stop setup even -j.
+demo-setup: export DEMO_SETUP_CC = $(CC)
+demo-setup: export DEMO_SETUP_UV = $(UV)
+demo-setup:
+	@$(PYTHON) tools/demo_setup.py preflight
+	$(UV) sync --locked
+	$(UV) sync --locked --directory renderer
+	$(MAKE) shared
+	@$(PYTHON) tools/demo_setup.py verify
+
+# Pass raw values through the environment: filenames are not shell/Make code.
+demo: export TILING_DEMO_INPUT = $(value INPUT)
+demo: export TILING_DEMO_TIMEOUT = $(value TIMEOUT)
+demo:
+	@$(PYTHON) tools/demo.py
+
+demo-check: export TILING_DEMO_TIMEOUT = $(value TIMEOUT)
+demo-check:
+	@$(PYTHON) tools/demo_check.py
+
 serial: $(SERIAL_LIBRARY)
 
 shared: $(SHARED_LIBRARY)
diff --git a/README.md b/README.md
index 8556b96..36071bf 100644
--- a/README.md
+++ b/README.md
@@ -3,17 +3,19 @@
 [![CI](https://github.com/xtraid/tiling-foundry/actions/workflows/ci.yml/badge.svg)](https://github.com/xtraid/tiling-foundry/actions/workflows/ci.yml)
 [![License](https://img.shields.io/badge/license-MIT-blue.svg)](LICENSE)
 
-Can a fixed set of just 23 Wang tiles encode an NP-complete problem? Tiling
-Foundry turns the Yang--Zhang construction into an inspectable, tested software
-pipeline: a formula becomes a finite simply connected region, independent
-engines decide it, and separate checkers validate every published SAT witness.
+Can a fixed set of just 23 Wang tiles encode an NP-complete problem?
 
-This is a research implementation, not a general-purpose tiling library. Its
+Tiling Foundry turns the Yang–Zhang construction into an experimental framework
+for finding, cross-verifying, and explaining solutions, with an eye toward
+performance.
+
+This is not a general-purpose tiling library. Its
 main concern is keeping the mathematical reduction, search, verification, and
 presentation boundaries visible enough to audit and measure. The previous
 experimental codebase remains frozen under `legacy/`.
 
 **Read:** [Documentation](https://xtraid.github.io/tiling-foundry/) ·
+[Presentazione](https://xtraid.github.io/tiling-foundry/presentazione/) ·
 [Pipeline](https://xtraid.github.io/tiling-foundry/pipeline/) ·
 [Worked example](https://xtraid.github.io/tiling-foundry/worked-example/) ·
 [Reference](https://xtraid.github.io/tiling-foundry/reference/) ·
@@ -22,15 +24,16 @@ experimental codebase remains frozen under `legacy/`.
 
 ## Why this repository exists
 
-The 2024 Yang--Zhang result proves NP-completeness for tiling finite simply
+The 2024 Yang--Zhang result establishes NP-completeness for tiling finite simply
 connected regions with one fixed set of 23 Wang tiles. Turning that compact
 proof into software exposes practical questions: which representation owns a
 claim, how the reduction is checked apart from search, how independent engines
 are compared, and what evidence is needed before parallelism.
 
-Tiling Foundry answers those questions with explicit ownership, an executable
-reference solver, differential tests, independent oracles and verifiers, and
-reproducible captures.
+The repository implements the construction, two serial search paths, and
+separate Boolean and Wang checks. Reproducible runs connect each result to its
+input, witnesses, and diagnostics. These tests check the software; the theorem
+and its proof belong to the [Yang–Zhang paper](#primary-reference).
 
 ## Quick start
 
@@ -39,18 +42,102 @@ userspace. The toolchain uses Linux/POSIX facilities including `mmap`, `/proc`,
 Valgrind, and dynamic loading of `libwang.so`; Windows and macOS are not
 currently supported.
 
-Install a C17 compiler, `make`, OpenMP support, and
-[`uv`](https://docs.astral.sh/uv/), then run:
+For the full dossier, install a C17 compiler, `make`, Python 3.11 or newer,
+Git, [`uv`](https://docs.astral.sh/uv/getting-started/installation/), and
+pdfLaTeX. On Debian 13, the system packages are:
+
+```sh
+sudo apt-get update
+sudo apt-get install --no-install-recommends \
+  build-essential python3 git ca-certificates curl texlive-latex-base
+```
+
+On Arch Linux / Omarchy, install the equivalent prerequisites:
+
+```sh
+sudo pacman -Syu --needed base-devel python git ca-certificates curl texlive-latex
+```
+
+Arch's [`texlive-latex`](https://archlinux.org/packages/extra/any/texlive-latex/)
+pulls in `texlive-basic` and `texlive-bin` and supplies the LaTeX packages used
+by the report. If setup reports `pdflatex is missing`, install this package,
+check `pdflatex --version`, then rerun `make demo-setup` while online.
+
+If `uv` is not installed, download and inspect the standalone installer before
+running it. The version used for the setup check is 0.12.1:
 
 ```sh
-git clone https://github.com/xtraid/tiling-foundry.git
+curl -LsSf https://astral.sh/uv/0.12.1/install.sh -o /tmp/uv-install.sh
+cat /tmp/uv-install.sh
+sh /tmp/uv-install.sh
+export PATH="$HOME/.local/bin:$PATH"
+uv --version
+```
+
+Clone the fixed release and prepare the project:
+
+```sh
+git clone --branch v1.0.0 --depth 1 https://github.com/xtraid/tiling-foundry.git
 cd tiling-foundry
-make check
+make demo-setup
 ```
 
-`make check` builds the serial executable and shared library, runs the C and
-core Python tests, builds the OpenMP scaffold, and exercises both serial solver
-paths. It does not require a GPU.
+`demo-setup` checks the compiler and compiles a small PDF with the real report
+template before installing dependencies. It then builds `libwang.so` and
+checks Z3, image rendering, and fonts. A missing prerequisite stops setup with
+an error; the target does not install system packages.
+
+The two Python environments stay separate: `.venv` uses Python 3.11 or newer;
+`renderer/.venv` uses Python 3.14, selected by `renderer/.python-version`.
+Both are installed with `uv sync --locked`. The first setup needs network
+access to download packages and, when absent, the renderer's Python. Keep the
+environments and uv-managed interpreter installed for offline use. No global
+`pip` installation or GPU is needed.
+
+Generate the first complete dossier from the included SAT case:
+
+```sh
+UV_OFFLINE=1 uv run --locked python tools/generate_run_dossier.py \
+  examples/run-cases-v2/pipeline-sat.json \
+  build/first-dossier --pdf
+```
+
+Open `build/first-dossier/report.pdf`. The output directory must be new for each
+run. `UV_OFFLINE=1` also reaches the renderer subprocesses. The command runs
+the four engines and checks the recorded results before producing the figures
+and PDF.
+
+Run the short, narrated verification suite after setup:
+
+```sh
+make demo-check
+```
+
+It checks parsing, known SAT and UNSAT cases, agreement between the four engines,
+and rejection of an altered witness. It stops at the first failure and prints
+the measured duration after success. See the
+[suite guide](docs/run_dossiers.md#suite-breve-commentata)
+for the six checks, diagnostics, and timeout options.
+
+### Run a new input
+
+After `make demo-setup`, give the demo a CM1-in-3 file without an expected result:
+
+```sh
+make demo INPUT='path/to/new formula.cm13' TIMEOUT=300
+```
+
+The command copies the input, runs each of the four engines once, checks their
+results, and produces the figures and PDF using the installed environments
+offline. It prints the PDF path only after the complete dossier succeeds.
+Each invocation retains its input, original name/hash and log in a new directory
+under `build/demo/`.
+
+`TIMEOUT` is a global limit in seconds, including capture, figures and PDF.
+Timeout, cancellation, UNKNOWN, disagreement or an incomplete trace fail with
+diagnostics; they do not mean UNSAT. Arbitrary inputs have no completion-time
+guarantee. The [dossier guide](docs/run_dossiers.md#new-cm1-in-3-input)
+describes the input format, output and diagnostic options.
 
 ## Current status
 
@@ -121,19 +208,32 @@ follows one named SAT source through the same contracts and checks.
 - Parallel search is deferred until the cleaned serial baseline has new
   evidence and explicit ownership tests.
 
-## Next milestones
+## Exam Ready release and next milestones
+
+**v1.0.0 Exam Ready** provides three commands: `make demo-setup` prepares the
+environment, `make demo INPUT=...` produces a checked dossier and PDF, and
+`make demo-check` runs the short narrated suite. The full workflow has been
+rehearsed on Debian and on an Omarchy laptop, including offline runs and PDF
+inspection. See the [release notes](RELEASE_NOTES.md) for prerequisites,
+measured rehearsal times, and limits.
 
-Work proceeds in this order:
+**Release checkpoint:** publish the tag and GitHub Release, then verify the
+documented commands from a fresh clone of that tag and open the resulting
+dossier on the presentation computer. A local freeze or merged PR alone does
+not complete this milestone.
 
-1. freeze the current visual documentation and PDF work;
-2. T99: split fast, integration, and evidence verification into reusable CI
+The [Exam Ready plan](docs/plans/2026-09-15-exam-ready-v1.0.md) records the six
+sessions and acceptance criteria. After the release and project defense, work
+resumes in this order:
+
+1. split fast, integration, and evidence verification into reusable CI
    levels;
-3. T100: perform a behavior-preserving structural cleanup of the serial
+2. perform a behavior-preserving structural cleanup of the serial
    solver;
-4. collect a new serial baseline, hard-UNSAT evidence, and the public option
+3. collect a new serial baseline, hard-UNSAT evidence, and the public option
    matrix;
-5. introduce a minimal `TaskPlan` with an equivalent serial executor;
-6. add and measure real OpenMP execution only after those gates pass.
+4. introduce a minimal `TaskPlan` with an equivalent serial executor;
+5. add and measure real OpenMP execution only after those gates pass.
 
 ## Build, test, and reproduce
 
@@ -144,6 +244,12 @@ make clean
 make check
 ```
 
+`make check` builds the serial libraries, runs the C and core Python tests,
+builds the OpenMP scaffold, and exercises both serial solver paths. The core
+checks require a C17 compiler with OpenMP support, `make`, Python and `uv`;
+they do not require LaTeX. The full dossier setup above also prepares the
+renderer and PDF tools.
+
 The renderer is an isolated locked Python project and has its own suite:
 
 ```sh
diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
new file mode 100644
index 0000000..38e2dbd
--- /dev/null
+++ b/RELEASE_NOTES.md
@@ -0,0 +1,73 @@
+# v1.0.0 — Exam Ready
+
+This release packages the serial Yang–Zhang pipeline for a reproducible
+demonstration: prepare the environments, check known cases, and turn a new
+CM1-in-3 input into a verified dossier with figures and a PDF.
+
+## Run the release
+
+Install the Linux system prerequisites in the [README](README.md#quick-start),
+including pdfLaTeX. Debian and Arch/Omarchy commands are provided there.
+The first setup needs network access; later demo commands use the installed
+environments offline.
+
+```sh
+git clone --branch v1.0.0 --depth 1 https://github.com/xtraid/tiling-foundry.git
+cd tiling-foundry
+make demo-setup
+make demo-check
+make demo INPUT=tests/instances/demo_sat.cm13
+make demo INPUT=tests/instances/pipeline_unsat_search.cm13
+```
+
+To demonstrate offline operation, disconnect the network after setup and run
+the last three commands. Open the PDF path printed after each successful demo.
+Keep the installed environments, managed Python interpreter, and generated
+materials available for the presentation. Save presentation copies outside
+`build/`, which is removed by `make clean`.
+
+For a new input, use `make demo INPUT='path/to/formula.cm13' TIMEOUT=300`.
+The header must be `p cm13 n n`, followed by `n` three-literal clauses;
+each declared variable occurs exactly three times, including repeated
+occurrences within a clause. The [dossier guide](docs/run_dossiers.md)
+describes the full format and output.
+
+## What is included
+
+- `make demo-setup` checks C17, the real PDF template, Z3, rendering and fonts,
+  and prepares both locked Python environments.
+- `make demo-check` narrates six checks covering parsing, SAT/UNSAT, agreement
+  between four engines, and rejection of a corrupted witness.
+- `make demo INPUT=...` accepts an input without an expected result. Reference,
+  optimized, Boolean Z3 and Wang Z3 each run once; figures and PDF reuse the
+  recorded capture. Input bytes, original name/hash and diagnostics survive.
+- SAT witnesses are independently checked. UNSAT records engine agreement
+  and marks witness-only sections not applicable. Trace is not an independent
+  UNSAT certificate.
+- Timeout, UNKNOWN, disagreement, incomplete traces and cancellation are
+  failures. They never become UNSAT or a completed dossier. Every invocation
+  uses a new directory, preserving earlier successful runs.
+- The documentation, figures and PDF support the demonstration, including
+  compact-region trace legends and routing labels that fit their boxes.
+
+## Rehearsal evidence and limits
+
+The workflow was exercised on Debian and an Omarchy laptop. On Omarchy, the
+initial rehearsal at `7ea377e` measured setup at 28.644 s, the six-check suite
+at 12.781 s, SAT/PDF at 132.138 s and UNSAT/PDF at 69.300 s. After the layout
+correction, UNSAT/PDF at `0215b73` took 66.289 s and the user confirmed that
+all text was readable. These are observations on that laptop, not timing
+guarantees or CI performance thresholds. Published-tag acceptance is recorded
+with the GitHub Release and its accompanying evidence.
+
+Linux is the supported platform. The core Python environment requires 3.11
+or newer; the renderer uses Python 3.14. NumPy, Pillow and Z3 are locked;
+the GPU is not required. Arbitrary inputs can exceed the global timeout or
+trace capacity, and wide regions can require zoom to inspect individual cells.
+Wang Z3 dominated the observed laptop runtime.
+
+Updated v2 readers accept earlier v2 dossiers. A strict older reader may
+reject a new-input dossier whose `expected_status` is null; use the readers
+shipped with this release. Dossier v1 and the independent solver/checker
+boundaries remain supported. No OpenMP solver or new serial optimization is
+introduced here; CI restructuring and serial cleanup follow the exam.
diff --git a/docs/assets/narrative/manifest.json b/docs/assets/narrative/manifest.json
index 0ceb9c2..51f8a9d 100644
--- a/docs/assets/narrative/manifest.json
+++ b/docs/assets/narrative/manifest.json
@@ -39,7 +39,7 @@
       },
       "animation": {
         "path": "pipeline-overview/trace.gif",
-        "sha256": "00c0f4681796b570f84e06e3bd95b8c1a1970e991534c744cf06ab56f9d9dad4",
+        "sha256": "1d31c465992d628ac71ac14e46b95d101822614994601cdeb72995e0b1ce0026",
         "media_type": "image/gif"
       },
       "fallback": {
@@ -49,7 +49,7 @@
       },
       "contact_sheet": {
         "path": "pipeline-overview/contact-sheet.png",
-        "sha256": "30a3386b19ab61db925c9112bd4b532c37f3f295abbe2fbd0448fdf5cf75491f",
+        "sha256": "fdaaa8be19a0fd41c5f1d0b5a821e718e25dfa353d0b9153f335cfc2fec9b5d9",
         "media_type": "image/png"
       },
       "frames": [
@@ -70,12 +70,12 @@
         },
         {
           "path": "pipeline-overview/frame-03.png",
-          "sha256": "25385a460ccde9b56ac811a63797d589aa65a4e4f58278e47aebbaaa58086d56",
+          "sha256": "09c9083358fc315addbc57a3e2fc6e6cf5761112f45e32cfbaf4ba4814b3f4aa",
           "media_type": "image/png"
         },
         {
           "path": "pipeline-overview/frame-04.png",
-          "sha256": "01d9e048e5ae2d98a1cc71abb6b2881c94fbf5e07e035617d28756ec2c114419",
+          "sha256": "c700039e4ab4ed89307ee724438162dc90f6b94c2a2d578c4b1fa09b82d621df",
           "media_type": "image/png"
         },
         {
@@ -228,68 +228,68 @@
       },
       "animation": {
         "path": "reference-trace/trace.gif",
-        "sha256": "3b76531c890d77276b264090c3a033c8f612198026ac9fa842bf5f8d8dc220af",
+        "sha256": "a60882c8ec69a3be22099fb3f9e3358eadcf0d45188f1f10f9968a9970bcd66a",
         "media_type": "image/gif"
       },
       "fallback": {
         "path": "reference-trace/frame-002517.png",
-        "sha256": "02e56bb73f7e471a68b17b9aab7cca90b7f59549e81db667472356aa62474e42",
+        "sha256": "4978c3e4d5abdd3c5368a65c5e3ef85d03c55eaac39784eeceb045f2d1f40b9f",
         "media_type": "image/png"
       },
       "contact_sheet": {
         "path": "reference-trace/contact-sheet.png",
-        "sha256": "a01abf57d04e10c3cb3fb290fac6ccd454836d92772fafa8a51eadd357a7df42",
+        "sha256": "2f4a8eda4ae3ac1c0108afac2706b5f26173c2f7a1de3390f21f6f9504fb7757",
         "media_type": "image/png"
       },
       "frames": [
         {
           "path": "reference-trace/frame-000000.png",
-          "sha256": "70af813fd336d1b0147c5e75dc23a35db9a2824d2fd280b65dd5ccc286e07db2",
+          "sha256": "1d7af8868cc259961984f235aa50d3c6eac71f876b1eefc2a24a2b8bf5ea0cc6",
           "media_type": "image/png"
         },
         {
           "path": "reference-trace/frame-000001.png",
-          "sha256": "582d40c0bf9549e3cc059d269c827d93d28d5faafe71945c687e19d52e234908",
+          "sha256": "a27d027e851fadce2fd74c87f832235630043833303ed9ba701d247b8d2c6af4",
           "media_type": "image/png"
         },
         {
           "path": "reference-trace/frame-001258.png",
-          "sha256": "9e51b3fb61137ea4c7c8dad0ea5ab8d76a77abc8c047e69a87856d9ce1d4b33c",
+          "sha256": "961e475c123dddd908b92fd43d5115db8706e541cbf80f2e05b049c3aa58dd29",
           "media_type": "image/png"
         },
         {
           "path": "reference-trace/frame-002516.png",
-          "sha256": "d26026ece1b2704c85f1841f5ecb17f23f6ae91d78e6f62ca7a9cdc543ddefc9",
+          "sha256": "2ff86d94be387e0bc76acd1a39cdcfc7fc34c9cd9136a3b66d01553738abb459",
           "media_type": "image/png"
         },
         {
           "path": "reference-trace/frame-002517.png",
-          "sha256": "02e56bb73f7e471a68b17b9aab7cca90b7f59549e81db667472356aa62474e42",
+          "sha256": "4978c3e4d5abdd3c5368a65c5e3ef85d03c55eaac39784eeceb045f2d1f40b9f",
           "media_type": "image/png"
         },
         {
           "path": "reference-trace/frame-002518.png",
-          "sha256": "06c8086922cf55b323747d137b9b77a9f723fc49555ae21399fffbca39f49090",
+          "sha256": "bc3e3c8bec1c05fec23ed42ac7165e21274cafdca094242cebe3116ce11013de",
           "media_type": "image/png"
         },
         {
           "path": "reference-trace/frame-002519.png",
-          "sha256": "ca4a9846d80808c49f627e73bc6c92cbacd5eee889f7169043906e102d3079d6",
+          "sha256": "88cc8d17d86df21449f0121e5aa6e11500ae5f4792c7596d833e08f92121b3b6",
           "media_type": "image/png"
         },
         {
           "path": "reference-trace/frame-002893.png",
-          "sha256": "75ae40691fd22486ac5ce6eeaf38008154d25a9da94b7588039984f68b46e463",
+          "sha256": "87489d6158ac3dd559debca79b8cee4670f9d3ae5a78adf05f5dc19f5072bd92",
           "media_type": "image/png"
         },
         {
           "path": "reference-trace/frame-002894.png",
-          "sha256": "aa2f00e31c6a48aa0e634217cd4ebf2b0371f8aeda65e7fce96528c2749a4fe6",
+          "sha256": "1b08307c075207102a7a09253bbf4a6e2c57337abfcf3823d5795925dffe9557",
           "media_type": "image/png"
         },
         {
           "path": "reference-trace/frame-002895.png",
-          "sha256": "bea7dae9cd8ccc445d8c0c68ebc5cab90b179bdd3dd37231d6574c727bae01aa",
+          "sha256": "ae7f5261d4dc73f5ad634100194ae9ba2f94cc771a33ac01e4f209dba9987138",
           "media_type": "image/png"
         }
       ]
@@ -311,68 +311,68 @@
       },
       "animation": {
         "path": "optimized-trace/trace.gif",
-        "sha256": "1cb69f87ac4116ed03e63503a8de962683144bb5f3e2c73d51935249e51b1245",
+        "sha256": "ecfe5481d400be9cbcef94ae4317eaacf2a81d8c67a84e596c1ee6e758d2a5bc",
         "media_type": "image/gif"
       },
       "fallback": {
         "path": "optimized-trace/frame-002562.png",
-        "sha256": "f69f64ef5cfcda039a95f316cc254a8492ae6470d85d1d37744c411e198e70c8",
+        "sha256": "c52991c9699a016a58de7ef959362bd92bd28907153e68e2ed430fc62d856f9b",
         "media_type": "image/png"
       },
       "contact_sheet": {
         "path": "optimized-trace/contact-sheet.png",
-        "sha256": "5f4771ead510b9647f993202cb9454552a700a684a5d73c4869d737fc83943d4",
+        "sha256": "dd898619c4110ae38276dfa9efae006a65297cbfb46172569c7cb0347827d7ef",
         "media_type": "image/png"
       },
       "frames": [
         {
           "path": "optimized-trace/frame-000000.png",
-          "sha256": "a0c053db834ce837c360396254ed67cb4a989f28ca79b464574e25a1f97c8573",
+          "sha256": "88685c108d41a398f370f94020da0daecbee9952721539a8af9b52f38057bca7",
           "media_type": "image/png"
         },
         {
           "path": "optimized-trace/frame-000001.png",
-          "sha256": "8f7d3e8240de5573c0c357ad144514511bb984d4466ff7115a692290eabae679",
+          "sha256": "1cabd9372179c361bf67ae29bfde923a3158886bf58136bf904034538335f232",
           "media_type": "image/png"
         },
         {
           "path": "optimized-trace/frame-001281.png",
-          "sha256": "e6bf99bda8c659b878923e805805ced14858381e75173d6f9d177db6b7a6c397",
+          "sha256": "df00288e4d8f37b5164a3636bf581fd26af0bed690dc5193d52f04f4da50d8e8",
           "media_type": "image/png"
         },
         {
           "path": "optimized-trace/frame-002561.png",
-          "sha256": "54aadf70edba02f29677e41f38482d5aea2b3e563bd9c19f7a1f858a6d525dea",
+          "sha256": "03254e8f3df055900fe5db3dd732f19fc25bb4513e4d0a3bffd44b78b2379478",
           "media_type": "image/png"
         },
         {
           "path": "optimized-trace/frame-002562.png",
-          "sha256": "f69f64ef5cfcda039a95f316cc254a8492ae6470d85d1d37744c411e198e70c8",
+          "sha256": "c52991c9699a016a58de7ef959362bd92bd28907153e68e2ed430fc62d856f9b",
           "media_type": "image/png"
         },
         {
           "path": "optimized-trace/frame-002563.png",
-          "sha256": "cf35cf6381fecb7197452f939583869e3ddc20578560b582638e4aed17ae764f",
+          "sha256": "d69dcbc775b2358e90ca46edbf94aab66ed3f9d7aeaa8e2dae12f7767f1fd6e3",
           "media_type": "image/png"
         },
         {
           "path": "optimized-trace/frame-002564.png",
-          "sha256": "cbdc6623aacfb77231d2036e4712fc2bb4de39e581a70112a916819bfac60f57",
+          "sha256": "b76d96ea437b14bcf29e29ea72c30f6699883c465c55b5f8ad16dfdd8ce78a70",
           "media_type": "image/png"
         },
         {
           "path": "optimized-trace/frame-002938.png",
-          "sha256": "3e01b52b7c8ed41ddcd1dad5a4f3e29888a865b06ddb2cc34289aaf317c8bb18",
+          "sha256": "3ae2884356dbe57629602f30f0e3c2e5ee4aed8791543ee1d101f7efa55576a5",
           "media_type": "image/png"
         },
         {
           "path": "optimized-trace/frame-002939.png",
-          "sha256": "fefcc7f6544266dc29c47798c5fff5ce204182f9acbdccf1fe0ac709ec3263b7",
+          "sha256": "71ba23b538689616bde0861a84773d8d0fd2525f11df5f374e8d831e11ae4878",
           "media_type": "image/png"
         },
         {
           "path": "optimized-trace/frame-002940.png",
-          "sha256": "35a279477066232120455d1a46dd97717463cc4ab60126d456b6441c1882b2c4",
+          "sha256": "e3c088c8786084864a40ad1f27923c53ee7032dc50255384f6c8862740018e40",
           "media_type": "image/png"
         }
       ]
@@ -649,7 +649,7 @@
       "compositor": "renderer.wang_narrative.render_overview_assets",
       "artifact": {
         "path": "pipeline-overview/worked-example.png",
-        "sha256": "3128491828307934c63546fcc9e42c2538293eb1027fdcd53ba1b97cd039519d",
+        "sha256": "3d6db9aa32c2fa81baa166ce1e6efef4df6e522b0c5826c1e865f1b6adcfad2b",
         "media_type": "image/png"
       }
     },
diff --git a/docs/assets/narrative/optimized-trace/contact-sheet.png b/docs/assets/narrative/optimized-trace/contact-sheet.png
index 1a40dc4..96bf1c6 100644
Binary files a/docs/assets/narrative/optimized-trace/contact-sheet.png and b/docs/assets/narrative/optimized-trace/contact-sheet.png differ
diff --git a/docs/assets/narrative/optimized-trace/frame-000000.png b/docs/assets/narrative/optimized-trace/frame-000000.png
index 1eca3b5..14b750c 100644
Binary files a/docs/assets/narrative/optimized-trace/frame-000000.png and b/docs/assets/narrative/optimized-trace/frame-000000.png differ
diff --git a/docs/assets/narrative/optimized-trace/frame-000001.png b/docs/assets/narrative/optimized-trace/frame-000001.png
index f6914d9..dde833c 100644
Binary files a/docs/assets/narrative/optimized-trace/frame-000001.png and b/docs/assets/narrative/optimized-trace/frame-000001.png differ
diff --git a/docs/assets/narrative/optimized-trace/frame-001281.png b/docs/assets/narrative/optimized-trace/frame-001281.png
index 6deb0ac..3486a7c 100644
Binary files a/docs/assets/narrative/optimized-trace/frame-001281.png and b/docs/assets/narrative/optimized-trace/frame-001281.png differ
diff --git a/docs/assets/narrative/optimized-trace/frame-002561.png b/docs/assets/narrative/optimized-trace/frame-002561.png
index a415b93..6829a92 100644
Binary files a/docs/assets/narrative/optimized-trace/frame-002561.png and b/docs/assets/narrative/optimized-trace/frame-002561.png differ
diff --git a/docs/assets/narrative/optimized-trace/frame-002562.png b/docs/assets/narrative/optimized-trace/frame-002562.png
index 65c2fdc..4e2b48c 100644
Binary files a/docs/assets/narrative/optimized-trace/frame-002562.png and b/docs/assets/narrative/optimized-trace/frame-002562.png differ
diff --git a/docs/assets/narrative/optimized-trace/frame-002563.png b/docs/assets/narrative/optimized-trace/frame-002563.png
index ab8bcc4..7bb0e07 100644
Binary files a/docs/assets/narrative/optimized-trace/frame-002563.png and b/docs/assets/narrative/optimized-trace/frame-002563.png differ
diff --git a/docs/assets/narrative/optimized-trace/frame-002564.png b/docs/assets/narrative/optimized-trace/frame-002564.png
index 95429ed..ab282b9 100644
Binary files a/docs/assets/narrative/optimized-trace/frame-002564.png and b/docs/assets/narrative/optimized-trace/frame-002564.png differ
diff --git a/docs/assets/narrative/optimized-trace/frame-002938.png b/docs/assets/narrative/optimized-trace/frame-002938.png
index 8dde9ad..d2efd73 100644
Binary files a/docs/assets/narrative/optimized-trace/frame-002938.png and b/docs/assets/narrative/optimized-trace/frame-002938.png differ
diff --git a/docs/assets/narrative/optimized-trace/frame-002939.png b/docs/assets/narrative/optimized-trace/frame-002939.png
index c69154e..19677d5 100644
Binary files a/docs/assets/narrative/optimized-trace/frame-002939.png and b/docs/assets/narrative/optimized-trace/frame-002939.png differ
diff --git a/docs/assets/narrative/optimized-trace/frame-002940.png b/docs/assets/narrative/optimized-trace/frame-002940.png
index 1a76c57..e36947f 100644
Binary files a/docs/assets/narrative/optimized-trace/frame-002940.png and b/docs/assets/narrative/optimized-trace/frame-002940.png differ
diff --git a/docs/assets/narrative/optimized-trace/trace.gif b/docs/assets/narrative/optimized-trace/trace.gif
index f0a51fc..7f2ac52 100644
Binary files a/docs/assets/narrative/optimized-trace/trace.gif and b/docs/assets/narrative/optimized-trace/trace.gif differ
diff --git a/docs/assets/narrative/pipeline-overview/contact-sheet.png b/docs/assets/narrative/pipeline-overview/contact-sheet.png
index 34255d9..e923d62 100644
Binary files a/docs/assets/narrative/pipeline-overview/contact-sheet.png and b/docs/assets/narrative/pipeline-overview/contact-sheet.png differ
diff --git a/docs/assets/narrative/pipeline-overview/frame-03.png b/docs/assets/narrative/pipeline-overview/frame-03.png
index 44acefb..12441e4 100644
Binary files a/docs/assets/narrative/pipeline-overview/frame-03.png and b/docs/assets/narrative/pipeline-overview/frame-03.png differ
diff --git a/docs/assets/narrative/pipeline-overview/frame-04.png b/docs/assets/narrative/pipeline-overview/frame-04.png
index 5d49502..6fc353e 100644
Binary files a/docs/assets/narrative/pipeline-overview/frame-04.png and b/docs/assets/narrative/pipeline-overview/frame-04.png differ
diff --git a/docs/assets/narrative/pipeline-overview/trace.gif b/docs/assets/narrative/pipeline-overview/trace.gif
index c00bdc6..b40820c 100644
Binary files a/docs/assets/narrative/pipeline-overview/trace.gif and b/docs/assets/narrative/pipeline-overview/trace.gif differ
diff --git a/docs/assets/narrative/pipeline-overview/worked-example.png b/docs/assets/narrative/pipeline-overview/worked-example.png
index f92a3a0..1ada1d7 100644
Binary files a/docs/assets/narrative/pipeline-overview/worked-example.png and b/docs/assets/narrative/pipeline-overview/worked-example.png differ
diff --git a/docs/assets/narrative/reference-trace/contact-sheet.png b/docs/assets/narrative/reference-trace/contact-sheet.png
index b542e13..3a8f708 100644
Binary files a/docs/assets/narrative/reference-trace/contact-sheet.png and b/docs/assets/narrative/reference-trace/contact-sheet.png differ
diff --git a/docs/assets/narrative/reference-trace/frame-000000.png b/docs/assets/narrative/reference-trace/frame-000000.png
index 94dfe7f..976f5f6 100644
Binary files a/docs/assets/narrative/reference-trace/frame-000000.png and b/docs/assets/narrative/reference-trace/frame-000000.png differ
diff --git a/docs/assets/narrative/reference-trace/frame-000001.png b/docs/assets/narrative/reference-trace/frame-000001.png
index 605afcb..6411c9c 100644
Binary files a/docs/assets/narrative/reference-trace/frame-000001.png and b/docs/assets/narrative/reference-trace/frame-000001.png differ
diff --git a/docs/assets/narrative/reference-trace/frame-001258.png b/docs/assets/narrative/reference-trace/frame-001258.png
index 1a6a336..2e0331c 100644
Binary files a/docs/assets/narrative/reference-trace/frame-001258.png and b/docs/assets/narrative/reference-trace/frame-001258.png differ
diff --git a/docs/assets/narrative/reference-trace/frame-002516.png b/docs/assets/narrative/reference-trace/frame-002516.png
index d72ea6c..7a319d0 100644
Binary files a/docs/assets/narrative/reference-trace/frame-002516.png and b/docs/assets/narrative/reference-trace/frame-002516.png differ
diff --git a/docs/assets/narrative/reference-trace/frame-002517.png b/docs/assets/narrative/reference-trace/frame-002517.png
index ce8e0e1..3d8d87d 100644
Binary files a/docs/assets/narrative/reference-trace/frame-002517.png and b/docs/assets/narrative/reference-trace/frame-002517.png differ
diff --git a/docs/assets/narrative/reference-trace/frame-002518.png b/docs/assets/narrative/reference-trace/frame-002518.png
index 2b98fb1..de3f17d 100644
Binary files a/docs/assets/narrative/reference-trace/frame-002518.png and b/docs/assets/narrative/reference-trace/frame-002518.png differ
diff --git a/docs/assets/narrative/reference-trace/frame-002519.png b/docs/assets/narrative/reference-trace/frame-002519.png
index 409d6c3..60be3e8 100644
Binary files a/docs/assets/narrative/reference-trace/frame-002519.png and b/docs/assets/narrative/reference-trace/frame-002519.png differ
diff --git a/docs/assets/narrative/reference-trace/frame-002893.png b/docs/assets/narrative/reference-trace/frame-002893.png
index 391349b..c69612e 100644
Binary files a/docs/assets/narrative/reference-trace/frame-002893.png and b/docs/assets/narrative/reference-trace/frame-002893.png differ
diff --git a/docs/assets/narrative/reference-trace/frame-002894.png b/docs/assets/narrative/reference-trace/frame-002894.png
index 8dd7808..ea0a7bb 100644
Binary files a/docs/assets/narrative/reference-trace/frame-002894.png and b/docs/assets/narrative/reference-trace/frame-002894.png differ
diff --git a/docs/assets/narrative/reference-trace/frame-002895.png b/docs/assets/narrative/reference-trace/frame-002895.png
index cc138af..dd44bef 100644
Binary files a/docs/assets/narrative/reference-trace/frame-002895.png and b/docs/assets/narrative/reference-trace/frame-002895.png differ
diff --git a/docs/assets/narrative/reference-trace/trace.gif b/docs/assets/narrative/reference-trace/trace.gif
index 10cd347..42e87e6 100644
Binary files a/docs/assets/narrative/reference-trace/trace.gif and b/docs/assets/narrative/reference-trace/trace.gif differ
diff --git a/docs/index.md b/docs/index.md
index cc24941..840d170 100644
--- a/docs/index.md
+++ b/docs/index.md
@@ -5,7 +5,7 @@ permalink: /
 page_kind: home
 page_class: story
 owned_assets: home_preview
-description: A research software laboratory for finite Wang tilings and inspectable solver design.
+description: From a CM1-in-3 formula to a region over 23 Wang tiles, checked solutions, and a reproducible PDF dossier.
 ---
 
 <section class="home-hero layout-reading" data-wang-sections data-content-column>
@@ -14,12 +14,15 @@ description: A research software laboratory for finite Wang tilings and inspecta
   <h1>Tiling Foundry</h1>
 
   <p>
-    Follow one Cubic Monotone 1-in-3 SAT instance through independent Boolean
-    and Wang models, the Yang–Zhang construction, two native solver paths,
-    explicit verification, and presentation-only views.
+    Can a region be tiled using a fixed set of 23 Wang tiles? Tiling Foundry
+    turns a Cubic Monotone 1-in-3 SAT formula into such a region using the
+    Yang–Zhang construction. Four decision paths compare results, separate
+    checkers validate SAT witnesses, and a PDF dossier records the run.
   </p>
 
   <div class="story-actions">
+    <a class="text-link" href="{{ '/run-dossiers/' | relative_url }}">Run the demo</a>
+    <a class="text-link" href="{{ '/presentazione/' | relative_url }}">Follow the technical tour</a>
     <a class="text-link" href="{{ '/pipeline/' | relative_url }}">Explore the pipeline</a>
     <a class="text-link" href="{{ '/worked-example/' | relative_url }}">Inspect the worked example</a>
   </div>
@@ -32,7 +35,7 @@ description: A research software laboratory for finite Wang tilings and inspecta
   </div>
 
   <ol class="pipeline-links">
-    <li>The fixed <a href="{{ '/components/tileset/' | relative_url }}">tile vocabulary</a> supplies one immutable domain.</li>
+    <li>The fixed <a href="{{ '/components/tileset/' | relative_url }}">tile vocabulary</a> contains the 23 tiles used by every Wang solver.</li>
     <li><a href="{{ '/components/boolean-z3/' | relative_url }}">Boolean Z3</a> checks the source formula.</li>
     <li><a href="{{ '/components/yang-zhang/' | relative_url }}">Yang–Zhang</a> constructs one finite Wang region.</li>
     <li><a href="{{ '/components/reference-solver/' | relative_url }}">Reference</a> and <a href="{{ '/components/optimized-solver/' | relative_url }}">optimized</a> native paths solve the same region.</li>
@@ -45,17 +48,17 @@ description: A research software laboratory for finite Wang tilings and inspecta
 <section class="home-section layout-presentation" id="verified-output" data-content-column>
   <div class="section-heading">
     <p class="eyebrow">Verified output</p>
-    <h2>A selected result, not a visual proof</h2>
+    <h2>A checked tiling from one SAT run</h2>
   </div>
 
   {% include narrative-static.html asset_id="home_preview" image="/assets/narrative/pipeline-overview/home-preview.png" alt="A compact square Wang witness preview for the captured SAT source." width="1520" height="860" label="observed" caption="Selected verified SAT square output for the captured instance." source="wang-solution-v1" %}
 
   <p class="home-section__prose">
-    The image is downstream of an independently checked square witness. Read
+    Independent checkers validated the square tiling shown here. Read
     the <a href="{{ '/worked-example/' | relative_url }}">named example</a> for
-    its source identity and the
+    its input and checks, and the
     <a href="{{ '/components/visualization/' | relative_url }}">visualization component</a>
-    for the transformation boundary.
+    for the square, generalized, and hex views of that same witness.
   </p>
 </section>
 
@@ -67,10 +70,12 @@ description: A research software laboratory for finite Wang tilings and inspecta
 
   <p class="home-section__prose">
     Use the <a href="{{ '/pipeline/' | relative_url }}">pipeline story</a> to
-    understand responsibilities, the <a href="{{ '/reference/' | relative_url }}">reference index</a>
-    for maintained contracts and history, and the
-    <a href="{{ '/evidence/' | relative_url }}">evidence index</a> for dated,
-    source-bound measurements. Reproducible captures remain separately indexed
-    under <a href="{{ '/run-dossiers/' | relative_url }}">run dossiers</a>.
+    follow the input through each component, the
+    <a href="{{ '/reference/' | relative_url }}">reference index</a>
+    for specifications and implementation guides, and the
+    <a href="{{ '/evidence/' | relative_url }}">evidence index</a> for measurements
+    with their dates, inputs, and limits. The
+    <a href="{{ '/run-dossiers/' | relative_url }}">dossier guide</a>
+    explains how to run your own input and inspect the recorded result.
   </p>
 </section>
diff --git a/docs/pipeline.md b/docs/pipeline.md
index e5de333..bc13168 100644
--- a/docs/pipeline.md
+++ b/docs/pipeline.md
@@ -9,9 +9,12 @@ description: Component order, data flow, independence, and trust boundaries from
 
 # The complete pipeline
 
-Tiling Foundry keeps construction, decision, verification, and presentation as
-separate responsibilities. A result is useful only when its source identity,
-component boundary, and independent checks remain visible.
+A CM1-in-3 formula enters four decision paths. When they agree on SAT, their
+returned witnesses must pass independent checks. When they agree on UNSAT,
+the run records that result without claiming an independent UNSAT certificate.
+The dossier and optional PDF reuse the recorded input, results, and checks.
+Use the [demo guide]({{ '/run-dossiers/#new-cm1-in-3-input' | relative_url }})
+to run a new formula through this sequence.
 
 {% include narrative-animation.html asset_id="pipeline_overview" animation="/assets/narrative/pipeline-overview/trace.gif" fallback="/assets/narrative/pipeline-overview/frame-07.png" contact_sheet="/assets/narrative/pipeline-overview/contact-sheet.png" alt="The captured formula moves through Boolean Z3, Yang-Zhang reduction, both native solvers, Wang Z3, verification, and presentation." width="1080" height="620" label="observed" caption="One validated v2 capture in fixed component order." source="wang-run-dossier-v2#named-components" %}
 
@@ -23,7 +26,9 @@ the formula directly. Independently, the
 [Yang–Zhang component]({{ '/components/yang-zhang/' | relative_url }}) constructs
 a finite region over the fixed [tile vocabulary]({{ '/components/tileset/' | relative_url }}).
 The reference solver, optimized solver, and Wang Z3 oracle consume that same
-hash-bound region and tileset.
+region and tileset, identified by their hashes. The paper proves the reduction's
+equivalence; the builder implements it, and the tests check that implementation
+on concrete inputs.
 
 | Step | Input | Output | Relationship |
 | --- | --- | --- | --- |
@@ -48,6 +53,7 @@ they do not trust a raster.
 - `SAT` is accepted only with the applicable witness checks.
 - `UNSAT` from a solver is a terminal observation, not a standalone certificate.
 - `UNKNOWN` is preserved where an oracle can return it; it is never rewritten as UNSAT.
+- Timeout, errors, disagreement, or incomplete traces stop the demo; none means UNSAT.
 - Trace replay presents recorded semantic events but does not solve again.
 - Generalized and hex views are downstream transformations, not new solvers.
 
diff --git a/docs/plans/2026-09-15-exam-ready-s2.md b/docs/plans/2026-09-15-exam-ready-s2.md
new file mode 100644
index 0000000..34edd89
--- /dev/null
+++ b/docs/plans/2026-09-15-exam-ready-s2.md
@@ -0,0 +1,209 @@
+# Exam Ready S2 — input libero e dossier completo
+
+> **For agentic workers:** usare `superpowers:subagent-driven-development` per
+> eseguire e revisionare i task in sequenza. Il coordinatore verifica la chiusura.
+
+**Goal:** `make demo INPUT=...` produce un dossier/PDF completo e verificato da
+una formula CM1-in-3 nuova, senza risultato atteso fornito dall'utente.
+
+**Architecture:** estendere in modo compatibile i contratti esistenti per
+un'aspettativa assente; riusare la cattura v2 e i suoi consumatori. Un processo
+supervisore gestisce il limite complessivo e l'interruzione del worker e dei
+suoi figli. Nessuna seconda pipeline o seconda esecuzione dei motori.
+
+**Tech stack:** Python stdlib, libreria C e adapter esistenti, ambienti uv
+lockati, Z3, renderer esistente e pdfLaTeX. Linux resta la piattaforma supportata.
+
+**Spec:** sezione S2 di `2026-09-15-exam-ready-v1.0.md`. L'analisi concreta dei
+confini è conservata in `build/exam-ready-s2/contract-design.md`.
+
+## Vincoli globali
+
+- Base di sessione `e179cc1` (S1 verificata e committata localmente).
+- Una PR complessiva in S6; commit locali per checkpoint. Nessun push/merge/tag.
+- Core C, ABI, ownership, oracoli, lock e asset canonici restano invariati.
+- Dossier v1 invariati; dossier v2 precedenti ancora leggibili e generabili.
+- Ogni motore eseguito una volta. Il PDF consuma solo la cattura validata.
+- Input nuovo copiato prima del parsing; hash, esportatori e motori usano quei byte.
+- SAT richiede witness validi; UNSAT non inventa witness o certificati.
+- UNKNOWN, timeout, errori, disaccordo e trace incomplete non producono successo.
+- Non cancellare `examples/sudoku3.cm13`, QA, log, fixture o rollback precedenti.
+- S3 suite narrata, S4 riscrittura documentale e S5 CI/QA finale restano separati.
+
+## Decisioni del design
+
+### Aspettativa assente e risultato osservato
+
+`MultiEngineRunCase.expected_status` diventa `str | None`; nei trasporti il
+campo resta obbligatorio e accetta `null`, `sat` o `unsat`. Il comando diretto
+passa sempre `None`. Builder e validator stabiliscono prima che tutti i quattro
+stati siano terminali e uguali; soltanto dopo controllano un'eventuale aspettativa.
+
+```python
+observed_status = statuses["reference"]
+if any(status not in {"sat", "unsat"} for status in statuses.values()):
+    raise PipelineSnapshotError("full-pipeline dossier forbids UNKNOWN results")
+if any(status != observed_status for status in statuses.values()):
+    raise PipelineSnapshotError("engine status mismatch")
+if case.expected_status is not None and case.expected_status != observed_status:
+    raise PipelineSnapshotError("known expected status mismatch")
+```
+
+Tutti i rami di witness, verifiche, tempi applicabili, asset e PDF usano lo stato
+osservato. `agreement.expected_status` conserva esattamente l'aspettativa, anche
+nulla. Gli stati duplicati in agreement devono coincidere con i rispettivi motori.
+
+Il manifest narrativo autonomo necessita di un discriminante osservato esplicito
+solo nella nuova forma; la forma legacy e gli hash canonici restano invariati:
+
+```json
+{"id":"demo-run","expected_status":null,"observed_status":"sat","source_sha256":"<sha256>"}
+```
+
+La nuova forma richiede `observed_status` esattamente quando expected_status è
+null; i casi noti conservano i tre campi precedenti. Le ricevute dispongono già
+dei quattro stati in agreement: non aggiungere un altro campo. Il PDF nuovo
+indica che non è stato fornito un risultato atteso. I vecchi lettori stretti non
+leggono la nuova variante; il codice aggiornato continua a leggere quella vecchia.
+
+### Comando e controllo dei processi
+
+Interfaccia principale: `make demo INPUT=percorso.cm13`, con `TIMEOUT=300` come
+default configurabile in secondi. Il percorso diretto Python espone anche
+output e capacità trace per diagnostica e test; rifiuta timeout non finiti o
+non positivi e capacità fuori dal contratto esistente (2–100000 eventi).
+
+Il supervisore usa soltanto stdlib, seleziona il Python core installato da S1 e
+avvia un worker con `start_new_session=True`. Il limite include preflight,
+copia input, parsing, riduzione, motori, validatori, renderer e LaTeX. In caso
+di timeout/SIGINT/SIGTERM termina l'intero gruppo, attende brevemente e usa
+SIGKILL per i figli ancora attivi. Raccoglie sempre il worker; nessun subprocess
+di rendering o PDF può sopravvivere alla terminazione gestita.
+
+Ogni invocazione crea una directory distinta sotto `build/demo/`, con input
+immutabile, log e sottocartella dossier. Un output esplicito esistente è un
+errore: non sovrascrivere o riutilizzare una run. I byte dell'input e il nome
+originale sono registrati prima di avviare i motori; nei contratti si mantiene
+un nome relativo portabile per la copia. Nessuna interpolazione shell dell'input.
+
+Il worker chiama un solo percorso condiviso in `dossier.multi_engine`.
+Il percorso dei casi JSON continua a chiamare lo stesso percorso, mantenendo
+i metadati legacy. La sorgente viene copiata prima della cattura anche per i
+casi JSON; native capture e trace exporter ricevono la copia, non l'originale.
+Un callback facoltativo Python segnala parsing, riduzione, reference, optimized,
+Boolean Z3, Wang Z3, verifiche, figure e PDF nei punti reali di esecuzione.
+Il callback non cambia ABI o semantica dei solver.
+
+Solo un worker concluso correttamente con dossier/PDF completi può stampare il
+percorso di successo. Errori conservano input/log e indicano chiaramente lo stato
+diagnostico. Eventuali artefatti parziali non sono presentati come dossier riusciti.
+
+## Task 1 — Contratti e consumatori
+
+File: `python/formats/run_case_v2.py`, `run_dossier_v2{,_builder,_bundle}.py`,
+`narrative_assets.py`, `run_report_v2_tex.py`; `python/dossier/narrative_assets.py`;
+`renderer/wang_narrative.py`; tre schemi JSON pertinenti; test dossier/renderer.
+
+- [x] Aggiungere prima test fallenti per null SAT/UNSAT, aspettativa opposta,
+  disaccordo, UNKNOWN e trace incompleta; preservare i test legacy.
+- [x] Applicare i rami osservati descritti sopra e la variante chiusa del manifest.
+- [x] Validare i collegamenti tra run e artefatti: source hash nativo, stato e
+  completezza delle trace, stato dei summary Z3. Testare alterazioni coerenti
+  degli hash del contenitore, così il test verifica il legame semantico.
+- [x] Testare ricevute nullable e manifest alterato; il PDF mostra l'aspettativa
+  assente. Controllare che i dati canonici non cambino.
+- [x] Eseguire i test pertinenti, review indipendente e commit del checkpoint.
+
+## Task 2 — Cattura da file e comando supervisionato
+
+File: `python/dossier/multi_engine.py`, `python/native/multi_engine_pipeline.py`,
+nuovo ingresso `tools/demo.py` e piccolo worker/modulo Python se necessario;
+`Makefile`, README, guida dossier e test demo dedicati.
+
+- [x] Test fallenti: file nuovo esterno, percorso con spazi, output già presente,
+  input alterato dopo copia, un solo invio a ogni motore, progressione reale.
+- [x] Estrarre il percorso condiviso della cattura senza duplicarne il corpo;
+  copiare e fissare l'input prima del parsing e degli hash degli esportatori.
+- [x] Aggiungere supervisore e worker con timeout complessivo e terminazione
+  del gruppo; tenere insieme solo gli helper necessari a questo comando.
+- [x] Testare timeout e interruzione con figli reali, incluso un figlio che
+  ignora SIGTERM; nessun processo vivo residuo e nessun successo parziale.
+- [x] Testare input malformato, dipendenza PDF mancante, trace troncata, errore,
+  UNKNOWN e disaccordo; i messaggi distinguono questi esiti da UNSAT.
+- [x] Documentare comandi, formato `p cm13 n n`, occorrenze cubicità, output,
+  limite globale, diagnosi e assenza di garanzie temporali su input arbitrario.
+- [x] Review del task e commit dopo i controlli pertinenti.
+
+## Task 3 — Accettazione S2 e handoff
+
+- [x] Usare due input nuovi conservati in `build/exam-ready-s2/inputs/`, con
+  esiti individuati per enumerazione indipendente e mai passati alla demo.
+  I primi casi a sei variabili restano evidenza dei limiti: il SAT ha superato
+  100000 eventi per entrambe le trace e raggiunto il timeout di 300 s. Dopo il
+  rifiuto anticipato delle trace incomplete, verificare i PDF su due nuovi casi
+  a tre variabili (otto assegnazioni enumerate), senza aumentare i limiti.
+- [x] Eseguire realmente entrambi i comandi, con rete disabilitata dopo il setup.
+- [x] Riaprire dossier e asset coi validator; verificare copia/hash input,
+  expected_status null, quattro motori concordi e trace complete.
+- [x] Revisionare i PDF SAT/UNSAT e misurare separatamente ciascuna esecuzione.
+- [x] Eseguire suite Python e renderer pertinenti, check documentali e regressioni
+  v1/v2; niente matrice prestazionale non pertinente.
+- [x] Review finale del range S2, chiudere finding e ricontrollare i fix.
+- [x] Registrare commit, hash, log, limiti e QA; aggiornare S2 a FATTO soltanto
+  dopo tutti i criteri. S3–S6 e pubblicazione restano TODO.
+
+## Verifica del piano
+
+| Confine | Produzione/consumo e verifica |
+|---|---|
+| Task 1 → Task 2 | None indica aspettativa assente; il worker lo passa senza solve preventivo. |
+| Task 2 → Task 3 | Input copiato e run unica; QA controlla hash, esiti, trace e terminazione. |
+| Task 1 → Task 3 | Vecchi dossier restano validi; nuove ricevute/PDF esplicitano l'assenza d'aspettativa. |
+| Task 1 interno | Schemi, validator, builder, renderer e PDF condividono la distinzione atteso/osservato. |
+| Task 2 interno | Timeout copre il worker completo; output parziale resta diagnostico. |
+| Task 3 interno | Un test compilato o PDF aperto da solo non chiude i criteri di correttezza. |
+
+Il piano applica lo scope S2 approvato. Le scelte di timeout, nome della copia
+e variante nullable sono dettagli implementativi motivati dai confini esistenti;
+restano soggetti a review. Non richiedono una nuova pipeline o un nuovo schema.
+
+## Chiusura S2 — 19 settembre 2026
+
+**FATTO** sul candidato `98718b2f3ef3bba48adb33af77615d0fac280c1c`.
+I checkpoint precedenti sono `a3ecd66` (contratti), `c737f7a` (comando),
+`5f722de` (rifiuto anticipato trace incomplete) e `a3b9723` (contact sheet).
+L'ultimo fix riassume le annotazioni di costruzione solo quando non entrano;
+frame canonici e dettaglio del singolo crossover restano invariati.
+
+| Accettazione offline finale | SAT | UNSAT |
+|---|---|---|
+| Input nuovo | `inputs/acceptance-sat.cm13` | `inputs/acceptance-unsat.cm13` |
+| Variabili / assegnazioni enumerate | 3 / 8 | 3 / 8 |
+| Aspettativa passata alla demo | nessuna | nessuna |
+| Esito dei quattro motori | SAT | UNSAT |
+| Trace native | complete | complete |
+| Witness check | sei superati | sei non applicabili |
+| Durata completa osservata | 70,316 s | 37,702 s |
+| PDF | 19 pagine | 20 pagine |
+
+I percorsi di evidenza sono relativi a `build/exam-ready-s2/`.
+`acceptance-summary-final.json` conserva percorsi e SHA-256 degli input/PDF;
+`acceptance-validation-final.log` registra la riapertura con i validator.
+`acceptance-final-page-comparison.json` copre le 39 pagine: 29 identiche alla
+prima QA integrale, dieci modificate e ricontrollate visivamente nei report
+`acceptance-sat-pdf-final-review.md` e `acceptance-unsat-pdf-final-review.md`.
+Nessun problema bloccante; nota minore P-M1 MRV conservata ed esplicita.
+
+Verifiche: `acceptance-gates.json` distingue il gate generale precedente
+(17 C / 232 Python) dai gate incrementali dei fix; renderer finale 337/337,
+87 asset canonical-pages rigenerati identici e 91 file protetti invariati.
+Review cumulativa e dei singoli fix conservate; README dell'utente preservato.
+
+I primi tentativi falliti restano evidenza, non risultati riusciti: trace oltre
+capacità nel SAT a sei variabili, contact sheet troppo grande, annotazioni
+costruzione sovrapposte. Le correzioni sono revisionate e verificate; i limiti
+restano espliciti e i dati originali conservati. Setup S2 usa il clone isolato
+e cache S1 già preparate, con rete disabilitata: non è una nuova prova di
+installazione a cache vuota. Quel criterio è coperto dalla chiusura S1.
+
+S3–S6 e pubblicazione restano TODO. Fonte operativa: `handoff-final.md`.
diff --git a/docs/plans/2026-09-15-exam-ready-v1.0.md b/docs/plans/2026-09-15-exam-ready-v1.0.md
new file mode 100644
index 0000000..e5d30d7
--- /dev/null
+++ b/docs/plans/2026-09-15-exam-ready-v1.0.md
@@ -0,0 +1,315 @@
+# Roadmap v1.0.0 — Exam Ready
+
+Data: 15 settembre 2026. **Release: TODO.** Scope concordato per preparare la
+difesa del progetto. **S1–S5 sono FATTO**, con setup isolato, nuovi dossier
+SAT/UNSAT, suite breve offline, documentazione revisionata e prova su Omarchy,
+inclusa la conferma del PDF corretto a `0215b73`.
+S6 è IN CORSO; pubblicazione e verifica dal tag restano da completare.
+
+L'obiettivo è poter clonare una versione precisa, inserire una formula nuova,
+eseguire il progetto con pochi comandi e mostrare un dossier completo con PDF.
+La documentazione deve aiutare a spiegare contributi, correttezza e limiti.
+
+**Milestone principale: v1.0.0 pubblicata e verificata come versione d'esame.**
+Il checkpoint in fondo al piano si chiude soltanto dopo la verifica della
+versione pubblicata. Un freeze locale o una PR integrata non lo completano.
+Scadenza confermata dall'utente il 17 settembre: **mercoledì 23 settembre 2026**.
+Obiettivo operativo: release pubblicata e verificata entro **domenica 20**, con
+lunedì e martedì dedicati alle prove. L'orario della scadenza non è ancora indicato.
+
+## Scope e ordine del lavoro
+
+La release riguarda la baseline seriale esistente: riduzione Yang–Zhang,
+reference, optimized, Boolean Z3, Wang Z3, checker, renderer e dossier.
+Il lavoro aggiunge accesso semplice, riproducibilità e chiarezza espositiva.
+
+Interfaccia prevista: **`demo-setup` implementato e verificato in S1**;
+`demo` implementato e verificato in S2;
+`demo-check` implementato e verificato in S3:
+
+```bash
+make demo-setup
+make demo INPUT=examples/professore.cm13
+make demo-check
+```
+
+`demo` deve produrre il dossier completo e `report.pdf`, poi stamparne il
+percorso. I nomi dei target potranno adattarsi ai comandi già esistenti,
+mantenendo un solo percorso documentato. `professore.cm13` è il file da creare
+con l'input proposto durante la dimostrazione.
+
+| Sessione Astra xhigh | Stato | Risultato | Stima |
+|---|---|---|---|
+| S1 | FATTO | Clone pulito e setup completo | 2–3 ore |
+| S2 | FATTO | Formula nuova → quattro motori → dossier e PDF | 4–6 ore |
+| S3 | FATTO | Suite breve commentata e regressioni della demo | 2–3 ore |
+| S4 | FATTO | Documentazione più chiara e utile alla difesa | 2–3 ore |
+| S5 | FATTO | Prova isolata, offline e sul computer dell'esame | 3–4 ore |
+| S6 | IN CORSO | PR, freeze, pubblicazione e verifica dal tag | 1–2 ore |
+
+Totale stimato: **14–21 ore**, più **2–4 ore di riserva**. Sono stime di lavoro
+con verifica e revisione, non garanzie; download, CI e ambiente possono
+allungare il calendario. S2 contiene la maggiore incertezza tecnica.
+
+Alla chiusura di S5 resta S6, inclusa la verifica dal tag pubblico e dei
+materiali offline distribuiti. La prova generale sul computer dell'esame
+è completata. La stima della tabella non include eventuali attese esterne;
+la milestone resta aperta fino alla verifica della release pubblicata.
+Il calendario non anticipa l'autorizzazione alle singole sessioni o alla
+pubblicazione e va rivisto se emergono problemi tecnici o indisponibilità.
+
+## S1 — Clone pulito e setup completo
+
+Verificare lo stato del repository e la base integrata prima di iniziare.
+Lavorare sulla feature branch dedicata e conservare il file utente
+`examples/sudoku3.cm13`, le QA e gli handoff precedenti.
+
+- Preparare un target che costruisca la libreria e configuri i due ambienti
+  Python con i lock esistenti, rispettando le versioni richieste.
+- Elencare i prerequisiti Linux, incluso LaTeX e quanto serve al PDF; rendere
+  comprensibile una dipendenza mancante prima di avviare la ricerca.
+- Provare l'installazione in un clone pulito e in un ambiente isolato, senza
+  riusare build, ambienti Python o file ignorati del server.
+- Documentare download e comandi esatti; dopo il setup la demo deve poter
+  funzionare senza rete. Non usare `pip` globale.
+
+**Completamento:** il clone isolato arriva alla prima esecuzione documentata
+con tutte le dipendenze necessarie al dossier, e conserva log e ambiente.
+
+**Chiusura verificata il 15 settembre:** `make demo-setup` prepara la libreria
+condivisa, i due ambienti Python con `uv sync --locked` e il PDF usando il
+template reale. Clone, home, cache e installazione Python inizialmente vuoti;
+home dell'host nascosta. Dopo il setup, il comando README sul SAT canonico è
+riuscito con rete disabilitata tramite namespace: dossier/PDF di 23 pagine in
+36,095 s, quattro motori concordi, sei checker verdi e trace complete.
+Validati bundle, asset, copia input/hash e commit della fixture; QA visiva
+campionata su cinque pagine. Verdi otto controlli d'errore del setup, 17 binari C,
+build dello scaffold OpenMP e dieci test dossier v1/TeX. Review e re-review
+senza finding residui. I tempi sono osservazioni di questa prova.
+
+Base operativa `2e3ca52`; il candidato è verificato nel solo clone QA detached
+`abe06ff`, tree `f38dca5`, con 463 input coincidenti prima del test. La sessione
+è stata poi fissata nel checkpoint locale `e179cc1`, all'avvio di S2.
+Evidenze, comandi, ambiente e handoff:
+`build/exam-ready-s1/resume-20260915T161536/`. S1 verifica il caso noto già
+distribuito; input nuovi SAT/UNSAT, QA completa e prova sul computer dell'esame
+restano nelle sessioni successive.
+
+## S2 — Input nuovo, dossier completo e PDF
+
+Accettare direttamente un file Cubic Monotone 1-in-3 senza risultato atteso.
+La guida deve spiegare il formato: intestazione `p cm13 n n`, con `n > 0`,
+seguita da `n` clausole di tre indici positivi tra `1` e `n`, terminate da `0`.
+Ogni variabile compare esattamente tre volte nell'intera formula; le eventuali
+ripetizioni vengono contate. Non è un ingresso per SAT generico.
+
+Il primo lavoro è risolvere il ruolo di `expected_status`, oggi presente nei
+casi, nel documento della run, nei validatori e negli asset. Separare
+l'aspettativa indipendente di un test noto dalla decisione osservata su input
+libero: non copiare il risultato del solver in un campo poi presentato come
+conferma indipendente. Conservare la compatibilità dei dossier precedenti.
+Un eventuale adattamento contrattuale deve essere minimo, motivato dal caso
+concreto e revisionato; non introdurre preventivamente schemi o framework.
+
+- Conservare una copia immutabile dell'input con hash e commit del progetto.
+  La riduzione e tutti i motori devono consumare quell'input identificato.
+- Eseguire reference, optimized, Boolean Z3 e Wang Z3 una volta ciascuno;
+  riusare adapter, esportatori, checker e catena di composizione esistenti.
+  Figure e PDF consumano i risultati registrati, senza solve o rerun nascosti.
+- Mostrare avanzamento reale: parsing, riduzione, motori, verifiche, figure,
+  PDF. Identificare ogni esecuzione e impedire il riuso accidentale di output
+  vecchi come risultato della nuova formula.
+- Gestire timeout e interruzione sull'intero gruppo di processi, inclusi
+  renderer e LaTeX; conservare log utili e liberare le risorse.
+- Distinguere SAT, UNSAT, UNKNOWN, timeout, errore, disaccordo dei motori e
+  trace tronca. Nessuno stato inconcludente può essere presentato come UNSAT.
+- Presentare come riuscito soltanto un dossier completo e validato. Gli
+  output parziali restano diagnostici. Non inventare witness o certificati
+  UNSAT: dichiarare esattamente quali motori e controlli sostengono l'esito.
+- Confrontare status e validità dei witness, senza richiedere che motori
+  diversi trovino lo stesso witness. Non aggiungere vincoli iniziali nascosti
+  per rendere più semplice la formula proposta.
+
+**Completamento:** cambiare formula non richiede modifiche a codice o risultati
+attesi; almeno un nuovo SAT e un nuovo UNSAT producono dossier e PDF coerenti.
+Misurare separatamente la durata del dossier sulla macchina scelta, senza
+promettere tempi costanti per qualsiasi formula.
+
+**Chiusura verificata il 19 settembre:** candidato `98718b2`, dopo i checkpoint
+contratti `a3ecd66`, comando `c737f7a` e fix di accettazione. Due input nuovi a
+tre variabili, verificati per enumerazione indipendente, hanno prodotto dossier
+completi nel clone QA con rete disabilitata: **SAT 70,316 s / 19 pagine** e
+**UNSAT 37,702 s / 20 pagine**. Nessun risultato atteso passato alla demo;
+copia/hash, quattro motori concordi, trace complete, bundle e asset validati.
+Tutte le 39 pagine sono coperte dalla QA: lettura iniziale integrale, confronto
+dei raster finali e ispezione di tutte le dieci pagine modificate.
+
+Review del codice e dei fix senza finding residui; nessun finding PDF bloccante.
+Resta la nota minore P-M1: una riga secondaria MRV è parzialmente coperta, ma le
+informazioni della decisione sono ripetute interamente nel riquadro principale.
+Le panoramiche di regioni larghe richiedono zoom, come documentato nella guida.
+Renderer finale **337/337**; **87 asset canonici rigenerati identici**. Il gate
+generale precedente aveva 17 C e 232 Python verdi; i fix successivi sono coperti
+da gate mirati, test dei processi e nuove prove offline, senza ripetere i motori
+all'interno di una run. Core, ABI, oracoli, lock e dossier v1 preservati.
+
+Limite osservato: il primo SAT a sei variabili supera i 100000 eventi per trace.
+Ora fallisce esplicitamente prima di export/Z3 (39,302 s nella prova), senza
+dossier incompleto presentato come successo. Nessuna garanzia su input arbitrari.
+Fonti: `build/exam-ready-s2/handoff-final.md`, `acceptance-summary-final.json`,
+review finali SAT/UNSAT e [piano S2](2026-09-15-exam-ready-s2.md).
+La prova sul computer dell'esame e la verifica della versione pubblicata restano
+rispettivamente S5 e S6.
+
+## S3 — Suite breve spiegabile durante l'esecuzione
+
+Preparare sei controlli rappresentativi, annunciati con una frase che spieghi
+cosa viene verificato e perché:
+
+1. Lettura di un input valido.
+2. Rifiuto di un input malformato o fuori dai vincoli del problema.
+3. Caso SAT con verifica indipendente del witness.
+4. Caso UNSAT noto, senza generare un witness inesistente.
+5. Accordo reference/optimized e confronto con Z3 su istanze piccole.
+6. Alterazione di una tessera e rifiuto del witness da parte del checker.
+
+La suite deve fermarsi su un fallimento e restituire un esito di processo
+corretto. Aggiungere regressioni mirate della nuova demo per timeout,
+interruzioni, errori, output incompleti e seconda esecuzione, senza duplicare
+l'intera suite del progetto nel comando dimostrativo.
+
+**Completamento:** controlli comprensibili, fallimenti riconoscibili e durata
+misurata. L'obiettivo di **30–60 secondi dopo il setup** riguarda questa suite,
+non il dossier; non diventa una soglia temporale della CI.
+
+**Chiusura S3 verificata il 20 settembre:** codice `3722f70`, review senza
+finding residui, 31 test mirati verdi in 25.119 s. Due esecuzioni reali di
+`make demo-check` con rete e renderer nascosti: 6/6 controlli in 6.274 e
+6.275 s complessivi, directory distinte e prima run preservata. I 30–60 s
+non erano un minimo; nessuna attesa aggiunta. Corretto anche il default
+TIMEOUT Make per entrambi i comandi. Fonti: piano S3 del 19 settembre e
+`build/exam-ready-s3/handoff-final.md`.
+
+## S4 — Documentazione leggibile e utile alla difesa
+
+Revisionare README, home, guida alla demo, Presentazione, pipeline ed esempio
+guidato. Mettere prima problema, contributo, comandi e risultato; eliminare
+introduzioni generiche, ripetizioni, gergo superfluo e riferimenti ai task
+interni dal percorso principale. Accorpare le spiegazioni duplicate e usare
+frasi concrete, esempi reali e affermazioni misurate.
+
+Rendere meno prominenti cronologie e dettagli operativi; conservare accessibili
+prove, dati, riferimenti scientifici e limiti. Distinguere il risultato teorico
+di Yang–Zhang, l'implementazione realizzata e le verifiche sperimentali.
+Spiegare la differenza tra controllo di un witness SAT e risultato UNSAT.
+Mantenere le etichette semantiche e le distinzioni necessarie alla correttezza.
+
+**Completamento:** un lettore segue il percorso senza conoscere la storia dei
+task; comandi, link, figure e pagine modificate passano i controlli pertinenti.
+
+**Chiusura verificata il 20 settembre:** sei pagine revisionate, con problema,
+contributo e percorso demo in apertura, suite/v2 prima dei diagnostici v1 e
+distinzione esplicita fra teorema, implementazione e prove. Review indipendente
+senza finding; WIP README dell'utente, ancore, include, asset e comandi
+preservati. Pages 41 route, 26 test checker, build Jekyll offline e verifica
+di 41 pagine HTML/929 riferimenti verdi. QA browser delle cinque pagine a
+1440 e 390 px, movimento normale/ridotto: 20 combinazioni coperte, più sei
+controlli mirati; lettura visiva desktop/mobile senza finding residui.
+Due misure premature delle ancore sono state ricontrollate dopo lo scorrimento;
+la figura home è stata verificata dopo decodifica, senza modifiche al sito.
+Nessun codice, contratto, renderer o lock modificato. Fonti:
+[piano S4](2026-09-20-exam-ready-s4.md) e
+`build/exam-ready-s4/handoff-final.md`. Prova d'esame e pubblicazione restano
+S5 e S6.
+
+## S5 — Prova generale e verifica dell'ambiente d'esame
+
+**FATTO.** L'utente ha completato la prova
+locale su Omarchy al commit `7ea377e`: setup, suite offline 6/6 (12.781 s),
+dossier SAT (132.138 s) e UNSAT (69.300 s), apertura PDF, errori, timeout,
+Ctrl+C e riavvio con preservazione dei PDF precedenti superati. Evidenza
+riferita dall'utente, distinta dalla prova isolata Debian sul server.
+L'UNSAT valido è `tests/instances/pipeline_unsat_search.cm13`; il vecchio
+esempio ad hoc della checklist era fuori dominio. Il follow-up corregge
+S5-I1, le righe secondarie della legenda e le etichette routing; PDF
+ricomposti e revisionati sul server. L'utente ha poi confermato HEAD
+`0215b73` e il nuovo PDF `run-nq7tup8a` completamente leggibile su Omarchy:
+UNSAT e validazione finale riusciti in 66.289 s reali. S5 è chiusa.
+Piano operativo: [S5](2026-09-20-exam-ready-s5.md).
+
+- Ripetere esattamente i comandi della guida da clone isolato: setup con rete,
+  poi demo e suite senza rete, senza dipendenze da percorsi personali.
+- Provare almeno un nuovo SAT e un nuovo UNSAT con struttura diversa dai casi
+  canonici, oltre a input errato, timeout, interruzione e seconda esecuzione.
+- Revisionare i nuovi PDF: input, risultati, titoli, didascalie, impaginazione
+  e sezioni non applicabili. La compilazione riuscita da sola non basta.
+- Aggiungere una verifica CI mirata della demo, usando gli stessi comandi
+  locali; eseguire i gate pertinenti a codice, contratti, renderer e Pages.
+- Provare sul computer della presentazione. Se si usa il server, verificare
+  trasferimento e apertura della copia del dossier senza repository o rete.
+- Preparare materiale offline coerente con la versione candidata, registrare
+  tempi effettivi di suite e dossier e individuare eventuali problemi bloccanti.
+
+**Completamento:** percorso riproducibile e prova reale di apertura riusciti,
+QA conservata e revisione finale senza problemi bloccanti.
+
+## S6 — Freeze, pubblicazione e controllo della versione distribuita
+
+**IN CORSO su autorizzazione dell'utente dopo la chiusura S5.** Sono incluse
+PR, merge, tag e release, seguiti dalla verifica del clone pubblico.
+Le quattro modifiche README dell'utente vengono incluse con revisione su
+sua conferma esplicita. Fonte operativa: `build/exam-ready-s6/handoff-current.md`.
+
+Completare PR e revisione, aggiornare i metadati di versione pertinenti e
+preparare note di release con contenuto, piattaforma verificata, comandi e
+limiti. Fissare commit e tree del candidato verificato e controllare la CI.
+Dopo il merge, confrontare il tree integrato con il candidato; eventuali
+differenze richiedono verifica prima del tag. Eseguire tag `v1.0.0` e GitHub
+Release secondo l'autorizzazione del task applicabile, poi controllare il
+risultato pubblico.
+
+Provare un nuovo clone del tag pubblicato con gli stessi comandi documentati,
+inclusa l'esecuzione offline dopo il setup. La formalizzazione di questo piano
+non esegue pubblicazione o implementazione delle sessioni.
+
+## CHECKPOINT PRINCIPALE — v1.0.0 PUBBLICATA E VERSIONE D'ESAME VERIFICATA
+
+**Stato: TODO. Questo è il traguardo della preparazione tecnica.**
+
+- [ ] S1–S5 concluse e verificate; nessun problema bloccante aperto, note
+  minori residue esplicite e compatibili con la demo.
+- [ ] PR integrata, revisione chiusa e CI pertinente verde sul codice
+  candidato; SHA e tree integrati confrontati con quelli congelati.
+- [ ] Tag `v1.0.0` e GitHub Release pubblici, coerenti con il commit verificato.
+- [ ] Clone nuovo del tag: comandi della guida riusciti, demo e suite offline
+  dopo il setup, nessuna dipendenza da file locali non distribuiti.
+- [ ] Dossier completi validati su input nuovi SAT e UNSAT; PDF revisionati,
+  suite commentata riuscita e tempi effettivi registrati.
+- [ ] Guida e note della release riportano prerequisiti, comandi, contributi
+  e limiti; materiali offline trasferiti e aperti sul computer dell'esame.
+- [ ] Versione da mostrare fissata precisamente per demo, slide e materiali;
+  conservati SHA, tag, URL release, log, ambiente, tempi e QA. Registrare
+  anche gli hash degli eventuali allegati pubblicati.
+
+**Segnare FATTO soltanto dopo pubblicazione e verifica successiva dal tag.**
+Se emergono problemi, correggere e ripetere i controlli pertinenti prima della
+chiusura; il solo merge o freeze non sostituisce questo checkpoint.
+
+## Dopo la release e gestione delle sessioni
+
+Ordine: **release verificata → prove e difesa → T99 → T100 → fase C → fase D**.
+Restano fuori dallo scope Exam Ready: T99 completo, refactor T100, OpenMP,
+`TaskPlan`, nuove ottimizzazioni, grandi campagne di benchmark, supporto
+Windows/macOS e riscrittura integrale della documentazione.
+
+Conservare indipendenza degli oracoli, ABI, ownership e semantica del core;
+renderer e documentazione restano consumatori downstream. Non duplicare la
+pipeline né trasformare `run.json` in un motore di orchestrazione.
+
+Ogni sessione ha un responsabile distinto quando pratico; il coordinatore
+verifica il risultato prima della chiusura. Lasciare un handoff breve con
+stato (`TODO`, `IN CORSO`, `FATTO`, `BLOCCATO`), commit, risultati verificati,
+evidenze, rischi e prossimo passo. Conservare QA e modifiche dell'utente;
+eseguire controlli proporzionati ed evitare cambiamenti concorrenti alle
+stesse dipendenze. Usare la sessione di riserva per problemi emersi, mantenendo
+prioritari il checkpoint di pubblicazione e il tempo per le prove orali.
diff --git a/docs/plans/2026-09-19-exam-ready-s3.md b/docs/plans/2026-09-19-exam-ready-s3.md
new file mode 100644
index 0000000..1c18c31
--- /dev/null
+++ b/docs/plans/2026-09-19-exam-ready-s3.md
@@ -0,0 +1,104 @@
+# Exam Ready S3 — suite breve narrata
+
+> **For agentic workers:** usare `superpowers:subagent-driven-development`;
+> responsabile S3 distinto, review indipendente e accettazione del coordinatore.
+
+**Goal:** `make demo-check` esegue sei controlli rappresentativi, spiega cosa
+dimostrano e si ferma al primo fallimento con un codice di uscita corretto.
+
+**Architecture:** un comando lineare usa parser, adapter native, oracoli e
+checker esistenti. Riusa il supervisore di `tools/demo.py` senza modificarlo.
+Ogni motore viene eseguito una volta per caso; non genera dossier o PDF.
+
+**Tech stack:** Linux, Python stdlib e ambiente core lockato, libreria C e Z3.
+
+**Spec:** sezione S3 del piano `2026-09-15-exam-ready-v1.0.md`, già approvato.
+Preflight tecnico: `build/exam-ready-s3/preflight.md`. Base locale `0247b29`.
+
+## Vincoli globali
+
+- Nessuna modifica a core, ABI, oracoli, formati, lock, renderer o supervisore S2.
+- Sei blocchi annunciati prima di eseguirli; nessun framework di registrazione.
+- Aspettative SAT/UNSAT note indipendentemente e distinte dall'esito osservato.
+- UNKNOWN, eccezioni, disaccordo e witness non validi interrompono la suite.
+- Nessun download o setup implicito; prerequisiti mancanti indicano il setup.
+- Nessuna attesa artificiale: 30–60 secondi è un obiettivo da misurare,
+  non una soglia CI. Misurare separatamente dal dossier.
+- Preservare README utente, `examples/sudoku3.cm13` e ogni QA/rollback.
+- Unica PR complessiva in S6; qui solo checkpoint locali.
+
+## Decisioni concrete
+
+1. Leggere `tests/instances/pipeline_sat.cm13` col parser C e controllarne
+   il contenuto atteso.
+2. Rifiutare `tests/fuzz/corpus/cm13/malformed_domain.cm13` precisamente come
+   errore di dominio: un errore I/O non dimostra il rifiuto dell'input.
+3. Risolvere il SAT con reference e verificare tiling e assegnazione tramite
+   il percorso indipendente esistente. Il caso ammette `(False, True, False)`.
+4. Risolvere `tests/instances/pipeline_unsat_search.cm13`: la clausola
+   `4 4 4` richiederebbe `3*x4 = 1`. Richiedere UNSAT e witness assenti.
+5. Confrontare i risultati reference già ottenuti con optimized, Boolean Z3
+   e Wang Z3 su entrambi i casi. Controllare i witness SAT, senza richiedere
+   che motori indipendenti scelgano lo stesso witness.
+6. Copiare il tiling SAT e sostituire una sola tessera con un ID valido che
+   viola un bordo imposto. Il checker deve rifiutare la copia e accettare
+   ancora l'originale. Stampare la cella e gli ID coinvolti.
+
+Una directory nuova `build/demo-check/run-*` conserva il log. Il worker scrive
+un marker privato `complete` contenente `6/6\n` soltanto dopo tutti i controlli;
+il parent richiede exit zero e marker esatto prima di annunciare successo.
+CLI: `--timeout` positivo/finito, default 300, e `--output` nuovo facoltativo.
+Make passa `TIMEOUT` raw nell'ambiente. Codici diretti: 124 timeout,
+130/143 interruzioni, 1 fallimento, 2 argomenti; Make restituisce il suo nonzero.
+
+## Review focus
+
+- Errore infrastrutturale scambiato per rifiuto del parser.
+- UNKNOWN o witness mancante/alterato scambiato per risultato terminale valido.
+- Uscita zero senza tutti i controlli scambiata per suite riuscita.
+- Timeout/interruzione propagati male dalla nuova entrypoint al supervisore.
+- Seconda invocazione che riusa o altera i risultati della prima.
+
+## Task 1 — Comando, regressioni e guida
+
+File: nuovo `tools/demo_check.py`, `tests/python/test_demo_check.py`,
+target in `Makefile`, sezione in `docs/run_dossiers.md`.
+
+- [x] Scrivere e osservare test fallenti per i sei controlli e i fallimenti
+  elencati sopra; registrare RED/GREEN nel report di implementazione.
+- [x] Implementare il comando minimo con le API indicate nel preflight.
+- [x] Verificare una sola chiamata per motore/caso e il tamper di una tessera
+  con ID valido; mantenere attivi i controlli anche con Python ottimizzato.
+- [x] Provare errori parser, UNKNOWN, disaccordo, witness invalidi e fail-fast.
+- [x] Provare marker assente/errato, codici di errore, argomenti invalidi,
+  directory esistente e passaggio letterale di TIMEOUT da Make.
+- [x] Eseguire test S3 e regressioni CLI/processi S2. La matrice reale del
+  supervisore esiste già: non duplicarla, aggiungere il collegamento S3.
+- [x] Documentare sei controlli, comandi, prerequisiti, log e limiti.
+- [x] Review indipendente, correzioni pertinenti e checkpoint locale.
+
+## Task 2 — Accettazione e chiusura
+
+- [x] Aggiornare il clone QA preservato al candidato revisionato.
+- [x] Eseguire due `make demo-check` offline, misurando separatamente i tempi.
+- [x] Verificare sei controlli, esito zero e directory distinte; confrontare
+  hash di log e marker della prima esecuzione dopo la seconda.
+- [x] Verificare fonti congelate, modifiche utente preservate e gate pertinenti.
+- [x] Registrare evidenze, note residue e stato S3 nella roadmap e nell'handoff.
+
+S4–S6 restano successive; il successo della suite sul server non sostituisce
+la prova sul computer dell'esame o la verifica dal tag pubblico.
+
+## Chiusura verificata — 20 settembre 2026
+
+S3 FATTO sul codice `3722f70` (implementazione `05ae767`). Review finale
+senza finding residui. Il test offline ha scoperto e fatto correggere il
+default TIMEOUT vuoto: 300 va assegnato prima di unexport nel Makefile.
+La regressione copre entrambi i comandi demo/demo-check e il vuoto esplicito.
+
+31 test mirati verdi in 25.119 s; due run offline con renderer nascosto in
+6.274 / 6.275 s complessivi, 6/6 controlli. Seconda run in directory distinta,
+prima run preservata byte per byte. Il target 30–60 s non era un minimo;
+nessuna attesa artificiale aggiunta. Pages 41 route verdi. README utente e
+sudoku3 preservati; nessuna pubblicazione. Fonte delle evidenze:
+`build/exam-ready-s3/handoff-final.md`.
diff --git a/docs/plans/2026-09-20-exam-ready-s4.md b/docs/plans/2026-09-20-exam-ready-s4.md
new file mode 100644
index 0000000..40d0ffb
--- /dev/null
+++ b/docs/plans/2026-09-20-exam-ready-s4.md
@@ -0,0 +1,79 @@
+# Exam Ready S4 — percorso documentale per la difesa
+
+> **For agentic workers:** usare `superpowers:subagent-driven-development`;
+> owner editoriale distinto, review indipendente, QA finale del coordinatore.
+
+**Stato: FATTO il 20 settembre 2026.** Verifica finale e checkpoint locale
+registrati in `build/exam-ready-s4/handoff-final.md`.
+
+**Goal:** un lettore trova problema, contributo, comandi e risultati senza
+conoscere la storia interna del progetto.
+
+**Architecture:** revisione editoriale delle sei pagine esistenti. La guida
+porta in apertura setup, suite e nuovo input; dettagli v1 restano accessibili.
+Nessuna nuova pagina, route, figura, astrazione o modifica funzionale.
+
+**Tech stack:** Markdown/Liquid, Jekyll e checker Pages esistenti.
+
+**Spec:** S4 della roadmap `2026-09-15-exam-ready-v1.0.md`, già approvata;
+preflight concreto in `build/exam-ready-s4/preflight.md`. Base `400c332`.
+
+## Vincoli
+
+- Preservare esattamente le frasi modificate dall'utente nel README; root
+  separa gli hunk della sessione dalle sue modifiche non committate.
+- Preservare ancore, include, fonti, label semantiche, alt/caption e asset.
+- Lingua delle pagine invariata, inclusa Presentazione in inglese e la
+  sezione italiana della suite nella guida.
+- Distinguere risultato teorico Yang–Zhang, implementazione e prove eseguite;
+  witness SAT controllabile, UNSAT osservato senza certificato inventato.
+- Mantenere indipendenza e dipendenze condivise dei quattro motori esplicite.
+- Comandi già verificati S1–S3; nessun claim di release già pubblicata.
+- Solo sei pagine; niente nuovi test che ripetano la prosa, nuovo codice,
+  renderer, PDF, benchmark, lock o cambi ai checker.
+- Preservare QA/rollback e sudoku3; nessuna pubblicazione o cleanup.
+
+## Task 1 — Sei pagine coerenti
+
+File: `README.md`, `docs/index.md`, `docs/run_dossiers.md`,
+`docs/presentazione.md`, `docs/pipeline.md`, `docs/worked-example.md`.
+
+- [x] README: correggere stato dei comandi, aggiungere percorso Presentazione
+  e togliere identificatori di task interni dalla sequenza futura.
+- [x] Home: aprire con formula, regione e risultato, collegare la guida demo.
+- [x] Guida: tre comandi in apertura, suite/v2 prima dei casi v1; conservare
+  tutte le ancore, il formato di input e i dettagli di compatibilità.
+- [x] Presentazione/pipeline: aperture concrete, teoria/implementazione/prove
+  distinte; mantenere casi osservati, SAT/UNSAT e confini di verifica.
+- [x] Esempio: rendere leggibile il caso a tre variabili e la sua assegnazione,
+  raccordare la riproduzione senza duplicare il quickstart.
+- [x] Eseguire diff-check, pages-check e i due moduli di test dei checker.
+- [x] Review indipendente di semantica, comandi, link e preservazione del WIP.
+
+## Task 2 — QA e chiusura
+
+- [x] Generare Pages con immagine Jekyll già presente, rete disabilitata,
+  sorgente read-only e nuova directory di output conservata.
+- [x] Eseguire checker HTML generato e verificare le cinque pagine pubblicate
+  a desktop/390 px, incluse ancore, figure, navigazione e reduced motion.
+- [x] Verificare i sei file congelati contro review e output; registrare
+  limiti o finding, aggiornare roadmap e handoff, checkpoint locale.
+
+S5 prova d'esame/CI e S6 pubblicazione restano successive. I gate si ampliano
+solo se una modifica effettiva o un finding lo richiede.
+
+## Evidenze di chiusura
+
+- Review indipendente: `build/exam-ready-s4/review-20260920-resume.md`, nessun
+  finding; sei file congelati per hash, README utente preservato.
+- Gate: Pages 41 route, 26 test checker, Jekyll offline e checker HTML
+  41 pagine/929 riferimenti. Report `resume-20260920T032702Z/checks.md`.
+- Browser: cinque pagine × due viewport (1440/390 px) × due preferenze di
+  movimento. Prima passata 18/20 verdi; i due casi guida con scroll animato
+  sono verdi nel supplemento che attende l'arrivo all'ancora. Sei verifiche
+  mirate aggiuntive su home, guida ed esempio. Tutti i tentativi conservati.
+- QA visiva desktop/mobile: report in `build/exam-ready-s4/closure/`;
+  immagine home verificata dopo scroll e decodifica. Nessun finding residuo.
+- Solo documentazione; nessun rilancio di solver/PDF o rigenerazione degli
+  asset. I quattro hunk README dell'utente restano separati dal checkpoint;
+  `examples/sudoku3.cm13`, rollback e QA preservati.
diff --git a/docs/plans/2026-09-20-exam-ready-s5.md b/docs/plans/2026-09-20-exam-ready-s5.md
new file mode 100644
index 0000000..6f1b7b4
--- /dev/null
+++ b/docs/plans/2026-09-20-exam-ready-s5.md
@@ -0,0 +1,181 @@
+# Exam Ready S5 — prova generale e computer d'esame
+
+**Stato: FATTO.** Codice finale verificato `0215b73`, base `04a2919`,
+branch `feature/exam-ready-v1.0`.
+Scope autorizzato dal continua dell'utente il 20 settembre. Coordinatore
+`/root`, responsabile CI `/root/exam_s5_rehearsal`, review distinta prima
+del checkpoint. S6 resta successiva.
+
+L'utente ha eseguito la demo direttamente sul proprio PC Omarchy Linux
+al commit `7ea377e`, con esiti ricevuti il 21 settembre e registrati sotto.
+Ha poi confermato il commit `0215b73` e l'apertura del nuovo dossier UNSAT,
+con tutti i testi leggibili e senza sovrapposizioni o tagli.
+La prova Debian sul server e la verifica della macchina d'esame sono evidenze
+separate; entrambe vanno registrate senza estendere i risultati da un host
+all'altro. Il piano Exam Ready principale resta il criterio di accettazione.
+
+## Scope e preservazione
+
+- Clone QA da commit, home/cache/interpreti inizialmente vuoti, setup con
+  rete e comandi della guida senza rete dopo setup.
+- Un SAT con struttura diversa dal caso canonico e un nuovo UNSAT, input
+  errato, timeout, interruzione e seconda esecuzione. Aspettative dei test
+  stabilite indipendentemente, mai passate alla demo come risultato atteso.
+- Validazione input/hash/commit, quattro motori, trace, bundle e PDF;
+  revisione visiva integrale dei nuovi PDF e materiali offline identificati.
+- CI minima nel job renderer esistente: setup, suite e un input libero SAT;
+  mantenere smoke v1, senza anticipare T99 o duplicare la pipeline.
+- Istruzioni e prova Omarchy con prerequisiti verificati sulle fonti ufficiali,
+  tempi misurati sul PC e apertura reale dei PDF. Nessuna installazione o
+  modifica remota implicita prima di conoscere i prerequisiti mancanti.
+- Preservare i quattro hunk README utente, sudoku3, QA e rollback. Backup
+  iniziale in `build/exam-ready-s5/before/`. Nessun push/merge/tag/release.
+
+## Checklist
+
+- [x] Preflight CI e stato locale: `build/exam-ready-s5/preflight-ci.md`.
+- [x] Modalità d'esame confermata: esecuzione locale su Omarchy.
+- [x] CI mirata implementata, verificata localmente e revisionata (`7ea377e`).
+- [x] Setup da clone/home/cache vuoti; log e ambiente conservati.
+- [x] Suite, SAT/UNSAT e casi d'errore offline; prima run preservata.
+- [x] Dossier/PDF validati e QA visiva completa sul server; finding chiusi.
+- [x] Gate proporzionati sul candidato e review senza finding bloccanti.
+- [x] Setup, suite, dossier e apertura PDF sul PC Omarchy; tempi registrati.
+- [x] Materiali offline, hash, handoff e checkpoint locale delle correzioni.
+- [x] Apertura del PDF corretto su Omarchy, dopo il riscontro al vecchio commit.
+
+## Gate
+
+Una passata `make check` per l'integrazione della branch, test renderer
+pertinenti e prove end-to-end del clone. Riusare i gate già verdi sui byte
+invariati, compresa QA Pages S4; verificare eventuali sezioni documentali
+nuove. Nessuna nuova campagna native/sanitizer/Valgrind per cambi soltanto
+CI e documentali. La CI corrente conserva i propri job fino a T99.
+
+La prova reale sul PC e l'apertura del PDF corretto sono acquisite: S5 è
+FATTO. La pubblicazione verificata dal tag resta S6, ancora TODO.
+
+## Riscontro della macchina d'esame — 21 settembre
+
+Fonte: report dell'utente su Omarchy, branch `feature/exam-ready-v1.0`,
+commit `7ea377e`. Rete scollegata manualmente dopo il setup,
+`UV_OFFLINE=1` e `UV_PYTHON_DOWNLOADS=never`. I tempi qui sono quelli del
+laptop; i PDF e i log locali del laptop non sono stati copiati sul server.
+
+| Prova | Esito riferito | Tempo reale |
+| --- | --- | --- |
+| `make demo-setup` | PASS dopo installazione TeX Live; inizialmente mancava `pdflatex` | 28.644 s |
+| `make demo-check` | PASS 6/6; durata interna 12.603 s | 12.781 s |
+| `make demo INPUT=tests/instances/demo_sat.cm13` | SAT, quattro motori concordi, witness verificati, PDF aperto | 132.138 s |
+| `make demo INPUT=tests/instances/pipeline_unsat_search.cm13` | UNSAT, quattro motori concordi, assegnamento/checker N/A, PDF aperto | 69.300 s |
+| Input malformato | Errore parser; nessun UNSAT o dossier completato | Non misurato |
+| `TIMEOUT=0.01` | Timeout esplicito 124; nessun dossier completato | Non misurato |
+| Ctrl+C, seconda esecuzione e primo PDF | SIGINT 130, diagnostica preservata, nuova run SAT e primo PDF ancora presente | Non misurato |
+
+Ambiente riferito: Python 3.14.7, Z3 5.1.0, NumPy 2.4.6, Pillow 12.2.0;
+PNG, font e `libwang.so` caricati. Wang Z3 domina il tempo osservato sul laptop.
+I codici 124/130 sono quelli della ricetta riportati da Make, non il codice
+di uscita di Make stesso.
+
+Percorsi sul laptop: primo SAT `build/demo/run-vzgafg1m/dossier/report.pdf`,
+UNSAT `build/demo/run-y3hqhlzv/dossier/report.pdf`, riavvio SAT
+`build/demo/run-2dttv76x/dossier/report.pdf`; diagnostiche interrotte
+`build/demo/run-7g8yqqct` e `build/demo/run-xhx_xm0v` preservate.
+Il difetto visuale UNSAT noto resta aperto in questa prova al vecchio commit:
+non equivale all'accettazione dei PDF prodotti dal renderer corretto.
+
+## Checklist ripetibile sul computer d'esame
+
+Installare prima i prerequisiti della propria distribuzione dal
+[README](../../README.md#quick-start), quindi eseguire dalla radice del clone:
+
+```sh
+git rev-parse HEAD
+time make demo-setup
+```
+
+Scollegare la rete dopo il setup e usare i fixture validi del repository:
+
+```sh
+export UV_OFFLINE=1
+export UV_PYTHON_DOWNLOADS=never
+time make demo-check
+time make demo INPUT=tests/instances/demo_sat.cm13
+time make demo INPUT=tests/instances/pipeline_unsat_search.cm13
+```
+
+Questo comando UNSAT **sostituisce l'esempio ad hoc
+`/tmp/tiling-exam-unsat.cm13`** della precedente checklist: due clausole con
+header `p cm13 3 3` sono incomplete; cambiare l'header in `p cm13 3 2` viola
+il dominio CM13. Il parser richiede `n` variabili, `n` clausole e tre
+occorrenze per ogni variabile. Il fixture scelto è:
+
+```text
+p cm13 4 4
+1 1 2 0
+1 2 3 0
+2 3 3 0
+4 4 4 0
+```
+
+Le occorrenze sono corrette e la clausola finale impone `3*x4=1`, impossibile
+per una variabile booleana. Nessun risultato atteso viene passato alla demo.
+Aprire entrambi i PDF ai percorsi stampati, controllare accordo dei quattro
+motori, figure e testi (MRV, propagazione, conflitto, rollback); nel dossier
+UNSAT witness e checker devono essere non applicabili e la trace non deve
+essere presentata come certificato indipendente.
+
+Provare separatamente i due fallimenti attesi:
+
+```sh
+make demo INPUT=tests/fuzz/corpus/cm13/malformed_domain.cm13
+make demo INPUT=tests/instances/demo_sat.cm13 TIMEOUT=0.01
+```
+
+Interrompere poi una demo SAT con Ctrl+C e rilanciarla. Verificare che usi
+una nuova directory, conservi la diagnostica parziale e lasci apribile il
+primo PDF riuscito. Registrare commit, durate e percorsi. Dopo la correzione
+del layout basta ripetere l'apertura/QA del nuovo PDF UNSAT; la verifica
+della versione pubblicata dal tag resta un criterio separato di S6.
+
+## Correzioni dopo il riscontro Omarchy
+
+- Trace: larghezza minima per separare testi e schede; altezza del corpo
+  sufficiente per l'intera legenda, uniforme fra i frame animati. S5-I1 e il
+  precedente residuo P-M1 chiusi nei PDF e negli asset rigenerati.
+- Costruzione: il font fitting esistente si applica anche alle strisce fino
+  a 15 segnali. Chiusa l'ulteriore sporgenza `r #12/#13/#14` rilevata dalla
+  lettura completa del fixture usato sul laptop.
+- Checklist: usa il fixture UNSAT valido esistente, con contratto CM13
+  esplicito; README e diagnostica setup includono Arch/Omarchy.
+
+Evidenze in `build/exam-ready-s5/omarchy-followup-20260921T134347Z/`:
+regressioni prima/dopo, report `layout-review.md` e `fixture-final-review.md`,
+PDF finali `narrow-final/dossier/report.pdf` e
+`fixture-final/dossier/report.pdf`, entrambi di 26 pagine. Ogni ricomposizione
+preserva cattura, input/hash, `run.json` e TeX, senza rilanciare i solver.
+La nuova run del fixture è riuscita in 35.093 s sul server; questo tempo
+non sostituisce i 69.300 s riferiti su Omarchy.
+
+Copia comoda del PDF corretto sul server:
+`~/dossiers/tiling-foundry-unsat-corrected-20260921.pdf`.
+SHA-256 `ef3a444fdd2f6ad88c4c8f33b5dc2f5174ea4f1dd84d4b635651bee12b0c2c7d`.
+Sul laptop l'utente ha rigenerato e aperto il dossier dal codice corretto,
+come registrato nella conferma finale seguente.
+
+## Chiusura S5 — conferma finale Omarchy
+
+L'utente conferma esplicitamente HEAD `0215b73` e il PDF
+`build/demo/run-nq7tup8a/dossier/report.pdf` completamente leggibile,
+senza etichette o legende sovrapposte/tagliate. La nuova demo UNSAT termina
+con validazione finale riuscita in **66.289 s reali** sul laptop; l'hash
+input è `ea2b8feb6eb8f4e722f1ec9021445c84858120c8567d42528631bdfb77400a94`.
+La trascrizione attesta questa demo; non viene usata come esito di un nuovo
+`make check` completo. La prova offline iniziale resta quella sopra a `7ea377e`.
+
+Fonte: `build/exam-ready-s5/omarchy-followup-20260921T134347Z/`, file
+`omarchy-rerun-nq7tup8a.json`, `omarchy-final-confirmation.json` e
+`handoff-final.md`. I vecchi percorsi `build/demo/` del laptop sono storici:
+l'utente ha eseguito `make clean` prima della nuova run. Per S6 verificare
+nuovamente l'inventario dei materiali offline della versione pubblicata.
+S5 è FATTO; S6, tag e release rimangono TODO.
diff --git a/docs/presentazione.md b/docs/presentazione.md
index 8debdcb..85fe06c 100644
--- a/docs/presentazione.md
+++ b/docs/presentazione.md
@@ -9,18 +9,23 @@ description: A compact technical tour through the construction, solver states, a
 
 # Presentazione
 
-Use these concrete states and construction views when explaining how the
-project works. The [pipeline]({{ '/pipeline/' | relative_url }}) remains the
-complete component map; [Reference]({{ '/reference/' | relative_url }}) holds
-the detailed specifications and implementation guides.
+How does a formula become a region, how does search find or rule out a tiling,
+and how is a returned SAT witness checked? This tour answers those questions
+with the implemented construction and recorded solver states. To produce a
+report for a new formula, use the [demo guide]({{ '/run-dossiers/#new-cm1-in-3-input' | relative_url }}).
+The [pipeline]({{ '/pipeline/' | relative_url }}) gives the component map;
+[Reference]({{ '/reference/' | relative_url }}) holds the detailed specifications.
 
 [Construction](#yangzhang-construction) → [native solver](#native-solver) →
 [verification](#verification-dependencies) → [worked result](#one-solved-example).
 
 ## Yang–Zhang construction
 
-**φ SAT ⇔ Rφ tileable with the fixed 23-tile set.** The construction below
-belongs to the same small SAT instance used by the solver examples.
+**φ SAT ⇔ Rφ tileable with the fixed 23-tile set.** This equivalence comes
+from the Yang–Zhang reduction. The project implements its construction and
+tests the resulting software; those tests do not replace the mathematical
+proof. The view below shows the constructed region for the same small SAT
+instance used by the solver examples.
 
 Read the colored spans from left to right: a **variable** chooses a Boolean
 value; **forwarders** preserve it; **crossovers** reorder signals without
diff --git a/docs/run_dossiers.md b/docs/run_dossiers.md
index 07acab1..ad2af5c 100644
--- a/docs/run_dossiers.md
+++ b/docs/run_dossiers.md
@@ -3,106 +3,165 @@ layout: page
 title: Observed-run dossiers and example index
 permalink: /run-dossiers/
 page_class: reference
-description: Opt-in v1 diagnostic reports and v2 multi-engine captures built from hash-bound traces, summaries, witnesses, and raw run metadata.
+description: Run the offline demo and narrated checks, inspect a PDF dossier, or reproduce named v1 and v2 cases.
 section: Architecture and correctness
 document_kind: Reproduction and report contract
 status: Current implementation
-updated: 2026-09-01
+updated: 2026-09-20
 nav_order: 35
 ---
 
 # Observed-run dossiers and example index
 
-The sole public generator dispatches closed v1 and v2 case documents to
-separate implementations. Both are explicitly opt-in and leave parsing,
-reduction, ordinary solving, snapshot export, and the default Wang renderer
-unchanged.
+Run a new CM1-in-3 input through the four engines and keep the checked results,
+figures, and PDF in one dossier. From the repository root, after installing the
+[system prerequisites]({{ site.repository_url }}#quick-start):
 
-The v1 path turns one configured native run into a self-contained directory
-with `run.json`, `report.tex`, `report.pdf`, and `assets/`. Its four diagnostic
-cases, schemas, formatter, template, initial-domain behavior, and output shape
-remain unchanged.
+```sh
+make demo-setup
+make demo-check
+make demo INPUT='path/to/new formula.cm13' TIMEOUT=300
+```
 
-`run.json` is the authoritative report input. It records the source and Git
-identity, environment, solver options and result, complete trace counters,
-initial-domain overrides, raw stage durations, replay scope, and SHA-256 for
-every referenced JSON or raster asset. The LaTeX document and PDF are derived
-from that one document. They do not recalculate events, witness state, timing,
-or provenance.
+Setup downloads the locked dependencies and checks the compiler, renderer, and
+PDF tools. The short suite checks known cases. The demo then accepts your own
+input without an expected result and prints the PDF path after the complete
+dossier succeeds. Both commands run offline after setup; each invocation keeps
+its own diagnostics.
 
-## Example index
+For SAT, the dossier includes checked witnesses. For UNSAT, it records engine
+agreement without an independent UNSAT certificate. Timeout, UNKNOWN, errors,
+and incomplete traces are failures, never substitutes for UNSAT.
 
-Four strict case documents are versioned. Their classification is checked
-against the observed trace rather than trusted as prose.
+Continue with the [input format and output files](#new-cm1-in-3-input),
+[the six narrated checks](#suite-breve-commentata), or
+[the named v2 cases](#named-cases). The older
+[single-solver diagnostic cases](#example-index) remain available below.
 
-| Case | Configured result | Required observed shape | Case source |
-| --- | --- | --- | --- |
-| SAT end to end | SAT | complete trace, independently checked witness, square and checked hex views | [case JSON]({{ site.repository_url }}/blob/main/examples/run-cases/sat-end-to-end.json) |
-| Immediate root conflict | UNSAT | three events: root, initial conflict, result; no propagation or search | [case JSON]({{ site.repository_url }}/blob/main/examples/run-cases/unsat-root-conflict.json) |
-| Initial propagation contradiction | UNSAT | domain reductions and propagation reach an initial conflict before any decision | [case JSON]({{ site.repository_url }}/blob/main/examples/run-cases/unsat-propagation.json) |
-| Non-superficial search | UNSAT | complete depth-two run with four decisions, three conflicts, and four backtracks | [case JSON]({{ site.repository_url }}/blob/main/examples/run-cases/unsat-search.json) |
+## Suite breve commentata
 
-The first three cases use the same small formula so the observed boundary is
-easy to compare. The two constrained UNSAT cases deliberately exercise the
-public initial-domain option: their UNSAT status describes that configured
-Wang solve, not the unconstrained source formula. The search case uses a
-separate cubic monotone input whose unconstrained optimized run reaches depth
-two before exhausting all branches.
+Dopo `make demo-setup`, eseguire offline:
 
-This page is only an index. The [solver trace contract]({{ '/wang-solver-trace/' | relative_url }})
-remains the canonical explanation of event semantics, truncation, and replay.
-The [reference solver component]({{ '/components/reference-solver/' | relative_url }})
-owns the public reference animation. The [static snapshot contract]({{ '/wang-explainability-snapshots/' | relative_url }})
-defines formula and region views, while the [square-to-hex reference]({{ '/wang-square-to-hex/' | relative_url }})
-defines the presentation-only port. No animation, explanation, or generated
-run narrative is copied here.
+```sh
+make demo-check
+```
 
-## Reproduce one dossier
+La suite annuncia in italiano sei controlli, spiegando cosa verificano:
 
-Build the shared native library, provide pdfLaTeX, and run the sole generator:
+1. **Input valido:** il parser C legge le tre variabili e le tre clausole del
+   caso `tests/instances/pipeline_sat.cm13`.
+2. **Input fuori dominio:** il parser rifiuta una variabile non dichiarata;
+   un errore I/O non conta come il rifiuto atteso.
+3. **SAT noto:** il solver reference produce un tiling verificato e un
+   assegnamento booleano estratto, controllati anche dai checker indipendenti.
+4. **UNSAT noto:** `tests/instances/pipeline_unsat_search.cm13` contiene la
+   clausola `(x4,x4,x4)`, che richiede `3*x4=1`; il risultato non ha witness.
+5. **Accordo:** optimized, Boolean Z3 e Wang Z3 confermano entrambi gli esiti
+   noti; ogni motore gira una volta per caso e ogni witness SAT viene verificato.
+   I risultati reference dei punti precedenti vengono riusati.
+6. **Witness alterato:** una sola tessera viene sostituita con un'altra del
+   tileset, incompatibile con un colore di bordo. Il checker Python deve
+   rifiutare la copia e accettare ancora l'originale. Le coordinate stampate
+   partono da zero.
+
+Questi sono casi fissi con esito noto; `make demo INPUT=...`, descritto sotto,
+accetta invece un input nuovo senza presumere SAT o UNSAT. La suite breve non
+genera PDF, figure o trace e non sostituisce l'intera suite di test del progetto.
+Richiede solo l'ambiente Python principale e la libreria nativa già installati;
+non avvia build, installazioni o download.
+
+Ogni invocazione conserva `worker.log` in una directory distinta
+`build/demo-check/run-*`, stampata come `diagnostics=...`. Si ferma al primo
+fallimento. Solo dopo tutti i controlli compare `Superati 6/6 controlli`, con
+la durata effettiva: l'obiettivo indicativo di 30–60 secondi dopo il setup non
+è una soglia CI e non introduce attese artificiali. La durata del dossier si
+misura separatamente.
+
+Il timeout globale predefinito è 300 secondi; si può cambiarlo con
+`make demo-check TIMEOUT=60`. Per scegliere una directory di diagnostica nuova:
 
 ```sh
-make shared
-uv run --frozen python tools/generate_run_dossier.py \
-  examples/run-cases/sat-end-to-end.json \
-  build/run-dossiers/sat-end-to-end \
-  --tex-engine pdflatex
+python3 tools/demo_check.py --output build/my-check --timeout 60
 ```
 
-The destination must not exist. Every intermediate is written below a sibling
-staging directory, the trace bundle is validated before rendering, and the
-completed directory is installed with one rename. A failed render or TeX
-compile leaves no partial destination.
+Directory, file o link già presenti non vengono sovrascritti. Timeout,
+interruzione, UNKNOWN, discordanza, errori e output incompleti sono fallimenti,
+mai risultati UNSAT. La CLI restituisce 124 per timeout, 130/143 per
+SIGINT/SIGTERM, 1 per errori e 2 per argomenti invalidi; GNU Make restituisce
+il proprio esito nonzero quando la ricetta fallisce. Timeout e interruzioni
+fermano anche i processi figli. Il log resta disponibile; se un terminale
+lento perde messaggi, contiene comunque l'output completo del worker.
 
-The generator calls the isolated renderer through its locked environment. A
-single replay composes the selected frames used for individual PNGs, the
-contact sheet, and the optional GIF. The PDF embeds the already-produced
-contact sheet and static square/hex PNGs; it never embeds viewer-dependent GIF
-or video content. UNSAT reports contain region views rather than inventing a
-solution.
+## Full-pipeline v2 capture
 
-pdfLaTeX is invoked directly, never through a shell, with
-`-no-shell-escape`, restricted input/output policy, a private TeX home, UTC,
-and `SOURCE_DATE_EPOCH` derived from the recorded run time. The CI smoke
-installs TeX only inside its disposable runner. TeX is not a runtime or root
-Python dependency.
+### New CM1-in-3 input
 
-## Timing and evidence boundary
+Run `make demo-setup` once, then use the installed environments offline:
 
-The monotonic durations for parse, region build, solve, export, render, and SAT
-witness verification are raw evidence from one environment. They are excluded
-from snapshot identity and are not performance gates. The native solver has no
-Z3-style encoding stage, so `encoding` is explicitly recorded as not applicable
-rather than reported as a fabricated zero-duration operation. Verification is
-also explicitly not applicable to UNSAT runs because the trace is diagnostic,
-not an independently checked certificate.
+```sh
+make demo INPUT='path/to/new formula.cm13' TIMEOUT=300
+```
 
-Every example requires a complete trace. Selected frames remain a presentation
-subset of that trace. For UNSAT, `unsat_certificate` is always false: conflicts
-and trail history diagnose what the run observed but do not constitute a
-standalone mathematical proof of unsatisfiability.
+The input needs a `p cm13 n n` header, followed by `n` clauses. Each clause has
+three positive variable indices in `1..n` and ends in `0`. Every variable must
+occur exactly three times across all clauses, counting repeated occurrences
+within one clause. Lines beginning with `c` are comments. For example:
 
-## Full-pipeline v2 capture
+```text
+c Three variables, each with three occurrences
+p cm13 3 3
+1 1 2 0
+1 2 3 0
+2 3 3 0
+```
+
+No expected result is supplied. The demo copies the original bytes before
+parsing, reduces once, and runs reference, optimized, Boolean Z3 and Wang Z3
+once each. The dossier and PDF consume that same validated capture. Named
+cases below use the same capture producer and retain their configured metadata.
+
+Each invocation creates a separate `build/demo/run-*` directory containing
+`input.cm13`, diagnostic `input.json` (original path/name and SHA-256),
+`worker.log`, and the completed `dossier/` with `run.json`, source/trace assets,
+figures, `report.tex` and `report.pdf`. Input names with spaces or shell/Make
+metacharacters are passed literally; quote the command argument as above.
+The portable name inside a new dossier is always `input.cm13`.
+
+The command prints real operations as they start. `worker.log` keeps the full
+worker output even if a slow terminal or pipe cannot display every message.
+`TIMEOUT` defaults to 300
+seconds and must be finite and positive. It covers the worker's preflight,
+input copy, native/Z3 capture, checks, figures and LaTeX. Timeout or Ctrl-C stops
+the worker and its child processes; SIGTERM is also handled. The log and copied
+input survive failures, while any staging artifacts remain diagnostic only.
+The command prints `dossier=` and `pdf=` only after successful completion.
+
+For explicit output and trace capacity, use the same supervised Python entry:
+
+```sh
+python3 tools/demo.py 'path/to/new formula.cm13' \
+  --output build/my-demo --timeout 300 --event-capacity 100000
+```
+
+The output directory must be new, including when a symlink already occupies
+that path. Trace capacity is an integer from 2 to 100000 per native solver;
+the default is 100000 and checkpoints are disabled. Exhaustion fails without
+rerunning either solver. Missing dependencies require `make demo-setup`; the
+demo never builds, installs or downloads them itself.
+
+Malformed input, missing dependencies, UNKNOWN, engine disagreement, incomplete
+trace and failed checks produce distinct diagnostic messages. Timeout exits
+with 124; handled SIGINT/SIGTERM exits with 130/143. These are process outcomes,
+not UNSAT results. GNU Make reports a failed recipe with its own nonzero exit.
+UNSAT succeeds only when all four engines agree on that terminal result, and
+still carries no independent UNSAT certificate. Arbitrary inputs may exceed the
+time or trace limits; neither option promises completion.
+
+Wide regions appear as overview figures in the PDF. Use the PDF viewer's zoom
+or the full-resolution PNG frames under `dossier/assets/narrative/` to inspect
+individual cells and trace labels; a whole-page view cannot show every detail.
+
+### Named cases
 
 `wang-run-case-v2` deliberately has no initial-domain override field. Its
 canonical case follows `tests/instances/pipeline_sat.cm13` through the four
@@ -130,6 +189,29 @@ SAT/UNSAT status plus independently valid SAT witnesses; different valid
 witnesses are not required to be byte-equal. UNKNOWN, mismatch, a truncated
 trace, or a failed checker aborts the capture before installation.
 
+### Result expectation and recorded outcome
+
+The v2 case and run contracts keep `expected_status` required and accept
+`"sat"`, `"unsat"`, or `null`. A null value means no expected result was supplied;
+it is never filled from a solver result and does not mean UNKNOWN. All four
+named engines must first report the same terminal result. A supplied expectation
+is then checked as an additional assertion. Witness checks, presentation
+applicability, and PDF status follow the observed agreement. For an absent
+expectation the PDF says so explicitly.
+
+The standalone narrative manifest adds `case.observed_status` exactly when
+`case.expected_status` is null. Known cases retain the existing three-field case
+shape. Verification receipts preserve the nullable expectation and use their
+four recorded agreement statuses; they need no extra status field. Bundle
+loading also binds each native source identity and trace status/completeness,
+and each Z3 summary status, to its run record.
+
+Updated readers continue to accept earlier v2 dossiers, and known-case output
+and canonical asset identities stay unchanged. Earlier strict readers reject
+the new nullable variant. V1 retains its existing contracts. This is an
+extension of the existing v2 and narrative contracts, with no new pipeline or
+independent UNSAT certificate.
+
 The downstream shared-asset pass then consumes only that validated capture.
 Its closed `wang-narrative-assets-v1` manifest names fixed component assets,
 not generic stages: Boolean and Wang Z3 encoding order, canonical region
@@ -178,3 +260,84 @@ All v2 durations use one monotonic nanosecond clock and are labelled
 `run-specific-observation-not-a-benchmark`. They are raw facts about that
 capture, never a performance comparison. SAT-only checker timings are null for
 UNSAT rather than fabricated as zero.
+
+## Example index
+
+The v1 reports describe one configured native run. Each completed directory
+contains `run.json`, `report.tex`, `report.pdf`, and `assets/`. The four cases
+below retain their existing schemas, initial-domain behavior, and output shape.
+
+`run.json` records the source and Git identity, environment, solver options and
+result, complete trace counters, initial-domain overrides, raw stage durations,
+replay scope, and SHA-256 for each referenced JSON or raster asset. The PDF uses
+that recorded data; it does not recalculate events, witness state, timing, or
+provenance.
+
+Four strict case documents are versioned. Their classification is checked
+against the observed trace rather than trusted as prose.
+
+| Case | Configured result | Required observed shape | Case source |
+| --- | --- | --- | --- |
+| SAT end to end | SAT | complete trace, independently checked witness, square and checked hex views | [case JSON]({{ site.repository_url }}/blob/main/examples/run-cases/sat-end-to-end.json) |
+| Immediate root conflict | UNSAT | three events: root, initial conflict, result; no propagation or search | [case JSON]({{ site.repository_url }}/blob/main/examples/run-cases/unsat-root-conflict.json) |
+| Initial propagation contradiction | UNSAT | domain reductions and propagation reach an initial conflict before any decision | [case JSON]({{ site.repository_url }}/blob/main/examples/run-cases/unsat-propagation.json) |
+| Non-superficial search | UNSAT | complete depth-two run with four decisions, three conflicts, and four backtracks | [case JSON]({{ site.repository_url }}/blob/main/examples/run-cases/unsat-search.json) |
+
+The first three cases use the same small formula so the observed boundary is
+easy to compare. The two constrained UNSAT cases deliberately exercise the
+public initial-domain option: their UNSAT status describes that configured
+Wang solve, not the unconstrained source formula. The search case uses a
+separate cubic monotone input whose unconstrained optimized run reaches depth
+two before exhausting all branches.
+
+The [solver trace contract]({{ '/wang-solver-trace/' | relative_url }})
+remains the canonical explanation of event semantics, truncation, and replay.
+The [reference solver component]({{ '/components/reference-solver/' | relative_url }})
+owns the public reference animation. The [static snapshot contract]({{ '/wang-explainability-snapshots/' | relative_url }})
+defines formula and region views, while the [square-to-hex reference]({{ '/wang-square-to-hex/' | relative_url }})
+defines the presentation-only port.
+
+## Reproduce one dossier
+
+Build the shared native library, provide pdfLaTeX, and run the sole generator:
+
+```sh
+make shared
+uv run --frozen python tools/generate_run_dossier.py \
+  examples/run-cases/sat-end-to-end.json \
+  build/run-dossiers/sat-end-to-end \
+  --tex-engine pdflatex
+```
+
+The destination must not exist. Every intermediate is written below a sibling
+staging directory, the trace bundle is validated before rendering, and the
+completed directory is installed with one rename. A failed render or TeX
+compile leaves no partial destination.
+
+The generator calls the isolated renderer through its locked environment. A
+single replay composes the selected frames used for individual PNGs, the
+contact sheet, and the optional GIF. The PDF embeds the already-produced
+contact sheet and static square/hex PNGs; it never embeds viewer-dependent GIF
+or video content. UNSAT reports contain region views rather than inventing a
+solution.
+
+pdfLaTeX is invoked directly, never through a shell, with
+`-no-shell-escape`, restricted input/output policy, a private TeX home, UTC,
+and `SOURCE_DATE_EPOCH` derived from the recorded run time. The CI smoke
+installs TeX only inside its disposable runner. TeX is not a runtime or root
+Python dependency.
+
+## Timing and evidence boundary
+
+The monotonic durations for parse, region build, solve, export, render, and SAT
+witness verification are raw evidence from one environment. They are excluded
+from snapshot identity and are not performance gates. The native solver has no
+Z3-style encoding stage, so `encoding` is explicitly recorded as not applicable
+rather than reported as a fabricated zero-duration operation. Verification is
+also explicitly not applicable to UNSAT runs because the trace is diagnostic,
+not an independently checked certificate.
+
+Every example requires a complete trace. Selected frames remain a presentation
+subset of that trace. For UNSAT, `unsat_certificate` is always false: conflicts
+and trail history diagnose what the run observed but do not constitute a
+standalone mathematical proof of unsatisfiability.
diff --git a/docs/worked-example.md b/docs/worked-example.md
index 70c367e..7c90869 100644
--- a/docs/worked-example.md
+++ b/docs/worked-example.md
@@ -9,8 +9,11 @@ description: One named pipeline_sat.cm13 instance followed from source bytes to
 
 # Worked SAT example
 
-This page follows one small three-variable CM1-in-3 SAT instance through the
-complete pipeline, from source formula to independently checked presentations.
+The input `pipeline_sat.cm13` has three variables and three clauses. All four
+engines report SAT, and the returned witnesses pass their independent checks.
+This page follows that one run from formula to square tiling and hex view.
+The [named-case command]({{ '/run-dossiers/#named-cases' | relative_url }})
+reproduces the same input through the pipeline.
 
 <details markdown="1">
 <summary>Technical provenance</summary>
@@ -32,9 +35,13 @@ view at a useful reading size; the component pages own their full explanations.
 
 ## Source formula
 
-The parser reads a canonical Cubic Monotone 1-in-3 SAT document with three
-variables and three source-order clauses. The snapshot below is bound to those
-source bytes; it is not reconstructed from a later tiling.
+Each clause requires exactly one true occurrence. The clauses are
+`(x1,x1,x2)`, `(x1,x2,x3)`, and `(x2,x3,x3)`. The assignment
+**x1 = 0, x2 = 1, x3 = 0** satisfies all three: each contains one true `x2`.
+The repeated occurrences count separately.
+
+The parser's snapshot below preserves the source clause order and is bound to
+the original file's bytes. It is not reconstructed from a later tiling.
 
 {% include narrative-static.html asset_id="formula" image="/assets/narrative/formula.png" alt="The parsed CM1-in-3 formula and its source-order clauses." width="796" height="394" label="observed" caption="Parsed formula snapshot for the named canonical source." source="cm13-formula-snapshot-v1" %}
 
@@ -55,7 +62,7 @@ native extraction. Only after those checks does the presentation layer render
 the enlarged square witness, recognize exact generalized contours, and apply
 the checked square-to-hex mapping shown in the final panel.
 
-The milestone sequence links to the owned explanations for the
+For the mechanism behind each step, read the component pages for the
 [tileset]({{ '/components/tileset/' | relative_url }}),
 [Boolean Z3]({{ '/components/boolean-z3/' | relative_url }}),
 [Yang–Zhang reduction]({{ '/components/yang-zhang/' | relative_url }}),
diff --git a/pyproject.toml b/pyproject.toml
index 2575439..8d00fec 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -1,6 +1,6 @@
 [project]
 name = "tiling-foundry"
-version = "0.1.0"
+version = "1.0.0"
 description = "Verified research tools for the Yang–Zhang 23-Wang-tile reduction"
 requires-python = ">=3.11"
 dependencies = [
diff --git a/python/dossier/multi_engine.py b/python/dossier/multi_engine.py
index a529460..68991df 100644
--- a/python/dossier/multi_engine.py
+++ b/python/dossier/multi_engine.py
@@ -11,6 +11,7 @@
 import subprocess
 import tempfile
 from time import perf_counter_ns
+from typing import Callable
 
 from formats.pipeline_snapshot import _encode_document, _write_atomic
 from formats.run_case_v2 import (
@@ -273,11 +274,53 @@ def generate_multi_engine_dossier(
     output_directory: str | Path,
     *,
     include_pdf: bool = False,
+    progress: Callable[[str], None] | None = None,
 ) -> Path:
     """Capture all named engines once and atomically install the complete v2 dossier."""
     case: MultiEngineRunCase = load_run_case_v2(case_path, ROOT)
-    destination = Path(output_directory).resolve()
-    if destination.exists():
+    return _generate_dossier(
+        case, ROOT / case.source, output_directory,
+        include_pdf=include_pdf, progress=progress,
+    )
+
+
+def generate_input_dossier(
+    input_path: str | Path,
+    output_directory: str | Path,
+    *,
+    include_pdf: bool = True,
+    event_capacity: int = 100_000,
+    progress: Callable[[str], None] | None = None,
+) -> Path:
+    """Capture a new CM1-in-3 file without supplying an expected result."""
+    if type(event_capacity) is not int or not 2 <= event_capacity <= 100_000:
+        raise ValueError("event_capacity must be an integer in [2, 100000]")
+    trace = TraceConfiguration(event_capacity, 0, 0)
+    case = MultiEngineRunCase(
+        identifier="demo-input",
+        title="CM1-in-3 input dossier",
+        purpose="Observe and independently check four engines on the copied input.",
+        source="input.cm13",
+        expected_status=None,
+        reference_trace=trace,
+        optimized_trace=trace,
+    )
+    return _generate_dossier(
+        case, Path(input_path), output_directory,
+        include_pdf=include_pdf, progress=progress,
+    )
+
+
+def _generate_dossier(
+    case: MultiEngineRunCase,
+    source_path: Path,
+    output_directory: str | Path,
+    *,
+    include_pdf: bool,
+    progress: Callable[[str], None] | None,
+) -> Path:
+    destination = Path(output_directory).absolute()
+    if os.path.lexists(destination):
         raise MultiEngineDossierError(
             f"output directory already exists: {destination!s}"
         )
@@ -286,28 +329,34 @@ def generate_multi_engine_dossier(
         tempfile.mkdtemp(prefix=f".{destination.name}.", dir=destination.parent)
     )
     try:
-        source_path = ROOT / case.source
+        data = staging / "assets/data"
+        data.mkdir(parents=True)
+        source_copy = data / Path(case.source).name
         source_bytes = source_path.read_bytes()
+        started = perf_counter_ns()
+        _write_atomic(source_copy, source_bytes)
+        export_ns = perf_counter_ns() - started
         source_sha256 = hashlib.sha256(source_bytes).hexdigest()
         capture = capture_multi_engine_native_pipeline(
-            source_path,
+            source_copy,
             reference_options=_native_options(case.reference_trace),
             optimized_options=_native_options(case.optimized_trace),
+            progress=progress,
         )
+        if capture.reference.trace.truncated or capture.optimized.trace.truncated:
+            raise MultiEngineDossierError(
+                "full-pipeline dossier requires complete traces; event capacity exhausted"
+            )
 
-        data = staging / "assets/data"
-        data.mkdir(parents=True)
-        source_copy = data / source_path.name
         reference_manifest_path = data / "reference-manifest.json"
         optimized_manifest_path = data / "optimized-manifest.json"
         boolean_summary_path = data / "boolean-z3.json"
         wang_summary_path = data / "wang-z3.json"
 
         started = perf_counter_ns()
-        _write_atomic(source_copy, source_bytes)
         dump_solver_trace_bundle(
             reference_manifest_path,
-            source_path,
+            source_copy,
             capture.formula,
             capture.region,
             capture.explanation,
@@ -316,7 +365,7 @@ def generate_multi_engine_dossier(
         )
         dump_solver_trace_bundle(
             optimized_manifest_path,
-            source_path,
+            source_copy,
             capture.formula,
             capture.region,
             capture.explanation,
@@ -325,11 +374,13 @@ def generate_multi_engine_dossier(
         )
         reference_manifest, _ = load_solver_trace_bundle(reference_manifest_path)
         optimized_manifest, _ = load_solver_trace_bundle(optimized_manifest_path)
-        export_ns = perf_counter_ns() - started
+        export_ns += perf_counter_ns() - started
         region_reference = reference_manifest["artifacts"]["region"]
         assert isinstance(region_reference, dict)
         region_sha256 = str(region_reference["sha256"])
 
+        if progress is not None:
+            progress("Boolean Z3")
         started = perf_counter_ns()
         boolean_summary = build_boolean_z3_summary(
             capture.formula,
@@ -338,6 +389,8 @@ def generate_multi_engine_dossier(
         boolean_z3_ns = perf_counter_ns() - started
         boolean_assignment = boolean_summary["model"]["assignment"]
         if boolean_summary["status"] == "sat":
+            if progress is not None:
+                progress("Boolean Z3 verification")
             started = perf_counter_ns()
             if not isinstance(boolean_assignment, list) or not is_valid_assignment(
                 capture.formula, boolean_assignment
@@ -349,6 +402,8 @@ def generate_multi_engine_dossier(
         else:
             boolean_z3_verify_ns = None
 
+        if progress is not None:
+            progress("Wang Z3")
         started = perf_counter_ns()
         wang_summary = build_wang_z3_summary(
             capture.formula,
@@ -359,6 +414,8 @@ def generate_multi_engine_dossier(
         wang_z3_ns = perf_counter_ns() - started
         wang_cells = wang_summary["model"]["cells"]
         if wang_summary["status"] == "sat":
+            if progress is not None:
+                progress("Wang Z3 verification")
             started = perf_counter_ns()
             if not isinstance(wang_cells, list) or not is_valid_tiling(
                 capture.region, TILESET, wang_cells
@@ -400,6 +457,8 @@ def generate_multi_engine_dossier(
             "wang_z3_verify_ns": wang_z3_verify_ns,
             "export_ns": export_ns,
         }
+        if progress is not None:
+            progress("Bundle verification")
         run_document = build_run_dossier_v2(
             case,
             capture,
@@ -423,6 +482,8 @@ def generate_multi_engine_dossier(
         )
 
         try:
+            if progress is not None:
+                progress("Figures")
             narrative_manifest = generate_narrative_assets(
                 run_path,
                 staging / "assets/narrative",
@@ -440,6 +501,8 @@ def generate_multi_engine_dossier(
         _write_atomic(run_path, _encode_document(run_document))
         validated_document = load_run_dossier_v2(run_path)
         if include_pdf:
+            if progress is not None:
+                progress("PDF")
             from dossier.tex_compile import TexCompileError, compile_tex_pdf
             from formats.narrative_assets import load_narrative_assets
             from formats.run_report_v2_tex import render_run_report_v2_tex
@@ -458,6 +521,9 @@ def generate_multi_engine_dossier(
                 compile_tex_pdf(staging, "pdflatex", captured_at)
             except TexCompileError as error:
                 raise MultiEngineDossierError(str(error)) from error
+        if progress is not None:
+            progress("Final validation")
+        load_run_dossier_v2(run_path)
         _install_directory(staging, destination)
         return destination
     except Exception:
diff --git a/python/dossier/narrative_assets.py b/python/dossier/narrative_assets.py
index 74a5799..64d7563 100644
--- a/python/dossier/narrative_assets.py
+++ b/python/dossier/narrative_assets.py
@@ -196,7 +196,7 @@ def _animation_metadata(
     run: dict[str, object],
 ) -> dict[str, dict[str, str]]:
     pipeline_digest = pipeline_source_sha256(identities, run)
-    search_diagnostic = run["case"]["expected_status"] == "unsat"
+    search_diagnostic = run["reference"]["status"] == "unsat"
     reference_trace_caption = (
         "Selected semantic milestones from the complete observed search "
         "diagnostic; it is not an UNSAT certificate."
@@ -512,7 +512,7 @@ def attach_narrative_assets(
             "selected_event_count": selected,
         }
 
-    if updated["case"]["expected_status"] == "sat":
+    if updated["reference"]["status"] == "sat":
         specifications = {
             "square": (
                 "observed verified square witness presentation",
@@ -649,7 +649,7 @@ def generate_narrative_assets(
             "--manifest",
             str(reference_manifest),
         ]
-        if run["case"]["expected_status"] == "sat":
+        if run["reference"]["status"] == "sat":
             reference_solution = _run_artifact(
                 run_root, run, "reference_solution"
             )
@@ -693,7 +693,7 @@ def generate_narrative_assets(
                 "renderer generalized specification disagrees with the narrative contract"
             )
 
-        status = run["case"]["expected_status"]
+        status = run["reference"]["status"]
         witness_outputs: dict[str, Path] | None = None
         if status == "sat":
             solution = _run_artifact(run_root, run, "reference_solution")
@@ -798,7 +798,11 @@ def generate_narrative_assets(
             "product": product,
             "case": {
                 "id": run["case"]["id"],
-                "expected_status": status,
+                "expected_status": run["case"]["expected_status"],
+                **(
+                    {"observed_status": status}
+                    if run["case"]["expected_status"] is None else {}
+                ),
                 "source_sha256": run["source"]["sha256"],
             },
             "identities": identities,
diff --git a/python/formats/narrative_assets.py b/python/formats/narrative_assets.py
index 376599b..b1c5d44 100644
--- a/python/formats/narrative_assets.py
+++ b/python/formats/narrative_assets.py
@@ -413,13 +413,17 @@ def validate_narrative_assets(
     if product not in PRODUCTS:
         raise PipelineSnapshotError("$.product: is unsupported")
     case = _require_object(manifest["case"], "$.case")
-    _require_exact_fields(
-        case, frozenset({"id", "expected_status", "source_sha256"}), "$.case"
-    )
+    case_fields = {"id", "expected_status", "source_sha256"}
+    if case.get("expected_status") is None:
+        case_fields.add("observed_status")
+    _require_exact_fields(case, frozenset(case_fields), "$.case")
     _nonempty_string(case["id"], "$.case.id")
-    status = _nonempty_string(case["expected_status"], "$.case.expected_status")
+    status_field = (
+        "observed_status" if case["expected_status"] is None else "expected_status"
+    )
+    status = _nonempty_string(case[status_field], f"$.case.{status_field}")
     if status not in {"sat", "unsat"}:
-        raise PipelineSnapshotError("$.case.expected_status: is unsupported")
+        raise PipelineSnapshotError(f"$.case.{status_field}: is unsupported")
     _require_sha256(case["source_sha256"], "$.case.source_sha256")
     if product == "canonical-pages" and case != CANONICAL_PAGES_CASE:
         raise PipelineSnapshotError(
@@ -578,11 +582,15 @@ def load_narrative_assets(
     except OSError as error:
         raise PipelineSnapshotError(f"cannot read narrative manifest: {error}") from error
     validate_narrative_assets(document, path)
-    if document["case"] != {
+    observed_status = run_document["reference"]["status"]
+    expected_case = {
         "id": run_document["case"]["id"],
         "expected_status": run_document["case"]["expected_status"],
         "source_sha256": run_document["source"]["sha256"],
-    }:
+    }
+    if expected_case["expected_status"] is None:
+        expected_case["observed_status"] = observed_status
+    if document["case"] != expected_case:
         raise PipelineSnapshotError("narrative case identity disagrees with run")
     expected_identities = {
         "source_formula": run_document["source"]["sha256"],
@@ -647,7 +655,7 @@ def load_narrative_assets(
             OPTIMIZED_MECHANISMS_SHA256,
         ),
     }
-    if run_document["case"]["expected_status"] == "sat":
+    if observed_status == "sat":
         expected_sources["witness_presentation"] = (
             "wang-solution-v1+wang-generalized-tiles-v1+checked-square-to-hex",
             witness_presentation_source_sha256(
@@ -674,7 +682,7 @@ def load_narrative_assets(
             generalized_digest,
         ),
     }
-    if run_document["case"]["expected_status"] == "sat":
+    if observed_status == "sat":
         assert solution_digest is not None
         expected_static_sources.update(
             {
@@ -707,7 +715,7 @@ def load_narrative_assets(
             )
     if (
         document["product"] == "run-specific"
-        and run_document["case"]["expected_status"] == "sat"
+        and observed_status == "sat"
     ):
         for name in ("square", "generalized", "hex"):
             narrative_artifact = document["statics"][f"{name}_presentation"][
diff --git a/python/formats/run_case_v2.py b/python/formats/run_case_v2.py
index 47003c1..4b79428 100644
--- a/python/formats/run_case_v2.py
+++ b/python/formats/run_case_v2.py
@@ -39,7 +39,7 @@ class MultiEngineRunCase:
     title: str
     purpose: str
     source: str
-    expected_status: str
+    expected_status: str | None
     reference_trace: TraceConfiguration
     optimized_trace: TraceConfiguration
 
@@ -118,11 +118,11 @@ def load_run_case_v2(
         raise PipelineSnapshotError(
             f"$.source: repository input does not exist: {source}"
         )
-    expected_status = _nonempty_string(
-        document["expected_status"], "$.expected_status"
-    )
-    if expected_status not in _STATUSES:
-        raise PipelineSnapshotError("$.expected_status: must equal sat or unsat")
+    expected_status = document["expected_status"]
+    if expected_status is not None:
+        expected_status = _nonempty_string(expected_status, "$.expected_status")
+        if expected_status not in _STATUSES:
+            raise PipelineSnapshotError("$.expected_status: must equal sat, unsat or null")
     return MultiEngineRunCase(
         identifier=identifier,
         title=title,
diff --git a/python/formats/run_dossier_v2.py b/python/formats/run_dossier_v2.py
index 26ede0e..52602d4 100644
--- a/python/formats/run_dossier_v2.py
+++ b/python/formats/run_dossier_v2.py
@@ -355,11 +355,13 @@ def validate_run_dossier_v2(document: object) -> None:
         raise PipelineSnapshotError("$.case.id: is invalid")
     _nonempty_string(case["title"], "$.case.title")
     _nonempty_string(case["purpose"], "$.case.purpose")
-    expected_status = _nonempty_string(
-        case["expected_status"], "$.case.expected_status"
-    )
-    if expected_status not in STATUSES:
-        raise PipelineSnapshotError("$.case.expected_status: must equal sat or unsat")
+    expected_status = case["expected_status"]
+    if expected_status is not None:
+        expected_status = _nonempty_string(expected_status, "$.case.expected_status")
+        if expected_status not in STATUSES:
+            raise PipelineSnapshotError(
+                "$.case.expected_status: must equal sat, unsat or null"
+            )
 
     source = _require_object(root["source"], "$.source")
     _require_exact_fields(source, frozenset({"path", "sha256"}), "$.source")
@@ -392,8 +394,11 @@ def validate_run_dossier_v2(document: object) -> None:
         "optimized": _validate_native_record(root["optimized"], "$.optimized", "optimized"),
         "wang_z3": _validate_z3_record(root["wang_z3"], "$.wang_z3", wang=True),
     }
-    if any(status != expected_status for status in statuses.values()):
+    observed_status = statuses["reference"]
+    if any(status != observed_status for status in statuses.values()):
         raise PipelineSnapshotError("engine status mismatch")
+    if expected_status is not None and expected_status != observed_status:
+        raise PipelineSnapshotError("known expected status mismatch")
 
     reduction = _require_object(root["reduction"], "$.reduction")
     _require_exact_fields(
@@ -425,9 +430,9 @@ def validate_run_dossier_v2(document: object) -> None:
         _validate_check(
             verification[name],
             f"$.verification.{name}",
-            performed=expected_status == "sat",
+            performed=observed_status == "sat",
         )
-    if expected_status == "sat":
+    if observed_status == "sat":
         expected_check_digests = {
             "boolean_z3_assignment": root["boolean_z3"]["witness_sha256"],
             "reference_tiling": root["reference"]["witness_sha256"],
@@ -463,18 +468,16 @@ def validate_run_dossier_v2(document: object) -> None:
         ),
         "$.agreement",
     )
-    for name in (
-        "expected_status",
-        "boolean_z3_status",
-        "reference_status",
-        "optimized_status",
-        "wang_z3_status",
-    ):
-        if agreement[name] != expected_status:
-            raise PipelineSnapshotError(f"$.agreement.{name}: disagrees with case")
+    if agreement["expected_status"] != expected_status:
+        raise PipelineSnapshotError("$.agreement.expected_status: disagrees with case")
+    for engine, status in statuses.items():
+        if agreement[f"{engine}_status"] != status:
+            raise PipelineSnapshotError(
+                f"$.agreement.{engine}_status: disagrees with engine"
+            )
     if agreement["all_status_equal"] is not True or agreement["passed"] is not True:
         raise PipelineSnapshotError("$.agreement: engine disagreement is a failure")
-    expected_witness_validity = True if expected_status == "sat" else None
+    expected_witness_validity = True if observed_status == "sat" else None
     if agreement["sat_witnesses_valid"] is not expected_witness_validity:
         raise PipelineSnapshotError("$.agreement.sat_witnesses_valid: is inconsistent")
 
@@ -495,7 +498,7 @@ def validate_run_dossier_v2(document: object) -> None:
             item["relationship"], relationship, f"$.presentation.{name}.relationship"
         )
         if _boolean(item["applicable"], f"$.presentation.{name}.applicable") is not (
-            expected_status == "sat"
+            observed_status == "sat"
         ):
             raise PipelineSnapshotError(f"$.presentation.{name}.applicable: disagrees")
         expected_artifact = f"{name}_presentation"
@@ -518,7 +521,7 @@ def validate_run_dossier_v2(document: object) -> None:
     for name in _TIMING_FIELDS - {"clock", "identity"}:
         elapsed = _nullable_nonnegative(timings[name], f"$.timings.{name}")
         if name in nullable:
-            if (elapsed is None) != (expected_status == "unsat"):
+            if (elapsed is None) != (observed_status == "unsat"):
                 raise PipelineSnapshotError(
                     f"$.timings.{name}: applicability disagrees"
                 )
@@ -534,10 +537,10 @@ def validate_run_dossier_v2(document: object) -> None:
         if raw is None:
             if not may_be_null:
                 raise PipelineSnapshotError(f"$.artifacts.{name}: is required")
-            if name.endswith("_solution") and expected_status == "sat":
+            if name.endswith("_solution") and observed_status == "sat":
                 raise PipelineSnapshotError(f"$.artifacts.{name}: SAT requires a solution")
             continue
-        if name.endswith("_solution") and expected_status == "unsat":
+        if name.endswith("_solution") and observed_status == "unsat":
             raise PipelineSnapshotError(f"$.artifacts.{name}: UNSAT forbids a solution")
         item = _require_object(raw, f"$.artifacts.{name}")
         _require_exact_fields(item, _ARTIFACT_FIELDS, f"$.artifacts.{name}")
@@ -598,7 +601,7 @@ def validate_run_dossier_v2(document: object) -> None:
         )
     for solver in ("reference", "optimized"):
         solution = artifacts[f"{solver}_solution"]
-        if expected_status == "sat" and solution["sha256"] != root[solver]["solution_sha256"]:
+        if observed_status == "sat" and solution["sha256"] != root[solver]["solution_sha256"]:
             raise PipelineSnapshotError(
                 f"$.artifacts.{solver}_solution.sha256: cross-field mismatch"
             )
diff --git a/python/formats/run_dossier_v2_builder.py b/python/formats/run_dossier_v2_builder.py
index d252f8d..805f153 100644
--- a/python/formats/run_dossier_v2_builder.py
+++ b/python/formats/run_dossier_v2_builder.py
@@ -102,8 +102,11 @@ def build_run_dossier_v2(
     }
     if any(status not in STATUSES for status in statuses.values()):
         raise PipelineSnapshotError("full-pipeline dossier forbids UNKNOWN results")
-    if any(status != case.expected_status for status in statuses.values()):
+    observed_status = statuses["reference"]
+    if any(status != observed_status for status in statuses.values()):
         raise PipelineSnapshotError("engine status mismatch")
+    if case.expected_status is not None and case.expected_status != observed_status:
+        raise PipelineSnapshotError("known expected status mismatch")
     if capture.reference.trace.truncated or capture.optimized.trace.truncated:
         raise PipelineSnapshotError("full-pipeline dossier requires complete traces")
 
@@ -114,7 +117,7 @@ def build_run_dossier_v2(
     wang_cells = _validate_cells(
         wang_summary["model"]["cells"], "wang_summary.model.cells"
     )
-    if case.expected_status == "sat":
+    if observed_status == "sat":
         if boolean_assignment is None or not is_valid_assignment(
             capture.formula, boolean_assignment
         ):
@@ -144,7 +147,7 @@ def build_run_dossier_v2(
         artifacts["optimized_trace_manifest"]["sha256"],
         artifacts["optimized_trace"]["sha256"],
     )
-    if case.expected_status == "sat":
+    if observed_status == "sat":
         reference["solution_sha256"] = artifacts["reference_solution"]["sha256"]
         optimized["solution_sha256"] = artifacts["optimized_solution"]["sha256"]
 
@@ -221,24 +224,24 @@ def build_run_dossier_v2(
             "wang_z3_status": statuses["wang_z3"],
             "all_status_equal": True,
             "sat_witnesses_valid": (
-                True if case.expected_status == "sat" else None
+                True if observed_status == "sat" else None
             ),
             "passed": True,
         },
         "presentation": {
             "square": {
                 "relationship": "verified-wang-solution",
-                "applicable": case.expected_status == "sat",
+                "applicable": observed_status == "sat",
                 "artifact": None,
             },
             "generalized": {
                 "relationship": "exact-14-to-23-presentation",
-                "applicable": case.expected_status == "sat",
+                "applicable": observed_status == "sat",
                 "artifact": None,
             },
             "hex": {
                 "relationship": "checked-square-to-hex-transformation",
-                "applicable": case.expected_status == "sat",
+                "applicable": observed_status == "sat",
                 "artifact": None,
             },
         },
diff --git a/python/formats/run_dossier_v2_bundle.py b/python/formats/run_dossier_v2_bundle.py
index 0639683..f60c291 100644
--- a/python/formats/run_dossier_v2_bundle.py
+++ b/python/formats/run_dossier_v2_bundle.py
@@ -59,6 +59,7 @@ def load_run_dossier_v2(path: str | Path) -> dict[str, object]:
             f"cannot read v2 dossier {run_path!s}: {error}"
         ) from error
     validate_run_dossier_v2(document)
+    observed_status = document["reference"]["status"]
     artifacts = document["artifacts"]
     assert isinstance(artifacts, dict)
     try:
@@ -125,15 +126,28 @@ def load_run_dossier_v2(path: str | Path) -> dict[str, object]:
             raise PipelineSnapshotError(
                 f"native manifest {manifest_name} identity disagrees with run"
             )
-    for solver, manifest in (
-        ("reference", reference_manifest),
-        ("optimized", optimized_manifest),
+    for solver, manifest, bundle in (
+        ("reference", reference_manifest, reference_documents),
+        ("optimized", optimized_manifest, optimized_documents),
     ):
+        if manifest["source_formula_sha256"] != document["source"]["sha256"]:
+            raise PipelineSnapshotError(f"{solver} native source identity disagrees with run")
+        trace = bundle["trace"]
+        if trace["status"] != document[solver]["status"]:
+            raise PipelineSnapshotError(f"{solver} trace status disagrees with run")
+        if trace["solver"] != solver:
+            raise PipelineSnapshotError(f"{solver} trace solver disagrees with run")
+        truncated = trace["capacity"]["truncated"]
+        if (
+            truncated != document[solver]["trace"]["truncated"]
+            or (not truncated) != document[solver]["trace"]["complete"]
+        ):
+            raise PipelineSnapshotError(f"{solver} trace completeness disagrees with run")
         trace_digest = manifest["artifacts"]["trace"]["sha256"]
         if trace_digest != document[solver]["trace"]["trace_sha256"]:
             raise PipelineSnapshotError(f"{solver} manifest trace identity mismatch")
         solution_reference = manifest["artifacts"]["solution"]
-        if document["case"]["expected_status"] == "sat":
+        if observed_status == "sat":
             if solution_reference["sha256"] != document[solver]["solution_sha256"]:
                 raise PipelineSnapshotError(
                     f"{solver} manifest solution identity mismatch"
@@ -158,6 +172,9 @@ def load_run_dossier_v2(path: str | Path) -> dict[str, object]:
     wang_summary = documents["wang_z3_summary"]
     validate_z3_encoding_summary(boolean_summary)
     validate_z3_encoding_summary(wang_summary)
+    for engine, summary in (("boolean_z3", boolean_summary), ("wang_z3", wang_summary)):
+        if summary["status"] != document[engine]["status"]:
+            raise PipelineSnapshotError(f"{engine} summary status disagrees with run")
     source_sha256 = document["source"]["sha256"]
     region_sha256 = document["reduction"]["region_sha256"]
     if boolean_summary["source_formula_sha256"] != source_sha256:
@@ -170,7 +187,7 @@ def load_run_dossier_v2(path: str | Path) -> dict[str, object]:
 
     formula = _formula_from_snapshot(reference_documents["formula"])
     region = _region_from_snapshot(reference_documents["region"])
-    if document["case"]["expected_status"] == "sat":
+    if observed_status == "sat":
         boolean_assignment = tuple(boolean_summary["model"]["assignment"])
         wang_cells = tuple(wang_summary["model"]["cells"])
         if not is_valid_assignment(formula, boolean_assignment):
@@ -250,7 +267,7 @@ def load_run_dossier_v2(path: str | Path) -> dict[str, object]:
                 raise PipelineSnapshotError(
                     f"{solver} selected event count disagrees with narrative manifest"
                 )
-        if document["case"]["expected_status"] == "sat" and any(
+        if observed_status == "sat" and any(
             document["artifacts"][f"{name}_presentation"] is None
             for name in ("square", "generalized", "hex")
         ):
diff --git a/python/formats/run_report_v2_tex.py b/python/formats/run_report_v2_tex.py
index c9b9077..007c3bd 100644
--- a/python/formats/run_report_v2_tex.py
+++ b/python/formats/run_report_v2_tex.py
@@ -207,7 +207,7 @@ def render_run_report_v2_tex(
             statics,
         )
     )
-    status = str(case["expected_status"])
+    status = str(reference["status"])
 
     source_artifact = artifacts["source_input"]
     assert isinstance(source_artifact, dict)
@@ -320,6 +320,13 @@ def render_run_report_v2_tex(
             rf"All named statuses agree & {_tex(agreement['all_status_equal'])} \\",
             rf"Agreement passed & {_tex(agreement['passed'])} \\",
             r"\end{tabular}",
+            *(
+                (
+                    r"\par",
+                    "Expected result: not supplied; result observed from four named engines.",
+                )
+                if case["expected_status"] is None else ()
+            ),
             _multi_panel_figure(
                 _milestones(manifest, "end_to_end"),
                 "Static semantic milestones from this validated full-pipeline run.",
diff --git a/python/native/multi_engine_pipeline.py b/python/native/multi_engine_pipeline.py
index 858002e..34933e9 100644
--- a/python/native/multi_engine_pipeline.py
+++ b/python/native/multi_engine_pipeline.py
@@ -138,6 +138,7 @@ def capture_multi_engine_native_pipeline(
     reference_options: TraceCaptureOptions,
     optimized_options: TraceCaptureOptions,
     clock_ns: Callable[[], int] = perf_counter_ns,
+    progress: Callable[[str], None] | None = None,
 ) -> MultiEngineNativeCapture:
     """Parse and reduce once, then capture reference and optimized exactly once."""
     if not isinstance(reference_options, TraceCaptureOptions):
@@ -147,11 +148,15 @@ def capture_multi_engine_native_pipeline(
     if not callable(clock_ns):
         raise TypeError("clock_ns must be callable")
 
+    if progress is not None:
+        progress("Parsing")
     started = clock_ns()
     with _loaded_formula(path) as native_formula:
         formula = _copy_formula(native_formula)
         parse_ns = _elapsed_ns(clock_ns, started)
 
+        if progress is not None:
+            progress("Reduction")
         started = clock_ns()
         with _built_explained_reduction(native_formula) as native_reduction:
             region = _copy_region(native_reduction.reduction.region)
@@ -168,6 +173,8 @@ def capture_multi_engine_native_pipeline(
                 ("reference", False, reference_options),
                 ("optimized", True, optimized_options),
             ):
+                if progress is not None:
+                    progress("Optimized" if optimized else "Reference")
                 started = clock_ns()
                 result, trace = _solve_native_traced(
                     native_reduction.reduction,
@@ -180,6 +187,11 @@ def capture_multi_engine_native_pipeline(
                 solve_timings[name] = _elapsed_ns(clock_ns, started)
 
                 if result.status is TilingSolveStatus.SAT:
+                    if progress is not None:
+                        progress(
+                            "Optimized verification" if optimized
+                            else "Reference verification"
+                        )
                     started = clock_ns()
                     assignment = _verify_and_extract(
                         native_formula,
diff --git a/renderer/pyproject.toml b/renderer/pyproject.toml
index db7a8c8..09d1716 100644
--- a/renderer/pyproject.toml
+++ b/renderer/pyproject.toml
@@ -1,6 +1,6 @@
 [project]
 name = "pap-render"
-version = "0.1.0"
+version = "1.0.0"
 description = "Add your description here"
 readme = "README.md"
 requires-python = ">=3.14"
diff --git a/renderer/test_wang_algorithm_animation.py b/renderer/test_wang_algorithm_animation.py
index 878a4d6..78ff945 100644
--- a/renderer/test_wang_algorithm_animation.py
+++ b/renderer/test_wang_algorithm_animation.py
@@ -1,7 +1,9 @@
 from __future__ import annotations
 
 from dataclasses import replace
+import io
 from pathlib import Path
+import re
 
 from PIL import Image, ImageDraw
 
@@ -116,6 +118,79 @@ def test_builder_animation_uses_versioned_provenance_and_is_byte_stable(tmp_path
     assert frame(bundle, 2).tobytes() != frame(crossover_changed, 2).tobytes()
 
 
+def _dense_builder_layout():
+    """Layout-only fixture with the 23 spans from the new 144x11 SAT capture."""
+    bundle = load_explainability_bundle(BUILDER_MANIFEST)
+    reduction = bundle.reduction
+    crossover = next(g for g in reduction.gadgets if g.kind == "crossover")
+    edges = (3, 7, 10, 12, 13, 21, 28, 34, 39, 43, 46, 48,
+             53, 57, 66, 74, 81, 87, 94, 103, 111, 121, 130, 140)
+    rows = (3, 2, 1, 0, 7, 6, 5, 4, 3, 2, 1, 4, 3, 8, 7, 6, 5, 6, 8, 7, 9, 8, 9)
+    gadgets = tuple(g for g in reduction.gadgets if g.kind in {"variable", "left_forward"})
+    gadgets += tuple(
+        replace(crossover, ordinal=i, x_begin=edges[i], x_end=edges[i + 1], swap_row=row)
+        for i, row in enumerate(rows)
+    )
+    region = replace(
+        bundle.region, max_x=143, active=(True,) * (144 * 11),
+        boundary=((None, None, None, None),) * (144 * 11),
+    )
+    return replace(bundle, region=region, reduction=replace(reduction, width=144, gadgets=gadgets))
+
+
+def _record_builder_text(monkeypatch):
+    records = []
+    original = ImageDraw.ImageDraw.text
+
+    def draw_and_record(draw, xy, text, *args, **kwargs):
+        bbox = draw.multiline_textbbox(
+            xy, text, font=kwargs.get("font"),
+            stroke_width=kwargs.get("stroke_width", 0),
+            spacing=kwargs.get("spacing", 4),
+        )
+        records.append((text, bbox))
+        return original(draw, xy, text, *args, **kwargs)
+
+    monkeypatch.setattr(ImageDraw.ImageDraw, "text", draw_and_record)
+    return records
+
+
+def test_builder_overflowing_swap_list_reports_count_and_omission_inside_panel(monkeypatch):
+    records = _record_builder_text(monkeypatch)
+    frame = wang_algorithm_animation._builder_frame(_dense_builder_layout(), 0)
+    evidence, bbox = next(
+        (text, bbox) for text, bbox in records
+        if text.startswith("source signals:") and "adjacent swaps:" in text
+    )
+    assert bbox[2] <= frame.width - 36
+    assert "adjacent swaps: 23" in evidence
+    assert "omitted" in evidence
+
+
+def test_builder_crowded_overview_has_no_colliding_labels_and_keeps_single_swap(monkeypatch):
+    records = _record_builder_text(monkeypatch)
+    bundle = _dense_builder_layout()
+    wang_algorithm_animation._builder_frame(bundle, 3)
+    boxes = [bbox for text, bbox in records if re.fullmatch(r"X\d+:s\d+", text)]
+    assert all(left[2] <= right[0] for left, right in zip(boxes, boxes[1:]))
+    assert any("23 crossover labels omitted" in text for text, _ in records)
+    assert any("23 validated adjacent swaps" in text for text, _ in records)
+    records.clear()
+    wang_algorithm_animation._builder_frame(bundle, 2)
+    assert any(text == "X0: swap rows 3/4" for text, _ in records)
+
+
+def test_builder_fitting_frames_keep_canonical_png_bytes():
+    bundle = load_explainability_bundle(BUILDER_MANIFEST)
+    for stage in range(6):
+        frame = wang_algorithm_animation._builder_frame(bundle, stage)
+        encoded = io.BytesIO()
+        frame.save(encoded, format="PNG", optimize=False, compress_level=9)
+        assert encoded.getvalue() == (
+            GOLDENS / "region-construction" / f"frame-{stage:02d}.png"
+        ).read_bytes()
+
+
 def test_builder_final_panel_distinguishes_region_and_boundary_states():
     bundle = load_explainability_bundle(BUILDER_MANIFEST)
     frame = getattr(wang_algorithm_animation, "_builder_frame")(bundle, 5)
@@ -175,6 +250,33 @@ def test_builder_preserves_noncanonical_region_capture_scope():
     ).size == (1976, 828)
 
 
+def test_builder_fits_all_labels_at_the_fifteen_signal_boundary(monkeypatch):
+    from wang_trace import load_trace_bundle
+
+    bundle = load_trace_bundle(
+        ROOT / "docs/assets/presentazione/search-unsat/reference-manifest.json"
+    )
+    signals = bundle.explanation.reduction.source_signals
+    assert len(signals) == 15
+    labels = []
+    original_centered_text = wang_algorithm_animation.centered_text
+
+    def check_label(draw, box, text, **kwargs):
+        bounds = draw.textbbox((0, 0), text, font=kwargs["font"])
+        assert bounds[2] - bounds[0] <= box[2] - box[0], text
+        assert bounds[3] - bounds[1] <= box[3] - box[1], text
+        labels.append(text)
+        return original_centered_text(draw, box, text, **kwargs)
+
+    monkeypatch.setattr(wang_algorithm_animation, "centered_text", check_label)
+    image = Image.new("RGB", (1976, 828), "white")
+    wang_algorithm_animation._draw_signal_order(
+        ImageDraw.Draw(image), y=140, label="source", signals=signals
+    )
+    assert len(labels) == 15
+    assert {"r #12", "r #13", "r #14"}.issubset(labels)
+
+
 def test_builder_summarizes_a_valid_44_variable_signal_strip():
     bundle = load_explainability_bundle(BUILDER_MANIFEST)
     reduction = bundle.reduction
diff --git a/renderer/test_wang_animation.py b/renderer/test_wang_animation.py
new file mode 100644
index 0000000..aa3e746
--- /dev/null
+++ b/renderer/test_wang_animation.py
@@ -0,0 +1,95 @@
+from __future__ import annotations
+
+import io
+
+from PIL import Image
+import pytest
+
+import wang_animation
+from wang_animation import write_animation_assets
+from wang_explain import EXPLAIN_OUTLINE_RGB
+
+
+def _frames(size, count):
+    return tuple(
+        Image.new("RGB", size, (20 * index, 10 * index, 200 - 10 * index))
+        for index in range(count)
+    )
+
+
+def _write(frames, destination):
+    return write_animation_assets(
+        frames, tuple(f"frame-{index}.png" for index in range(len(frames))),
+        destination, fallback_index=len(frames) - 1, duration_ms=80,
+    )
+
+
+@pytest.mark.parametrize(
+    "size,count,side,pixels,expected_extent",
+    [
+        ((12, 8), 5, 24, 10000, (24, 10)),  # Width bound.
+        ((8, 12), 10, 24, 10000, (12, 24)),  # Height bound.
+        ((12, 8), 7, 64, 300, (21, 12)),  # Area bound alone.
+        ((12, 8), 7, 24, 144, (15, 9)),  # Both bounds.
+        ((20, 1), 4, 30, 30, (15, 2)),  # One-pixel short side still fits area.
+    ],
+)
+def test_only_contact_thumbnails_shrink_within_limits_in_original_order(
+    tmp_path, monkeypatch, size, count, side, pixels, expected_extent
+):
+    frames = _frames(size, count)
+    source_pixels = tuple(frame.tobytes() for frame in frames)
+    baseline = _write(frames, tmp_path / "full-size")
+    monkeypatch.setattr(wang_animation, "MAX_CANVAS_SIDE", side)
+    monkeypatch.setattr(wang_animation, "MAX_CANVAS_PIXELS", pixels)
+
+    scaled = _write(frames, tmp_path / "bounded")
+    again = _write(frames, tmp_path / "repeated")
+
+    assert tuple(frame.size for frame in frames) == (size,) * count
+    assert tuple(frame.tobytes() for frame in frames) == source_pixels
+    assert scaled.fallback == scaled.frames[-1]
+    for full, bounded in zip(baseline.frames, scaled.frames, strict=True):
+        assert full.read_bytes() == bounded.read_bytes()
+    assert scaled.animation.read_bytes() == baseline.animation.read_bytes()
+    assert scaled.contact_sheet.read_bytes() == again.contact_sheet.read_bytes()
+
+    with Image.open(scaled.contact_sheet) as sheet:
+        assert sheet.size == expected_extent
+        assert sheet.width <= side and sheet.height <= side
+        assert sheet.width * sheet.height <= pixels
+        columns = 3
+        rows = (count + 2) // 3
+        width, height = sheet.width // columns, sheet.height // rows
+        # The minor dimension rounds down, but never below one pixel.
+        if size[0] >= size[1]:
+            assert abs(height - size[1] * width / size[0]) < 1
+        else:
+            assert abs(width - size[0] * height / size[1]) < 1
+        for index, frame in enumerate(frames):
+            center = ((index % 3) * width + width // 2, (index // 3) * height + height // 2)
+            assert sheet.getpixel(center) == frame.getpixel((0, 0))
+        # The final unused cell retains the existing background.
+        assert sheet.getpixel((sheet.width - 1, sheet.height - 1)) == EXPLAIN_OUTLINE_RGB
+
+
+@pytest.mark.parametrize("side,pixels", [(36, 864), (100, 10000)])
+def test_fitting_legacy_contact_sheet_keeps_exact_png_bytes(
+    tmp_path, monkeypatch, side, pixels
+):
+    frames = _frames((12, 8), 7)
+    # Nonuniform pixels also detect accidental resampling on the legacy branch.
+    frames[0].putpixel((1, 2), (255, 0, 71))
+    frames[6].putpixel((11, 7), (1, 2, 3))
+    expected = Image.new("RGB", (36, 24), EXPLAIN_OUTLINE_RGB)
+    positions = ((0, 0), (12, 0), (24, 0), (0, 8), (12, 8), (24, 8), (0, 16))
+    for frame, position in zip(frames, positions, strict=True):
+        expected.paste(frame, position)
+    encoded = io.BytesIO()
+    expected.save(encoded, format="PNG", optimize=False, compress_level=9)
+    monkeypatch.setattr(wang_animation, "MAX_CANVAS_SIDE", side)
+    monkeypatch.setattr(wang_animation, "MAX_CANVAS_PIXELS", pixels)
+
+    result = _write(frames, tmp_path / "legacy")
+
+    assert result.contact_sheet.read_bytes() == encoded.getvalue()
diff --git a/renderer/test_wang_narrative.py b/renderer/test_wang_narrative.py
index d4b46f1..08747db 100644
--- a/renderer/test_wang_narrative.py
+++ b/renderer/test_wang_narrative.py
@@ -74,7 +74,9 @@ def _run_record(
     *,
     manifest: Path | None = None,
     assignment: tuple[bool, ...] | None = None,
+    expectation_supplied: bool = True,
 ) -> dict[str, object]:
+    expected_status = status if expectation_supplied else None
     performed = status == "sat"
     checks = {}
     specifications = (
@@ -96,7 +98,7 @@ def _run_record(
             "witness_sha256": digest,
         }
     agreement = {
-        "expected_status": status,
+        "expected_status": expected_status,
         "boolean_z3_status": status,
         "reference_status": status,
         "optimized_status": status,
@@ -135,12 +137,42 @@ def _run_record(
     ).hexdigest()
     return {
         "schema": "wang-verification-receipts-v1",
-        "expected_status": status,
+        "expected_status": expected_status,
         **receipt_payload,
         "source_sha256": source_sha256,
     }
 
 
+@pytest.mark.parametrize("status", ["sat", "unsat"])
+def test_nullable_verification_uses_observed_consensus_and_binds_receipts(tmp_path, status):
+    context = (
+        {"manifest_path": TRACE_MANIFEST, "solution_path": TRACE_SOLUTION,
+         "extracted_assignment": ASSIGNMENT}
+        if status == "sat" else {}
+    )
+    document = _run_record(
+        status, expectation_supplied=False,
+        manifest=TRACE_MANIFEST if status == "sat" else None,
+        assignment=ASSIGNMENT if status == "sat" else None,
+    )
+    path = tmp_path / "receipts.json"
+    path.write_text(json.dumps(document), encoding="utf-8")
+    observed, records, _, _, _ = wang_narrative._load_verification(path, **context)
+    assert observed == status
+    assert all(record["performed"] is (status == "sat") for record in records)
+    for field, value in (("reference_status", "unknown"), ("optimized_status", "unsat" if status == "sat" else "sat"), ("expected_status", status)):
+        original = document["agreement"][field]
+        document["agreement"][field] = value
+        path.write_text(json.dumps(document), encoding="utf-8")
+        with pytest.raises(WangSquareRenderError, match="agreement"):
+            wang_narrative._load_verification(path, **context)
+        document["agreement"][field] = original
+    document["source_sha256"] = "0" * 64
+    path.write_text(json.dumps(document), encoding="utf-8")
+    with pytest.raises(WangSquareRenderError, match="source"):
+        wang_narrative._load_verification(path, **context)
+
+
 def test_verification_composition_is_deterministic_for_sat_and_unsat(tmp_path):
     for status in ("unsat",):
         run = tmp_path / f"{status}.json"
diff --git a/renderer/test_wang_trace.py b/renderer/test_wang_trace.py
index 35b7762..e9174b5 100644
--- a/renderer/test_wang_trace.py
+++ b/renderer/test_wang_trace.py
@@ -175,7 +175,8 @@ def test_one_composition_chain_is_byte_stable_for_png_sheet_and_gif(tmp_path):
     assert first.contact_sheet.name == "contact-sheet.png"
     with Image.open(first.frames[0]) as frame:
         assert frame.mode == "RGB"
-        assert frame.size == (1976, 828)
+        assert frame.size == (1976, 972)
+    assert {Image.open(frame).size for frame in first.frames} == {(1976, 972)}
     with Image.open(first.animation) as animation:
         assert animation.format == "GIF"
         assert animation.n_frames == 10
@@ -248,7 +249,7 @@ def test_observed_mrv_selection_is_row_major_and_deterministic(tmp_path):
     render_trace_assets(MANIFEST, second_dir, max_frames=10)
 
     assert _tree_bytes(first_dir) == _tree_bytes(second_dir)
-    assert Image.open(first.fallback).size == (1976, 828)
+    assert Image.open(first.fallback).size == (1976, 972)
 
 
 def test_active_domain_counts_exclude_inactive_positions():
@@ -273,8 +274,99 @@ def test_mrv_legend_uses_the_unresolved_grid_color(tmp_path):
 def test_decision_fallback_has_large_focused_mrv_summary_cards(tmp_path):
     rendered = render_trace_assets(MANIFEST, tmp_path / "rendered", max_frames=10)
     with Image.open(rendered.fallback) as fallback:
-        assert fallback.getpixel((1630, 660)) == EXPLAIN_SELECTED_MRV_RGB
-        assert fallback.getpixel((1804, 660)) == EXPLAIN_DECISION_RGB
+        assert fallback.getpixel((1630, 804)) == EXPLAIN_SELECTED_MRV_RGB
+        assert fallback.getpixel((1804, 804)) == EXPLAIN_DECISION_RGB
+
+
+@pytest.mark.parametrize(
+    "event_index", (1, 3, 5, 6), ids=("mrv", "propagation", "conflict", "rollback")
+)
+def test_narrow_region_keeps_summary_text_inside_canvas_and_clear_of_cards(
+    monkeypatch, event_index
+):
+    bundle = load_trace_bundle(MANIFEST)
+    initial = tuple({0: 9, 1: 384, 20: 320}.get(cell, 0) for cell in range(77))
+    events = (
+        TraceEvent(0, "root", "initial", None, 0, None, 0, None, None, None),
+        TraceEvent(1, "decision", "search", None, 1, 0, 0, 9, 1, None),
+        TraceEvent(2, "domain_reduction", "search", "decision", 1, 0, 1, 9, 1, None),
+        TraceEvent(3, "domain_reduction", "search", "propagation", 1, 1, 2, 384, 128, None),
+        TraceEvent(4, "domain_reduction", "search", "propagation", 1, 20, 3, 320, 0, None),
+        TraceEvent(5, "conflict", "search", None, 1, 20, 3, None, None, None),
+        TraceEvent(6, "backtrack", "search", None, 1, 0, 0, None, None, None),
+        TraceEvent(7, "decision", "search", None, 1, 0, 0, 9, 8, None),
+        TraceEvent(8, "domain_reduction", "search", "decision", 1, 0, 1, 9, 8, None),
+        TraceEvent(9, "result", None, None, 0, None, 1, None, None, "sat"),
+    )
+    trace = replace(
+        bundle.trace,
+        width=7,
+        height=11,
+        initial_domains=initial,
+        events=events,
+        event_capacity=len(events),
+        observed_event_count=len(events),
+        checkpoints=(),
+        checkpoint_interval=0,
+        checkpoint_capacity=0,
+    )
+    region = replace(
+        bundle.explanation.region,
+        max_x=6,
+        max_y=10,
+        active=tuple(bool(domain) for domain in initial),
+    )
+    bundle = replace(
+        bundle, trace=trace, explanation=replace(bundle.explanation, region=region)
+    )
+    states = replay_trace(trace)
+    event = events[event_index]
+    before = states[event_index - 1]
+    texts = []
+    legend_texts = []
+    cards = []
+    summaries = []
+    original_text = ImageDraw.ImageDraw.text
+    original_rectangle = ImageDraw.ImageDraw.rectangle
+
+    def record_text(draw, xy, text, *args, **kwargs):
+        if xy[0] == 52 and xy[1] >= 600:
+            texts.append((text, draw.textbbox(xy, text, font=kwargs["font"])))
+        if xy[0] in (304, 356):
+            legend_texts.append((text, draw.textbbox(xy, text, font=kwargs["font"])))
+        return original_text(draw, xy, text, *args, **kwargs)
+
+    def record_rectangle(draw, xy, *args, **kwargs):
+        if xy[0] == 28 and xy[1] >= 600 and xy[2] - xy[0] > 100:
+            summaries.append(xy)
+        if xy[0] > 52 and xy[1] > 600 and xy[2] - xy[0] > 100:
+            cards.append(xy)
+        return original_rectangle(draw, xy, *args, **kwargs)
+
+    monkeypatch.setattr(ImageDraw.ImageDraw, "text", record_text)
+    monkeypatch.setattr(ImageDraw.ImageDraw, "rectangle", record_rectangle)
+    frame = wang_trace_render._compose_frame(
+        bundle,
+        event,
+        before if event.kind == "decision" else states[event_index],
+        before,
+        event_index,
+    )
+
+    assert len(texts) >= 2 and len(cards) >= 2
+    assert len(summaries) == 1 and len(legend_texts) >= 5
+    for text, box in legend_texts:
+        assert box[3] < summaries[0][1], text
+    for text, box in texts:
+        assert 0 <= box[0] < box[2] < frame.width, text
+        assert 0 <= box[1] < box[3] < frame.height, text
+        for card in cards:
+            assert (
+                box[2] <= card[0]
+                or card[2] <= box[0]
+                or box[3] <= card[1]
+                or card[3] <= box[1]
+            ), text
 
 
 def test_sat_selection_keeps_a_decision_restriction_and_its_continuation():
@@ -308,8 +400,8 @@ def test_trace_story_facts_remain_readable_at_390_px(tmp_path):
     propagation = tmp_path / "rendered/frame-002519.png"
     assert propagation in rendered.frames
     with Image.open(propagation) as frame:
-        assert _display_ink_height(frame, (52, 676, 1400, 734)) >= 8
-        assert _display_ink_height(frame, (52, 726, 1400, 784)) >= 8
+        assert _display_ink_height(frame, (52, 820, 1400, 878)) >= 8
+        assert _display_ink_height(frame, (52, 882, 1400, 944)) >= 8
 
     conflict = _search_story_panel(bundle, 2)
     assert _display_ink_height(conflict, (52, 828, 1400, 900)) >= 8
diff --git a/renderer/uv.lock b/renderer/uv.lock
index d19ab82..60f7547 100644
--- a/renderer/uv.lock
+++ b/renderer/uv.lock
@@ -60,7 +60,7 @@ wheels = [
 
 [[package]]
 name = "pap-render"
-version = "0.1.0"
+version = "1.0.0"
 source = { virtual = "." }
 dependencies = [
     { name = "numpy" },
diff --git a/renderer/wang_algorithm_animation.py b/renderer/wang_algorithm_animation.py
index e24f347..9bc0c4b 100644
--- a/renderer/wang_algorithm_animation.py
+++ b/renderer/wang_algorithm_animation.py
@@ -208,14 +208,13 @@ def _draw_signal_order(
         )
         font_size = 16 if signal is None else 28
         font = explain_font(font_size * scale)
-        if len(signals) > 15:
-            inner_width = box_width - 8
-            while font_size > 12:
-                text_box = draw.textbbox((0, 0), text, font=font)
-                if text_box[2] - text_box[0] <= inner_width:
-                    break
-                font_size -= 1
-                font = explain_font(font_size * scale)
+        inner_width = box_width - 8
+        while font_size > 12:
+            text_box = draw.textbbox((0, 0), text, font=font)
+            if text_box[2] - text_box[0] <= inner_width:
+                break
+            font_size -= 1
+            font = explain_font(font_size * scale)
         centered_text(
             draw,
             (x + 4, y + 3, x + box_width - 4, y + 55),
@@ -340,6 +339,22 @@ def _builder_frame(bundle: object, stage: int) -> Image.Image:
                 outline=(174, 181, 193),
             )
 
+    crossover_labels_omitted = False
+    if stage == 3:
+        previous_right = origin_x
+        for gadget in crossovers:
+            label_box = draw.textbbox(
+                (origin_x + gadget.x_begin * cell + 8,
+                 origin_y + gadget.y_begin * cell + 5),
+                f"X{gadget.ordinal}:s{gadget.swap_row}",
+                font=explain_font(14 * EXPLAIN_RENDER_SCALE),
+                stroke_width=3,
+            )
+            if label_box[0] < previous_right or label_box[2] > origin_x + grid_width:
+                crossover_labels_omitted = True
+                break
+            previous_right = label_box[2]
+
     for gadget in reduction.gadgets:
         visible = (
             (stage == 0 and gadget.kind == "variable")
@@ -366,7 +381,9 @@ def _builder_frame(bundle: object, stage: int) -> Image.Image:
             outline=_GADGET_COLORS[gadget.kind],
             width=width,
         )
-        if gadget.kind == "crossover" and stage in {2, 3}:
+        if gadget.kind == "crossover" and (
+            stage == 2 or (stage == 3 and not crossover_labels_omitted)
+        ):
             crossover_label = (
                 f"X{gadget.ordinal}: swap rows "
                 f"{gadget.swap_row}/{gadget.swap_row + 1}"
@@ -464,11 +481,19 @@ def _builder_frame(bundle: object, stage: int) -> Image.Image:
                 fill=EXPLAIN_TEXT_RGB,
             )
             y += 42
+        evidence_font = explain_font(14 * EXPLAIN_RENDER_SCALE)
+        swap_list = "adjacent swaps: " + ", ".join(
+            str(gadget.swap_row) for gadget in crossovers
+        )
+        if draw.textbbox((legend_x, 0), swap_list, font=evidence_font)[2] > image.width - 36:
+            swap_list = f"adjacent swaps: {len(crossovers)} (row list omitted)"
+        evidence = f"source signals: {len(reduction.source_signals)}\n{swap_list}"
+        if crossover_labels_omitted:
+            evidence += f"\n{len(crossovers)} crossover labels omitted (overview)"
         draw.text(
             (legend_x, y + 8),
-            f"source signals: {len(reduction.source_signals)}\nadjacent swaps: "
-            + ", ".join(str(gadget.swap_row) for gadget in crossovers),
-            font=explain_font(14 * EXPLAIN_RENDER_SCALE),
+            evidence,
+            font=evidence_font,
             fill=EXPLAIN_TEXT_RGB,
             spacing=12,
         )
diff --git a/renderer/wang_animation.py b/renderer/wang_animation.py
index ac06e51..ee2f15d 100644
--- a/renderer/wang_animation.py
+++ b/renderer/wang_animation.py
@@ -99,11 +99,39 @@ def write_animation_assets(
         or sheet_height > MAX_CANVAS_SIDE
         or sheet_width * sheet_height > MAX_CANVAS_PIXELS
     ):
-        raise WangSquareRenderError("animation contact sheet exceeds canvas limits")
+        # Keep full-resolution frames/GIF; shrink only contact-sheet thumbnails.
+        # An integer search also handles very thin frames whose short side must
+        # remain at least one pixel. A square-root scale alone can exceed the
+        # area limit after clamping that short side.
+        longest = max(frame_width, frame_height)
+        lower, upper = 1, longest
+        thumbnail_size = None
+        while lower <= upper:
+            candidate = (lower + upper) // 2
+            width = max(1, frame_width * candidate // longest)
+            height = max(1, frame_height * candidate // longest)
+            if (
+                columns * width <= MAX_CANVAS_SIDE
+                and rows * height <= MAX_CANVAS_SIDE
+                and columns * width * rows * height <= MAX_CANVAS_PIXELS
+            ):
+                thumbnail_size = (width, height)
+                lower = candidate + 1
+            else:
+                upper = candidate - 1
+        if thumbnail_size is None:
+            raise WangSquareRenderError("animation contact sheet exceeds canvas limits")
+        frame_width, frame_height = thumbnail_size
+        sheet_width = columns * frame_width
+        sheet_height = rows * frame_height
     sheet = Image.new("RGB", (sheet_width, sheet_height), EXPLAIN_OUTLINE_RGB)
     for index, frame in enumerate(frames):
+        thumbnail = (
+            frame if frame.size == (frame_width, frame_height)
+            else frame.resize((frame_width, frame_height), Image.Resampling.LANCZOS)
+        )
         sheet.paste(
-            frame,
+            thumbnail,
             ((index % columns) * frame_width, (index // columns) * frame_height),
         )
     contact_path = destination / "contact-sheet.png"
diff --git a/renderer/wang_narrative.py b/renderer/wang_narrative.py
index b4160a1..06e289d 100644
--- a/renderer/wang_narrative.py
+++ b/renderer/wang_narrative.py
@@ -351,9 +351,11 @@ def _load_verification(
         raise WangSquareRenderError("verification receipt snapshot must be closed")
     if document["schema"] != "wang-verification-receipts-v1":
         raise WangSquareRenderError("verification receipt schema is unsupported")
-    status = document["expected_status"]
-    if type(status) is not str or status not in {"sat", "unsat"}:
-        raise WangSquareRenderError("verification receipt status is unsupported")
+    expected_status = document["expected_status"]
+    if expected_status is not None and (
+        type(expected_status) is not str or expected_status not in {"sat", "unsat"}
+    ):
+        raise WangSquareRenderError("verification receipt expectation is unsupported")
     verification = document["verification"]
     agreement = document["agreement"]
     if type(verification) is not dict or set(verification) != {
@@ -372,8 +374,12 @@ def _load_verification(
     }
     if type(agreement) is not dict or set(agreement) != agreement_fields:
         raise WangSquareRenderError("verification agreement must be closed")
+    status = agreement["reference_status"]
+    if type(status) is not str or status not in {"sat", "unsat"}:
+        raise WangSquareRenderError("verification agreement status is unsupported")
     if (
-        agreement["expected_status"] != status
+        agreement["expected_status"] != expected_status
+        or (expected_status is not None and expected_status != status)
         or any(
             agreement[name] != status
             for name in (
diff --git a/renderer/wang_trace_render.py b/renderer/wang_trace_render.py
index 049502e..6d12fcf 100644
--- a/renderer/wang_trace_render.py
+++ b/renderer/wang_trace_render.py
@@ -40,6 +40,11 @@
 _HEADER: Final = 76 * EXPLAIN_RENDER_SCALE
 _LEGEND_WIDTH: Final = 210 * EXPLAIN_RENDER_SCALE
 _GAP: Final = 12 * EXPLAIN_RENDER_SCALE
+# Summary text and cards need room independent of the input region's width.
+_MIN_FRAME_WIDTH: Final = 960 * EXPLAIN_RENDER_SCALE
+# Six legend swatches plus five detail lines must fit above every summary.
+# Keep the same body height for every event so animation frames stay uniform.
+_MIN_BODY_HEIGHT: Final = 270 * EXPLAIN_RENDER_SCALE
 _UNSAT_RGB: Final = EXPLAIN_CONFLICT_RGB
 _SINGLETON_RGB: Final = EXPLAIN_SINGLETON_RGB
 _CHANGED_RGB: Final = EXPLAIN_DECISION_RGB
@@ -50,9 +55,11 @@ def _scaled(value: int) -> int:
 
 
 def _frame_height(grid_height: int) -> int:
-    return 2 * _MARGIN + _HEADER + max(
-        grid_height + _scaled(112),
-        _scaled(310),
+    return (
+        2 * _MARGIN
+        + _HEADER
+        + max(grid_height, _MIN_BODY_HEIGHT)
+        + _scaled(112)
     )
 
 
@@ -589,7 +596,9 @@ def _compose_frame(
             )
     grid_width = region.width * _CELL_SIZE
     grid_height = region.height * _CELL_SIZE
-    width = 2 * _MARGIN + grid_width + _GAP + _LEGEND_WIDTH
+    width = max(
+        _MIN_FRAME_WIDTH, 2 * _MARGIN + grid_width + _GAP + _LEGEND_WIDTH
+    )
     height = _frame_height(grid_height)
     if (
         width > MAX_CANVAS_SIDE
@@ -742,7 +751,7 @@ def _compose_frame(
             fill=EXPLAIN_MUTED_RGB,
         )
         y += _scaled(15)
-    summary_top = top + grid_height + _scaled(12)
+    summary_top = top + max(grid_height, _MIN_BODY_HEIGHT) + _scaled(12)
     if mrv_candidates:
         summary_box = (
             _MARGIN,
diff --git a/schemas/wang-narrative-assets-v1.schema.json b/schemas/wang-narrative-assets-v1.schema.json
index c761047..3f847bf 100644
--- a/schemas/wang-narrative-assets-v1.schema.json
+++ b/schemas/wang-narrative-assets-v1.schema.json
@@ -22,9 +22,13 @@
       "required": ["id", "expected_status", "source_sha256"],
       "properties": {
         "id": {"type": "string", "minLength": 1},
-        "expected_status": {"enum": ["sat", "unsat"]},
+        "expected_status": {"enum": ["sat", "unsat", null]},
+        "observed_status": {"enum": ["sat", "unsat"]},
         "source_sha256": {"$ref": "#/$defs/sha256"}
-      }
+      },
+      "if": {"properties": {"expected_status": {"type": "null"}}},
+      "then": {"required": ["observed_status"]},
+      "else": {"not": {"required": ["observed_status"]}}
     },
     "identities": {
       "type": "object",
diff --git a/schemas/wang-run-case-v2.schema.json b/schemas/wang-run-case-v2.schema.json
index 105a20f..c6109f2 100644
--- a/schemas/wang-run-case-v2.schema.json
+++ b/schemas/wang-run-case-v2.schema.json
@@ -20,7 +20,7 @@
     "title": {"type": "string", "minLength": 1},
     "purpose": {"type": "string", "minLength": 1},
     "source": {"type": "string", "pattern": "^(?!/)(?!.*(?:^|/)\\.\\.?/).+\\.cm13$"},
-    "expected_status": {"enum": ["sat", "unsat"]},
+    "expected_status": {"enum": ["sat", "unsat", null]},
     "reference_trace": {"$ref": "#/$defs/trace"},
     "optimized_trace": {"$ref": "#/$defs/trace"}
   },
diff --git a/schemas/wang-run-dossier-v2.schema.json b/schemas/wang-run-dossier-v2.schema.json
index ac4e83b..cb79797 100644
--- a/schemas/wang-run-dossier-v2.schema.json
+++ b/schemas/wang-run-dossier-v2.schema.json
@@ -30,7 +30,7 @@
         "id": {"type": "string", "pattern": "^[a-z0-9]+(?:-[a-z0-9]+)*$"},
         "title": {"type": "string", "minLength": 1},
         "purpose": {"type": "string", "minLength": 1},
-        "expected_status": {"enum": ["sat", "unsat"]}
+        "expected_status": {"enum": ["sat", "unsat", null]}
       }
     },
     "source": {
@@ -110,7 +110,7 @@
         "passed"
       ],
       "properties": {
-        "expected_status": {"enum": ["sat", "unsat"]},
+        "expected_status": {"enum": ["sat", "unsat", null]},
         "boolean_z3_status": {"enum": ["sat", "unsat"]},
         "reference_status": {"enum": ["sat", "unsat"]},
         "optimized_status": {"enum": ["sat", "unsat"]},
diff --git a/tests/fixtures/demo_process.py b/tests/fixtures/demo_process.py
new file mode 100644
index 0000000..32d1bb5
--- /dev/null
+++ b/tests/fixtures/demo_process.py
@@ -0,0 +1,53 @@
+"""Real subprocess tree used only by the demo supervisor tests."""
+
+from pathlib import Path
+import ctypes
+import os
+import signal
+import subprocess
+import sys
+import time
+
+
+mode, location = sys.argv[1:]
+root = Path(location)
+
+
+def wait_for(name):
+    deadline = time.monotonic() + 8
+    while not (root / name).exists():
+        if time.monotonic() >= deadline:
+            raise RuntimeError(f"fixture did not receive {name}")
+        time.sleep(0.01)
+
+
+if mode in ("child", "grandchild"):
+    signal.signal(signal.SIGTERM, signal.SIG_IGN)
+    (root / f"{mode}.pid").write_text(str(os.getpid()))
+    if mode == "child":
+        subprocess.Popen([sys.executable, __file__, "grandchild", str(root)])
+        wait_for("grandchild.pid")
+    (root / f"{mode}.ready").touch()
+    while True:
+        time.sleep(0.02)
+
+(root / "worker.pid").write_text(str(os.getpid()))
+if mode == "unusual-name":
+    # /proc stat comm is arbitrary bytes and can contain whitespace/parentheses.
+    assert ctypes.CDLL(None).prctl(15, b"demo \xff ) name", 0, 0, 0) == 0
+if mode == "normal":
+    print("normal worker output", flush=True)
+    sys.exit(0)
+
+subprocess.Popen([sys.executable, __file__, "child", str(root)])
+wait_for("child.ready")
+(root / "ready").touch()
+sys.stdout.write("partial output without newline")
+sys.stdout.flush()
+if mode in ("leader0", "leader7"):
+    wait_for("release")
+    sys.exit(0 if mode == "leader0" else 7)
+while True:
+    if mode == "verbose":
+        os.write(sys.stdout.fileno(), b"x" * 65536)
+    time.sleep(0.002)
diff --git a/tests/instances/demo_sat.cm13 b/tests/instances/demo_sat.cm13
new file mode 100644
index 0000000..45a3fa3
--- /dev/null
+++ b/tests/instances/demo_sat.cm13
@@ -0,0 +1,5 @@
+c Direct-input demo smoke; each clause requires x1 + x2 + x3 = 1
+p cm13 3 3
+2 3 1 0
+1 3 2 0
+3 2 1 0
diff --git a/tests/python/test_demo_capture.py b/tests/python/test_demo_capture.py
new file mode 100644
index 0000000..e4b5e30
--- /dev/null
+++ b/tests/python/test_demo_capture.py
@@ -0,0 +1,169 @@
+from __future__ import annotations
+
+from dataclasses import replace
+import hashlib
+from pathlib import Path
+import tempfile
+import unittest
+from unittest.mock import patch
+
+from dossier import multi_engine
+from formats.pipeline_snapshot import PipelineSnapshotError
+from formats.run_case_v2 import load_run_case_v2
+from formats.run_dossier_v2_bundle import load_run_dossier_v2
+from native.formula_adapter import FormulaLoadError
+from native import multi_engine_pipeline as native
+
+
+ROOT = Path(__file__).resolve().parents[2]
+CASE = ROOT / "examples/run-cases-v2/pipeline-sat.json"
+SOURCE = ROOT / "tests/instances/pipeline_sat.cm13"
+
+
+class DemoCaptureTests(unittest.TestCase):
+    def direct(self, *args, **kwargs):
+        producer = getattr(multi_engine, "generate_input_dossier", None)
+        self.assertTrue(callable(producer), "direct file producer is missing")
+        return producer(*args, **kwargs)
+
+    def test_named_case_copies_before_native_capture_and_preserves_basename(self):
+        with tempfile.TemporaryDirectory() as name:
+            root = Path(name)
+            source = root / "legacy-name.cm13"
+            content = SOURCE.read_bytes()
+            source.write_bytes(content)
+            case = replace(load_run_case_v2(CASE, ROOT), source=source.name)
+
+            def inspect_copy(path, **kwargs):
+                self.assertNotEqual(path, source)
+                self.assertEqual(path.name, source.name)
+                self.assertEqual(path.read_bytes(), content)
+                source.write_text("changed original")
+                self.assertEqual(path.read_bytes(), content)
+                raise RuntimeError("stop after copy inspection")
+
+            with patch.object(multi_engine, "ROOT", root), patch.object(
+                multi_engine, "load_run_case_v2", return_value=case
+            ), patch.object(multi_engine, "capture_multi_engine_native_pipeline", side_effect=inspect_copy):
+                with self.assertRaisesRegex(RuntimeError, "stop after copy"):
+                    multi_engine.generate_multi_engine_dossier(CASE, root / "out")
+            self.assertEqual(sorted(p.name for p in root.iterdir()), [source.name])
+
+    def test_direct_capture_freezes_external_bytes_and_runs_each_engine_once(self):
+        with tempfile.TemporaryDirectory(prefix="demo input ") as name:
+            root = Path(name)
+            source = root / "formula $(touch never) `false` ; #.cm13"
+            content = b"c External demo input\n" + SOURCE.read_bytes()
+            source.write_bytes(content)
+            destination = root / "dossier"
+            progress = []
+            original_capture = multi_engine.capture_multi_engine_native_pipeline
+            original_export = multi_engine.dump_solver_trace_bundle
+
+            def capture_copy(path, **kwargs):
+                self.assertEqual(path.name, "input.cm13")
+                self.assertNotEqual(path, source)
+                source.write_text("malformed after copy")
+                self.assertEqual(path.read_bytes(), content)
+                return original_capture(path, **kwargs)
+
+            def export_copy(manifest, path, *args, **kwargs):
+                self.assertEqual(path.name, "input.cm13")
+                self.assertEqual(path.read_bytes(), content)
+                return original_export(manifest, path, *args, **kwargs)
+
+            with patch.object(multi_engine, "capture_multi_engine_native_pipeline", side_effect=capture_copy), patch.object(
+                multi_engine, "dump_solver_trace_bundle", side_effect=export_copy
+            ), patch.object(native, "_loaded_formula", wraps=native._loaded_formula) as parse, patch.object(
+                native, "_built_explained_reduction", wraps=native._built_explained_reduction
+            ) as reduce, patch.object(native, "_solve_native_traced", wraps=native._solve_native_traced) as solve, patch.object(
+                multi_engine, "build_boolean_z3_summary", wraps=multi_engine.build_boolean_z3_summary
+            ) as boolean, patch.object(multi_engine, "build_wang_z3_summary", wraps=multi_engine.build_wang_z3_summary) as wang:
+                self.direct(source, destination, include_pdf=False, progress=progress.append)
+            self.assertEqual((parse.call_count, reduce.call_count, solve.call_count, boolean.call_count, wang.call_count), (1, 1, 2, 1, 1))
+            self.assertEqual([call.kwargs["optimized"] for call in solve.call_args_list], [False, True])
+            for call in solve.call_args_list:
+                self.assertEqual((call.kwargs["event_capacity"], call.kwargs["checkpoint_interval"], call.kwargs["checkpoint_capacity"]), (100000, 0, 0))
+            run = load_run_dossier_v2(destination / "run.json")
+            self.assertIsNone(run["case"]["expected_status"])
+            self.assertEqual({run[engine]["status"] for engine in ("reference", "optimized", "boolean_z3", "wang_z3")}, {"sat"})
+            self.assertEqual(run["source"]["sha256"], hashlib.sha256(content).hexdigest())
+            self.assertEqual((destination / run["artifacts"]["source_input"]["path"]).read_bytes(), content)
+            self.assertEqual(progress, ["Parsing", "Reduction", "Reference", "Reference verification", "Optimized", "Optimized verification", "Boolean Z3", "Boolean Z3 verification", "Wang Z3", "Wang Z3 verification", "Bundle verification", "Figures", "Final validation"])
+
+    def test_progress_callbacks_precede_real_operations_and_measured_windows(self):
+        ticks = 0
+        events = []
+
+        def clock():
+            nonlocal ticks
+            ticks += 10
+            return ticks
+
+        def progress(label):
+            nonlocal ticks
+            ticks += 1000
+            events.append(label)
+
+        options = native.TraceCaptureOptions(100000, 0, 0)
+        self.assertIn("progress", __import__("inspect").signature(native.capture_multi_engine_native_pipeline).parameters)
+        capture = native.capture_multi_engine_native_pipeline(SOURCE, reference_options=options, optimized_options=options, clock_ns=clock, progress=progress)
+        self.assertEqual(events, ["Parsing", "Reduction", "Reference", "Reference verification", "Optimized", "Optimized verification"])
+        self.assertEqual([getattr(capture.timings, key) for key in capture.timings.__dataclass_fields__], [10] * 6)
+
+    def test_direct_capture_rejects_malformed_input_and_incomplete_trace(self):
+        with tempfile.TemporaryDirectory() as name:
+            root = Path(name)
+            source = root / "malformed.cm13"
+            source.write_text("p cm13 nope\n")
+            with self.assertRaises(FormulaLoadError):
+                self.direct(source, root / "bad", include_pdf=False)
+            with patch.object(
+                multi_engine, "dump_solver_trace_bundle",
+                side_effect=AssertionError("incomplete traces must fail before export"),
+            ) as export:
+                with self.assertRaisesRegex((PipelineSnapshotError, multi_engine.MultiEngineDossierError), "complete|truncat"):
+                    self.direct(SOURCE, root / "short", include_pdf=False, event_capacity=2)
+                export.assert_not_called()
+            self.assertEqual(sorted(p.name for p in root.iterdir()), [source.name])
+
+    def test_direct_trace_capacity_rejected_before_reading_source(self):
+        for capacity in (None, True, 1, 100001, 2.0, "2"):
+            with self.subTest(capacity=capacity), self.assertRaisesRegex(ValueError, "capacity"):
+                self.direct("missing.cm13", "unused", event_capacity=capacity)
+
+    def test_existing_output_including_dangling_symlink_is_never_followed(self):
+        with tempfile.TemporaryDirectory() as name:
+            root = Path(name)
+            for generate, source in ((multi_engine.generate_multi_engine_dossier, CASE), (self.direct, SOURCE)):
+                destination = root / "link"
+                destination.symlink_to(root / "missing")
+                try:
+                    with self.assertRaisesRegex(multi_engine.MultiEngineDossierError, "already exists"):
+                        generate(source, destination, include_pdf=False)
+                    self.assertTrue(destination.is_symlink())
+                    self.assertFalse((root / "missing").exists())
+                finally:
+                    destination.unlink()
+
+    def test_direct_capture_rejects_unknown_disagreement_and_engine_error(self):
+        actual_boolean = multi_engine.build_boolean_z3_summary
+        with tempfile.TemporaryDirectory() as name:
+            root = Path(name)
+            for status, message in (("unknown", "UNKNOWN"), ("unsat", "status mismatch"), ("error", "engine failed")):
+                def altered(*args, **kwargs):
+                    if status == "error":
+                        raise RuntimeError("engine failed")
+                    result = actual_boolean(*args, **kwargs)
+                    result["status"] = status
+                    result["model"]["assignment"] = None
+                    result["statistics"][-1]["value"] = 0
+                    return result
+                with self.subTest(status=status), patch.object(multi_engine, "build_boolean_z3_summary", side_effect=altered):
+                    with self.assertRaisesRegex((RuntimeError, ValueError), message):
+                        self.direct(SOURCE, root / status, include_pdf=False)
+                self.assertEqual(list(root.iterdir()), [])
+
+
+if __name__ == "__main__":
+    unittest.main()
diff --git a/tests/python/test_demo_check.py b/tests/python/test_demo_check.py
new file mode 100644
index 0000000..7d21653
--- /dev/null
+++ b/tests/python/test_demo_check.py
@@ -0,0 +1,295 @@
+from __future__ import annotations
+
+import contextlib
+import importlib
+import importlib.util
+import io
+import os
+from pathlib import Path
+import shlex
+import subprocess
+import sys
+import tempfile
+import unittest
+from unittest.mock import patch
+
+from crosscheck import witness_pipeline
+from model.tiling import TilingSolveResult, TilingSolveStatus
+from model.tileset import TILESET
+from native import formula_adapter
+from native.formula_adapter import FormulaLoadError, FormulaParseStatus
+from oracles import boolean_solver, tiling_check, tiling_solver
+from oracles.boolean_solver import BooleanSolveResult, BooleanSolveStatus
+from tools import demo
+
+
+ROOT = Path(__file__).resolve().parents[2]
+
+
+class DemoCheckTests(unittest.TestCase):
+    def setUp(self):
+        self.assertIsNotNone(
+            importlib.util.find_spec("tools.demo_check"),
+            "the narrated demo-check command is missing",
+        )
+        self.command = importlib.import_module("tools.demo_check")
+
+    def worker(self):
+        with tempfile.TemporaryDirectory() as name:
+            run = Path(name)
+            with contextlib.redirect_stdout(io.StringIO()) as out, contextlib.redirect_stderr(io.StringIO()) as err:
+                code = self.command._worker(run)
+            marker = run / "complete"
+            return code, out.getvalue(), err.getvalue(), marker.read_bytes() if marker.exists() else None
+
+    def test_six_real_checks_reuse_each_engine_result_and_reject_one_changed_tile(self):
+        checked = []
+        actual_check = tiling_check.is_valid_tiling
+
+        def record_check(region, tileset, tiling):
+            valid = actual_check(region, tileset, tiling)
+            checked.append((region, tuple(tiling), valid))
+            return valid
+
+        with patch.object(witness_pipeline, "solve_native_and_extract", wraps=witness_pipeline.solve_native_and_extract) as native, patch.object(
+            boolean_solver, "solve_boolean", wraps=boolean_solver.solve_boolean
+        ) as boolean, patch.object(tiling_solver, "solve_tiling", wraps=tiling_solver.solve_tiling) as wang, patch.object(
+            tiling_check, "is_valid_tiling", side_effect=record_check
+        ):
+            code, out, err, marker = self.worker()
+        self.assertEqual(code, 0, err)
+        self.assertEqual(marker, b"6/6\n")
+        self.assertEqual([line.split()[0] for line in out.splitlines() if line.startswith("[")], [f"[{i}/6]" for i in range(1, 7)])
+        self.assertEqual(out.count("OK:"), 6)
+        self.assertIn("SAT", out)
+        self.assertIn("UNSAT", out)
+        self.assertIn("rifiut", out.lower())
+        self.assertEqual((native.call_count, boolean.call_count, wang.call_count), (4, 2, 2))
+        self.assertEqual(
+            [(Path(call.args[0]).name, call.kwargs["optimized"]) for call in native.call_args_list],
+            [("pipeline_sat.cm13", False), ("pipeline_unsat_search.cm13", False),
+             ("pipeline_sat.cm13", True), ("pipeline_unsat_search.cm13", True)],
+        )
+        rejected = [(region, tiling) for region, tiling, valid in checked if not valid]
+        self.assertEqual(len(rejected), 1)
+        region, altered = rejected[0]
+        original = next(tiling for area, tiling, valid in checked if area == region and valid)
+        changes = [i for i, pair in enumerate(zip(original, altered, strict=True)) if pair[0] != pair[1]]
+        self.assertEqual(len(changes), 1)
+        self.assertTrue(region.active[changes[0]])
+        self.assertIn(altered[changes[0]], range(len(TILESET)))
+        self.assertTrue(actual_check(region, TILESET, original))
+
+    def test_parser_io_failure_is_not_the_expected_domain_rejection(self):
+        actual_load = formula_adapter.load_formula
+
+        def fail_invalid(path):
+            if Path(path).name == "malformed_domain.cm13":
+                raise FormulaLoadError(str(path), FormulaParseStatus.IO_ERROR, 0, 0)
+            return actual_load(path)
+
+        with patch.object(formula_adapter, "load_formula", side_effect=fail_invalid):
+            code, out, err, marker = self.worker()
+        self.assertEqual(code, 1)
+        self.assertIn("IO_ERROR", err)
+        self.assertNotIn("[3/6]", out)
+        self.assertIsNone(marker)
+
+    def test_unknown_disagreement_engine_error_and_invalid_witness_stop_the_suite(self):
+        cases = (
+            (BooleanSolveResult(BooleanSolveStatus.UNKNOWN), "UNKNOWN"),
+            (BooleanSolveResult(BooleanSolveStatus.UNSAT), "atteso SAT"),
+            (RuntimeError("engine failed"), "engine failed"),
+            (BooleanSolveResult(BooleanSolveStatus.SAT, (False, False, False)), "witness"),
+        )
+        for result, message in cases:
+            override = {"side_effect": result} if isinstance(result, Exception) else {"return_value": result}
+            with self.subTest(result=result), patch.object(boolean_solver, "solve_boolean", **override):
+                code, out, err, marker = self.worker()
+            self.assertEqual(code, 1)
+            self.assertIn(message, err)
+            self.assertNotIn("[6/6]", out)
+            self.assertIsNone(marker)
+
+    def test_optimized_disagreement_is_not_hidden_by_reference_success(self):
+        actual_native = witness_pipeline.solve_native_and_extract
+
+        def disagree(path, *, optimized):
+            formula, region, result, assignment = actual_native(path, optimized=optimized)
+            if optimized and Path(path).name == "pipeline_sat.cm13":
+                return formula, region, TilingSolveResult(TilingSolveStatus.UNSAT), None
+            return formula, region, result, assignment
+
+        with patch.object(witness_pipeline, "solve_native_and_extract", side_effect=disagree):
+            code, out, err, marker = self.worker()
+        self.assertEqual(code, 1)
+        self.assertIn("optimized", err)
+        self.assertIn("atteso SAT", err)
+        self.assertNotIn("[6/6]", out)
+        self.assertIsNone(marker)
+
+    def test_checker_accepting_the_altered_witness_is_a_failure(self):
+        with patch.object(tiling_check, "is_valid_tiling", return_value=True):
+            code, out, err, marker = self.worker()
+        self.assertEqual(code, 1)
+        self.assertIn("[6/6]", out)
+        self.assertIn("alterat", err.lower())
+        self.assertIsNone(marker)
+
+    def test_missing_native_dependency_fails_before_checks_with_setup_guidance(self):
+        with patch("native._lib.library", side_effect=OSError("missing library")):
+            code, out, err, marker = self.worker()
+        self.assertEqual(code, 1)
+        self.assertIn("make demo-setup", err)
+        self.assertNotIn("[1/6]", out)
+        self.assertIsNone(marker)
+
+    def test_missing_installed_python_gives_setup_guidance(self):
+        with tempfile.TemporaryDirectory() as name:
+            root = Path(name)
+            with patch.object(self.command, "ROOT", root), contextlib.redirect_stdout(io.StringIO()) as out, contextlib.redirect_stderr(io.StringIO()) as err:
+                code = self.command.main(["--output", str(root / "run")])
+            self.assertEqual(code, 1)
+            self.assertIn("make demo-setup", err.getvalue())
+            self.assertNotIn("Superati 6/6", out.getvalue())
+
+    def test_invalid_timeout_does_not_start_a_worker(self):
+        with patch.object(demo, "_supervise", side_effect=AssertionError("unexpected worker")), contextlib.redirect_stderr(io.StringIO()):
+            for value in ("nan", "inf", "-inf", "0", "-1", "invalid", ""):
+                with self.subTest(timeout=value), self.assertRaises(SystemExit) as stopped:
+                    self.command.main(["--timeout=" + value])
+                self.assertEqual(stopped.exception.code, 2)
+
+    def test_existing_output_is_preserved_without_starting_worker(self):
+        with tempfile.TemporaryDirectory() as name:
+            root = Path(name)
+            (root / "directory").mkdir()
+            (root / "file").write_text("keep")
+            (root / "link").symlink_to(root / "missing")
+            for output in list(root.iterdir()):
+                with self.subTest(output=output), patch.object(demo, "_supervise", side_effect=AssertionError("unexpected worker")), contextlib.redirect_stderr(io.StringIO()):
+                    self.assertEqual(self.command.main(["--output", str(output)]), 1)
+            self.assertEqual((root / "file").read_text(), "keep")
+            self.assertTrue((root / "link").is_symlink())
+            self.assertFalse((root / "missing").exists())
+
+    def test_zero_exit_with_missing_or_wrong_completion_marker_is_failure(self):
+        for marker in (None, b"5/6\n", b"6/6\nextra"):
+            with self.subTest(marker=marker), tempfile.TemporaryDirectory() as name:
+                output = Path(name) / "run"
+
+                def incomplete(*args, **kwargs):
+                    if marker is not None:
+                        (output / "complete").write_bytes(marker)
+                    return 0
+
+                with patch.object(demo, "_supervise", side_effect=incomplete), contextlib.redirect_stdout(io.StringIO()) as out, contextlib.redirect_stderr(io.StringIO()) as err:
+                    code = self.command.main(["--output", str(output)])
+                self.assertEqual(code, 1)
+                self.assertNotIn("Superati 6/6", out.getvalue())
+                self.assertIn("incomplet", err.getvalue())
+
+    def test_parent_prints_duration_only_after_successful_completed_worker(self):
+        with tempfile.TemporaryDirectory() as name:
+            output = Path(name) / "run"
+
+            def complete(*args, **kwargs):
+                (output / "complete").write_bytes(b"6/6\n")
+                return 0
+
+            with patch.object(demo, "_supervise", side_effect=complete) as supervise, contextlib.redirect_stdout(io.StringIO()) as out:
+                code = self.command.main(["--output", str(output), "--timeout", "1.25"])
+            self.assertEqual(code, 0)
+            self.assertRegex(out.getvalue(), r"Superati 6/6 controlli in [0-9]+\.[0-9]+ s")
+            self.assertIn("diagnostics=" + str(output), out.getvalue())
+            command = supervise.call_args.args[0]
+            options = supervise.call_args.kwargs
+            self.assertEqual(command[0], str(ROOT / ".venv/bin/python"))
+            self.assertEqual(options["timeout"], 1.25)
+            self.assertEqual({key: options["env"][key] for key in ("UV_OFFLINE", "UV_NO_SYNC", "UV_PYTHON_DOWNLOADS")}, {"UV_OFFLINE": "1", "UV_NO_SYNC": "1", "UV_PYTHON_DOWNLOADS": "never"})
+
+    def test_worker_exit_codes_cannot_be_masked_by_a_completion_marker(self):
+        for status in (1, 124, 130, 143):
+            with self.subTest(status=status), tempfile.TemporaryDirectory() as name:
+                output = Path(name) / "run"
+
+                def failed(*args, **kwargs):
+                    (output / "complete").write_bytes(b"6/6\n")
+                    return status
+
+                with patch.object(demo, "_supervise", side_effect=failed), contextlib.redirect_stdout(io.StringIO()) as out, contextlib.redirect_stderr(io.StringIO()):
+                    code = self.command.main(["--output", str(output)])
+                self.assertEqual(code, status)
+                self.assertNotIn("Superati 6/6", out.getvalue())
+
+    def test_real_entrypoint_timeout_returns_124_and_keeps_diagnostics(self):
+        with tempfile.TemporaryDirectory() as name:
+            output = Path(name) / "run"
+            completed = subprocess.run(
+                ["python3", "tools/demo_check.py", "--output", str(output), "--timeout", "0.001"],
+                cwd=ROOT, capture_output=True, text=True, timeout=10,
+            )
+            self.assertEqual(completed.returncode, 124, completed.stdout + completed.stderr)
+            self.assertIn("timeout", completed.stderr)
+            self.assertNotIn("Superati 6/6", completed.stdout)
+            self.assertTrue((output / "worker.log").is_file())
+
+    def test_make_passes_raw_timeout_without_evaluating_make_or_shell_code(self):
+        with tempfile.TemporaryDirectory() as name:
+            marker = Path(name) / "expanded"
+            completed = subprocess.run(
+                ["make", "--no-print-directory", "demo-check", "TIMEOUT=$(shell touch " + str(marker) + ")"],
+                cwd=ROOT, capture_output=True, text=True, timeout=10,
+            )
+            self.assertNotEqual(completed.returncode, 0)
+            self.assertIn("finite and positive", completed.stderr)
+            self.assertNotIn("diagnostics=", completed.stdout)
+            self.assertFalse(marker.exists())
+
+    def test_make_defaults_to_300_seconds_for_both_demo_commands(self):
+        # Exercise Make's actual export and each CLI's argparse conversion;
+        # stop only at supervision so this regression needs no PDF generation.
+        with tempfile.TemporaryDirectory() as name:
+            wrapper = Path(name) / "capture_timeout.py"
+            wrapper.write_text(
+                "import importlib, pathlib, sys\n"
+                "sys.path.insert(0, str(pathlib.Path.cwd()))\n"
+                "from tools import demo\n"
+                "entry = pathlib.Path(sys.argv[1]).stem\n"
+                "command = importlib.import_module('tools.' + entry)\n"
+                "def capture(*args, **kwargs):\n"
+                "    print('captured-timeout=' + str(kwargs['timeout']), flush=True)\n"
+                "    return 73\n"
+                "demo._supervise = capture\n"
+                "output = pathlib.Path(__file__).parent / (entry + '-run')\n"
+                "raise SystemExit(command.main(['--output', str(output)]))\n"
+            )
+            environment = os.environ.copy()
+            for key in ("TIMEOUT", "TILING_DEMO_TIMEOUT", "INPUT", "TILING_DEMO_INPUT", "MAKEFLAGS", "MAKEOVERRIDES"):
+                environment.pop(key, None)
+            for target in ("demo", "demo-check"):
+                with self.subTest(target=target):
+                    completed = subprocess.run(
+                        ["make", "--no-print-directory", target,
+                         "INPUT=" + str(ROOT / "tests/instances/pipeline_sat.cm13"),
+                         "PYTHON=" + shlex.join([sys.executable, str(wrapper)])],
+                        cwd=ROOT, env=environment, capture_output=True, text=True, timeout=10,
+                    )
+                    self.assertIn("captured-timeout=300.0", completed.stdout, completed.stdout + completed.stderr)
+                    self.assertIn("Error 73", completed.stderr)
+
+    def test_make_rejects_explicit_empty_timeout_for_both_demo_commands(self):
+        for target in ("demo", "demo-check"):
+            with self.subTest(target=target):
+                completed = subprocess.run(
+                    ["make", "--no-print-directory", target,
+                     "INPUT=" + str(ROOT / "tests/instances/pipeline_sat.cm13"), "TIMEOUT="],
+                    cwd=ROOT, capture_output=True, text=True, timeout=10,
+                )
+                self.assertNotEqual(completed.returncode, 0)
+                self.assertIn("finite and positive", completed.stderr)
+                self.assertNotIn("diagnostics=", completed.stdout)
+
+
+if __name__ == "__main__":
+    unittest.main()
diff --git a/tests/python/test_demo_cli.py b/tests/python/test_demo_cli.py
new file mode 100644
index 0000000..de4340d
--- /dev/null
+++ b/tests/python/test_demo_cli.py
@@ -0,0 +1,176 @@
+from __future__ import annotations
+
+import contextlib
+import hashlib
+import io
+import json
+import os
+from pathlib import Path
+import shutil
+import subprocess
+import sys
+import tempfile
+import unittest
+from unittest.mock import patch
+
+from tools import demo
+
+
+ROOT = Path(__file__).resolve().parents[2]
+SOURCE = ROOT / "tests/instances/pipeline_sat.cm13"
+
+
+class DemoCliTests(unittest.TestCase):
+    def main(self, args):
+        main = getattr(demo, "main", None)
+        self.assertTrue(callable(main), "public demo command is missing")
+        return main(args)
+
+    def worker(self, *args):
+        worker = getattr(demo, "_worker", None)
+        self.assertTrue(callable(worker), "demo worker is missing")
+        return worker(*args)
+
+    def test_invalid_arguments_never_start_a_worker(self):
+        with patch.object(demo, "_supervise", side_effect=AssertionError("unexpected worker")), contextlib.redirect_stderr(io.StringIO()):
+            for timeout in ("nan", "inf", "-inf", "0", "-1", "invalid", ""):
+                with self.subTest(timeout=timeout):
+                    with self.assertRaises(SystemExit) as stopped:
+                        self.main([str(SOURCE), "--timeout=" + timeout])
+                    self.assertEqual(stopped.exception.code, 2)
+            for capacity in ("1", "100001", "2.0"):
+                with self.subTest(capacity=capacity), self.assertRaises(SystemExit):
+                    self.main([str(SOURCE), "--event-capacity", capacity])
+            with patch.dict(os.environ, {}, clear=True), self.assertRaises(SystemExit):
+                self.main([])
+
+    def test_existing_output_entries_are_preserved_without_starting_worker(self):
+        with tempfile.TemporaryDirectory() as name:
+            root = Path(name)
+            (root / "directory").mkdir()
+            (root / "file").write_text("keep")
+            (root / "link").symlink_to(root / "missing")
+            for path in root.iterdir():
+                with self.subTest(path=path), patch.object(demo, "_supervise", side_effect=AssertionError("unexpected worker")), contextlib.redirect_stderr(io.StringIO()):
+                    self.assertNotEqual(self.main([str(SOURCE), "--output", str(path)]), 0)
+            self.assertEqual((root / "file").read_text(), "keep")
+            self.assertTrue((root / "link").is_symlink())
+            self.assertFalse((root / "missing").exists())
+
+    def test_worker_copies_input_and_metadata_before_dependency_failure(self):
+        with tempfile.TemporaryDirectory(prefix="input with spaces ") as name:
+            root = Path(name)
+            source = root / "formula $x `true` ;.cm13"
+            content = SOURCE.read_bytes()
+            source.write_bytes(content)
+            run = root / "run"
+            run.mkdir()
+            actual_which = demo.shutil.which if hasattr(demo, "shutil") else None
+
+            def missing_pdf(command):
+                return None if command == "pdflatex" else actual_which(command)
+
+            self.assertTrue(hasattr(demo, "shutil"), "worker preflight is missing")
+            with patch.object(demo.shutil, "which", side_effect=missing_pdf), contextlib.redirect_stdout(io.StringIO()), contextlib.redirect_stderr(io.StringIO()) as error:
+                code = self.worker(source, run, 100000)
+            self.assertNotEqual(code, 0)
+            self.assertIn("pdflatex", error.getvalue())
+            self.assertIn("dependenc", error.getvalue().lower())
+            self.assertEqual((run / "input.cm13").read_bytes(), content)
+            metadata = json.loads((run / "input.json").read_text())
+            self.assertEqual(metadata["original_path"], str(source))
+            self.assertEqual(metadata["original_name"], source.name)
+            self.assertEqual(metadata["sha256"], hashlib.sha256(content).hexdigest())
+            self.assertFalse((run / "dossier").exists())
+
+    def test_zero_exit_without_complete_files_is_failure_and_no_success_is_printed(self):
+        with tempfile.TemporaryDirectory() as name:
+            output = Path(name) / "run"
+            with patch.object(demo, "_supervise", return_value=0), contextlib.redirect_stdout(io.StringIO()) as stdout, contextlib.redirect_stderr(io.StringIO()):
+                code = self.main([str(SOURCE), "--output", str(output)])
+            self.assertNotEqual(code, 0)
+            self.assertNotIn("dossier=", stdout.getvalue())
+            self.assertTrue(output.is_dir())
+
+    def test_demo_invocations_have_distinct_diagnostic_directories(self):
+        with tempfile.TemporaryDirectory() as name:
+            root = Path(name)
+            (root / ".venv/bin").mkdir(parents=True)
+            (root / ".venv/bin/python").symlink_to(sys.executable)
+            with patch.object(demo, "ROOT", root), patch.object(demo, "_supervise", return_value=1), contextlib.redirect_stdout(io.StringIO()), contextlib.redirect_stderr(io.StringIO()):
+                self.assertEqual(self.main([str(SOURCE)]), 1)
+                self.assertEqual(self.main([str(SOURCE)]), 1)
+            self.assertEqual(len(list((root / "build/demo").iterdir())), 2)
+
+    def test_worker_command_uses_installed_python_and_disables_downloads(self):
+        with tempfile.TemporaryDirectory() as name:
+            output = Path(name) / "run"
+            with patch.object(demo, "_supervise", return_value=124) as supervise, contextlib.redirect_stdout(io.StringIO()), contextlib.redirect_stderr(io.StringIO()):
+                code = self.main([str(SOURCE), "--output", str(output), "--timeout", "1.25", "--event-capacity", "2000"])
+            self.assertEqual(code, 124)
+            call = supervise.call_args
+            self.assertEqual(call.args[0][0], str(ROOT / ".venv/bin/python"))
+            self.assertIn(str(SOURCE), call.args[0])
+            self.assertEqual(call.kwargs["timeout"], 1.25)
+            self.assertEqual({key: call.kwargs["env"][key] for key in ("UV_OFFLINE", "UV_NO_SYNC", "UV_PYTHON_DOWNLOADS")}, {"UV_OFFLINE": "1", "UV_NO_SYNC": "1", "UV_PYTHON_DOWNLOADS": "never"})
+
+    def test_worker_preserves_malformed_input_diagnostics_after_preflight(self):
+        with tempfile.TemporaryDirectory() as name:
+            root = Path(name)
+            source = root / "malformed.cm13"
+            source.write_bytes(b"p cm13 invalid\n")
+            run = root / "run"
+            run.mkdir()
+            # Parsing does not require the optional renderer or TeX installation.
+            with patch.object(demo, "_preflight"), contextlib.redirect_stdout(io.StringIO()), contextlib.redirect_stderr(io.StringIO()) as error:
+                code = self.worker(source, run, 100000)
+            self.assertNotEqual(code, 0)
+            self.assertIn("malformed input", error.getvalue().lower())
+            self.assertEqual((run / "input.cm13").read_bytes(), source.read_bytes())
+            self.assertEqual(json.loads((run / "input.json").read_text())["original_path"], str(source))
+            self.assertFalse((run / "dossier").exists())
+
+    def test_make_passes_raw_metacharacters_and_preserves_dependency_diagnostics(self):
+        with tempfile.TemporaryDirectory(prefix="make demo input ") as name:
+            root = Path(name)
+            # Exercise the same failure on hosts with and without demo setup.
+            # Keep touch available so accidental Make/shell expansion is detected.
+            commands = root / "bin"
+            commands.mkdir()
+            for command in ("make", "find", "touch", "git", "uv"):
+                executable = shutil.which(command)
+                self.assertIsNotNone(executable, command)
+                (commands / command).symlink_to(executable)
+            (commands / "python3").symlink_to(sys.executable)
+            environment = dict(os.environ, PATH=str(commands))
+            marker = ROOT / ("demo-expanded-" + root.name.replace(" ", "-"))
+            source = root / ("literal $(shell touch " + marker.name + ") $x `true`; #.cm13")
+            source.write_bytes(b"p cm13 invalid\n")
+            completed = subprocess.run(
+                ["make", "--no-print-directory", "demo", "INPUT=" + str(source), "TIMEOUT=20"],
+                cwd=ROOT, env=environment, capture_output=True, text=True, timeout=30,
+            )
+            self.assertNotEqual(completed.returncode, 0)
+            self.assertIn("missing dependency: pdflatex", completed.stdout + completed.stderr)
+            diagnostic = next((line.removeprefix("diagnostics=") for line in completed.stdout.splitlines() if line.startswith("diagnostics=")), None)
+            self.assertIsNotNone(diagnostic, completed.stdout + completed.stderr)
+            run = Path(diagnostic)
+            self.assertEqual((run / "input.cm13").read_bytes(), source.read_bytes())
+            self.assertEqual(json.loads((run / "input.json").read_text())["original_path"], str(source))
+            self.assertIn("missing dependency: pdflatex", (run / "worker.log").read_text())
+            self.assertFalse((run / "dossier").exists())
+            self.assertNotIn("dossier=", completed.stdout)
+            self.assertFalse(marker.exists())
+            invalid_timeout = subprocess.run(
+                ["make", "--no-print-directory", "demo", "INPUT=" + str(source),
+                 "TIMEOUT=$(shell touch " + marker.name + ")"],
+                cwd=ROOT, env=environment, capture_output=True, text=True, timeout=10,
+            )
+            self.assertNotEqual(invalid_timeout.returncode, 0)
+            self.assertIn("finite and positive", invalid_timeout.stderr)
+            self.assertNotIn("diagnostics=", invalid_timeout.stdout)
+            self.assertFalse(marker.exists())
+
+
+if __name__ == "__main__":
+    unittest.main()
diff --git a/tests/python/test_demo_processes.py b/tests/python/test_demo_processes.py
new file mode 100644
index 0000000..b84bb3c
--- /dev/null
+++ b/tests/python/test_demo_processes.py
@@ -0,0 +1,166 @@
+from __future__ import annotations
+
+import importlib.util
+import os
+from pathlib import Path
+import signal
+import subprocess
+import sys
+import tempfile
+import time
+import unittest
+
+
+ROOT = Path(__file__).resolve().parents[2]
+FIXTURE = ROOT / "tests/fixtures/demo_process.py"
+HARNESS = """
+import os, pathlib, sys, time
+from tools import demo
+root = pathlib.Path(sys.argv[1])
+if sys.argv[4] == 'backpressure':
+    # Fill both pipes before supervision, then leave their readers idle.
+    for stream in (sys.stdout, sys.stderr):
+        fd = stream.fileno()
+        os.set_blocking(fd, False)
+        try:
+            while True:
+                os.write(fd, b'P' * 4096)
+        except BlockingIOError:
+            pass
+        finally:
+            os.set_blocking(fd, True)
+if sys.argv[4] == 'broken-output':
+    class BrokenOutput:
+        def write(self, data):
+            raise OSError('terminal disappeared')
+        def flush(self):
+            pass
+    sys.stdout = BrokenOutput()
+try:
+    result = demo._supervise(
+        [sys.executable, sys.argv[2], sys.argv[3], str(root)],
+        cwd=pathlib.Path.cwd(), env=os.environ.copy(),
+        log_path=root / 'worker.log', timeout=float(sys.argv[5]),
+    )
+except OSError as error:
+    print(str(error), file=sys.stderr)
+    result = 1
+sys.exit(result)
+"""
+
+
+def live(pid):
+    try:
+        # Linux stat comm may contain spaces and parentheses.
+        state = Path(f"/proc/{pid}/stat").read_bytes().rsplit(b")", 1)[1].split()[0]
+        return state not in (b"Z", b"X")
+    except FileNotFoundError:
+        return False
+
+
+class DemoProcessTests(unittest.TestCase):
+    def setUp(self):
+        self.assertIsNotNone(importlib.util.find_spec("tools.demo"), "demo supervisor is missing")
+
+    def run_tree(self, mode, *, timeout=1.5, signals=(), broken=False, undrained=False):
+        with tempfile.TemporaryDirectory() as name:
+            root = Path(name)
+            started = time.monotonic()
+            process = subprocess.Popen(
+                [sys.executable, "-c", HARNESS, str(root), str(FIXTURE), mode,
+                 "backpressure" if undrained else "broken-output" if broken else "output", str(timeout)],
+                cwd=ROOT, stdout=subprocess.PIPE, stderr=subprocess.PIPE, text=True,
+                start_new_session=True,
+            )
+            try:
+                if mode != "normal":
+                    deadline = time.monotonic() + 8
+                    while not (root / "ready").exists():
+                        if process.poll() is not None or time.monotonic() >= deadline:
+                            stdout, stderr = process.communicate(timeout=3)
+                            self.fail(f"fixture did not become ready: {stdout} {stderr}")
+                        time.sleep(0.01)
+                    if mode.startswith("leader"):
+                        (root / "release").touch()
+                    for item in signals:
+                        process.send_signal(item)
+                        time.sleep(0.05)
+                if undrained:
+                    try:
+                        process.wait(timeout=4)
+                    except subprocess.TimeoutExpired:
+                        self.fail("supervisor blocked on undrained output instead of stopping its group")
+                stdout, stderr = process.communicate(timeout=10)
+                self.assertLess(time.monotonic() - started, 10)
+                for pid_file in root.glob("*.pid"):
+                    self.assertFalse(live(int(pid_file.read_text())), pid_file.name)
+                log = (root / "worker.log").read_bytes()
+                self.assertNotIn("dossier=", stdout)
+                return process.returncode, stdout, stderr, log
+            finally:
+                worker_pid = root / "worker.pid"
+                if worker_pid.exists():
+                    try:
+                        os.killpg(int(worker_pid.read_text()), signal.SIGKILL)
+                    except ProcessLookupError:
+                        pass
+                if process.poll() is None:
+                    os.killpg(process.pid, signal.SIGKILL)
+                process.communicate(timeout=3)
+
+    def test_normal_worker_is_reaped_and_output_is_logged_and_forwarded(self):
+        code, stdout, _, log = self.run_tree("normal")
+        self.assertEqual(code, 0)
+        self.assertIn("normal worker output", stdout)
+        self.assertIn(b"normal worker output", log)
+
+    def test_timeout_stops_child_and_grandchild_which_ignore_term(self):
+        code, stdout, stderr, log = self.run_tree("tree")
+        self.assertEqual(code, 124, stderr)
+        self.assertIn("timeout", (stdout + stderr).lower())
+        self.assertIn(b"partial output without newline", log)
+
+    def test_process_names_with_non_utf8_bytes_do_not_break_group_cleanup(self):
+        code, _, stderr, _ = self.run_tree("unusual-name")
+        self.assertEqual(code, 124, stderr)
+
+    def test_dead_leader_does_not_orphan_children_or_block_on_inherited_output(self):
+        for mode in ("leader0", "leader7"):
+            with self.subTest(mode=mode):
+                code, _, _, log = self.run_tree(mode, timeout=8)
+                self.assertNotEqual(code, 0)
+                self.assertNotEqual(code, 124)
+                self.assertIn(b"partial output", log)
+
+    def test_repeated_cancellation_signals_do_not_interrupt_group_cleanup(self):
+        for first in (signal.SIGINT, signal.SIGTERM):
+            with self.subTest(signal=first):
+                code, stdout, stderr, _ = self.run_tree("tree", timeout=8, signals=(first, signal.SIGTERM, signal.SIGINT))
+                self.assertEqual(code, 128 + first, stderr)
+                self.assertIn("cancel", (stdout + stderr).lower())
+
+    def test_verbose_partial_output_cannot_postpone_global_timeout(self):
+        code, stdout, _, log = self.run_tree("verbose")
+        self.assertEqual(code, 124)
+        self.assertGreater(len(log), 100000)
+        self.assertLess(len(stdout), 2_000_000)
+
+    def test_full_stdout_and_stderr_pipes_cannot_block_timeout_or_cancellation(self):
+        for signals in ((), (signal.SIGTERM, signal.SIGINT)):
+            with self.subTest(signals=signals):
+                code, _, _, log = self.run_tree(
+                    "verbose", timeout=8 if signals else 0.4,
+                    signals=signals, undrained=True,
+                )
+                self.assertEqual(code, 143 if signals else 124)
+                self.assertIn(b"partial output without newline", log)
+
+    def test_parent_output_exception_still_cleans_the_entire_group(self):
+        code, _, stderr, log = self.run_tree("tree", timeout=8, broken=True)
+        self.assertEqual(code, 1)
+        self.assertIn("terminal disappeared", stderr)
+        self.assertIn(b"partial output", log)
+
+
+if __name__ == "__main__":
+    unittest.main()
diff --git a/tests/python/test_multi_engine_dossier.py b/tests/python/test_multi_engine_dossier.py
index 758a315..f9bf9b4 100644
--- a/tests/python/test_multi_engine_dossier.py
+++ b/tests/python/test_multi_engine_dossier.py
@@ -2,6 +2,7 @@
 
 import copy
 from datetime import datetime, timezone
+import hashlib
 import json
 import os
 from pathlib import Path
@@ -107,6 +108,30 @@ def test_wide_figure_keeps_its_caption_on_the_image_page(self) -> None:
         self.assertEqual(image_pages, caption_pages)
 
 
+class NullableCaseContractTests(unittest.TestCase):
+    def test_case_requires_an_explicit_nullable_terminal_expectation(self) -> None:
+        original = json.loads(SAT_CASE.read_text(encoding="utf-8"))
+        with tempfile.TemporaryDirectory() as name:
+            path = Path(name) / "case.json"
+            for value in (None, "sat", "unsat"):
+                with self.subTest(value=value):
+                    case = {**original, "expected_status": value}
+                    path.write_text(json.dumps(case), encoding="utf-8")
+                    self.assertEqual(load_run_case_v2(path, ROOT).expected_status, value)
+            for value in ("unknown", "", False, 0, [], {}):
+                with self.subTest(invalid=value):
+                    path.write_text(json.dumps({**original, "expected_status": value}), encoding="utf-8")
+                    with self.assertRaises(PipelineSnapshotError):
+                        load_run_case_v2(path, ROOT)
+            for case in (
+                {key: value for key, value in original.items() if key != "expected_status"},
+                {**original, "expected_status": None, "observed_status": "sat"},
+            ):
+                path.write_text(json.dumps(case), encoding="utf-8")
+                with self.assertRaises(PipelineSnapshotError):
+                    load_run_case_v2(path, ROOT)
+
+
 class MultiEngineDossierTests(unittest.TestCase):
     @classmethod
     def setUpClass(cls) -> None:
@@ -129,6 +154,210 @@ def setUpClass(cls) -> None:
     def tearDownClass(cls) -> None:
         cls.temporary.cleanup()
 
+    def test_absent_expectation_preserves_observed_sat_and_unsat(self) -> None:
+        for case_path, status in ((SAT_CASE, "sat"), (UNSAT_CASE, "unsat")):
+            with self.subTest(status=status):
+                case = json.loads(case_path.read_text(encoding="utf-8"))
+                case["expected_status"] = None
+                nullable_case = self.root / f"nullable-{status}.json"
+                nullable_case.write_text(json.dumps(case), encoding="utf-8")
+                self.assertIsNone(load_run_case_v2(nullable_case, ROOT).expected_status)
+                destination = self.root / f"nullable-{status}"
+                multi_engine.generate_multi_engine_dossier(nullable_case, destination)
+                run = load_run_dossier_v2(destination / "run.json")
+                self.assertIsNone(run["case"]["expected_status"])
+                self.assertIsNone(run["agreement"]["expected_status"])
+                self.assertEqual(run["reference"]["status"], status)
+                self.assertIs(run["presentation"]["square"]["applicable"], status == "sat")
+                self.assertIs(run["agreement"]["sat_witnesses_valid"], True if status == "sat" else None)
+                manifest_path = destination / "assets/narrative/manifest.json"
+                manifest = load_narrative_assets(manifest_path, run)
+                self.assertEqual(manifest["case"], {
+                    "id": case["id"], "expected_status": None,
+                    "observed_status": status, "source_sha256": run["source"]["sha256"],
+                })
+                tex = render_run_report_v2_tex(run, manifest, V2_TEMPLATE.read_text(encoding="utf-8"))
+                self.assertIn(f"Terminal status & {status.upper()}", tex)
+                self.assertIn("Expected result: not supplied", tex)
+                for field, value in (("observed_status", None), ("observed_status", "unsat" if status == "sat" else "sat"), ("expected_status", status)):
+                    changed = copy.deepcopy(manifest)
+                    if value is None:
+                        del changed["case"][field]
+                    else:
+                        changed["case"][field] = value
+                    manifest_path.write_text(json.dumps(changed), encoding="utf-8")
+                    with self.assertRaises(PipelineSnapshotError):
+                        load_narrative_assets(manifest_path, run)
+                changed = copy.deepcopy(manifest)
+                changed["case"]["expected_status"] = status
+                del changed["case"]["observed_status"]
+                manifest_path.write_text(json.dumps(changed), encoding="utf-8")
+                with self.assertRaisesRegex(PipelineSnapshotError, "case identity"):
+                    load_narrative_assets(manifest_path, run)
+                manifest_path.write_text(json.dumps(manifest), encoding="utf-8")
+
+    def test_nullable_contract_rejects_nonterminal_disagreement_and_forged_checks(self) -> None:
+        for original in (self.sat_document, self.unsat_document):
+            run = copy.deepcopy(original)
+            run["case"]["expected_status"] = None
+            run["agreement"]["expected_status"] = None
+            validate_run_dossier_v2(run)
+            for value in ("unknown", "", False, 0, [], {}):
+                changed = copy.deepcopy(run)
+                changed["case"]["expected_status"] = value
+                with self.assertRaises(PipelineSnapshotError):
+                    validate_run_dossier_v2(changed)
+            changed = copy.deepcopy(run)
+            del changed["case"]["expected_status"]
+            with self.assertRaises(PipelineSnapshotError):
+                validate_run_dossier_v2(changed)
+            mutations = [
+                ("agreement", "reference_status", "unknown"),
+                ("agreement", "optimized_status", "unknown"),
+                ("agreement", "boolean_z3_status", "unknown"),
+                ("agreement", "wang_z3_status", "unknown"),
+                ("agreement", "expected_status", original["reference"]["status"]),
+                ("wang_z3", "status", "unknown"),
+            ]
+            for section, field, value in mutations:
+                with self.subTest(section=section, field=field):
+                    changed = copy.deepcopy(run)
+                    changed[section][field] = value
+                    with self.assertRaises(PipelineSnapshotError):
+                        validate_run_dossier_v2(changed)
+            for check in run["verification"]:
+                changed = copy.deepcopy(run)
+                changed["verification"][check]["performed"] = original["reference"]["status"] != "sat"
+                with self.assertRaises(PipelineSnapshotError):
+                    validate_run_dossier_v2(changed)
+            for solver in ("reference", "optimized"):
+                changed = copy.deepcopy(run)
+                changed["artifacts"][f"{solver}_solution"] = (
+                    None if original["reference"]["status"] == "sat"
+                    else self.sat_document["artifacts"][f"{solver}_solution"]
+                )
+                with self.assertRaises(PipelineSnapshotError):
+                    validate_run_dossier_v2(changed)
+            changed = copy.deepcopy(run)
+            changed["reference"]["trace"]["complete"] = False
+            with self.assertRaisesRegex(PipelineSnapshotError, "complete trace"):
+                validate_run_dossier_v2(changed)
+            changed = copy.deepcopy(run)
+            changed["case"]["expected_status"] = "unsat" if original["reference"]["status"] == "sat" else "sat"
+            with self.assertRaisesRegex(PipelineSnapshotError, "known expected status mismatch"):
+                validate_run_dossier_v2(changed)
+        mismatch = copy.deepcopy(self.sat_document)
+        mismatch["case"]["expected_status"] = None
+        mismatch["agreement"]["expected_status"] = None
+        mismatch["wang_z3"].update(status="unsat", cells=None, witness_sha256=None)
+        with self.assertRaisesRegex(PipelineSnapshotError, "engine status mismatch"):
+            validate_run_dossier_v2(mismatch)
+
+    def _bare_bundle(self, name: str, *, sat: bool = False) -> tuple[Path, dict]:
+        source = self.sat_directory if sat else self.unsat_directory
+        destination = self.root / name
+        shutil.copytree(source / "assets/data", destination / "assets/data")
+        run = copy.deepcopy(self.sat_document if sat else self.unsat_document)
+        for solver in ("reference", "optimized"):
+            run[solver]["trace"]["selection"] = {"performed": False, "selected_event_count": None}
+        for view in ("square", "generalized", "hex"):
+            run["presentation"][view]["artifact"] = None
+            run["artifacts"][f"{view}_presentation"] = None
+        return destination, run
+
+    def _rewrite_bundle_artifact(self, directory: Path, run: dict, name: str, document: dict) -> str:
+        path = directory / run["artifacts"][name]["path"]
+        encoded = (json.dumps(document, indent=2) + "\n").encode("utf-8")
+        path.write_bytes(encoded)
+        digest = hashlib.sha256(encoded).hexdigest()
+        run["artifacts"][name]["sha256"] = digest
+        return digest
+
+    def test_bundle_rejects_rehashed_z3_status_disagreement(self) -> None:
+        for engine in ("boolean_z3", "wang_z3"):
+            with self.subTest(engine=engine):
+                directory, run = self._bare_bundle(f"summary-status-{engine}")
+                name = f"{engine}_summary"
+                summary = json.loads((directory / run["artifacts"][name]["path"]).read_text())
+                summary["status"] = "unknown"
+                run[engine]["encoding_summary_sha256"] = self._rewrite_bundle_artifact(directory, run, name, summary)
+                (directory / "run.json").write_text(json.dumps(run), encoding="utf-8")
+                with self.assertRaisesRegex(PipelineSnapshotError, "summary status.*run"):
+                    load_run_dossier_v2(directory / "run.json")
+
+    def test_bundle_rejects_rehashed_native_source_disagreement(self) -> None:
+        directory, run = self._bare_bundle("native-source")
+        source = directory / run["artifacts"]["source_input"]["path"]
+        source.write_bytes(source.read_bytes() + b"\n")
+        digest = hashlib.sha256(source.read_bytes()).hexdigest()
+        run["source"]["sha256"] = digest
+        run["artifacts"]["source_input"]["sha256"] = digest
+        for artifact in run["artifacts"].values():
+            if artifact is not None:
+                artifact["source_sha256"] = digest
+        for engine in ("boolean_z3", "wang_z3"):
+            name = f"{engine}_summary"
+            summary = json.loads((directory / run["artifacts"][name]["path"]).read_text())
+            summary["source_formula_sha256"] = digest
+            run[engine]["encoding_summary_sha256"] = self._rewrite_bundle_artifact(directory, run, name, summary)
+        (directory / "run.json").write_text(json.dumps(run), encoding="utf-8")
+        with self.assertRaisesRegex(PipelineSnapshotError, "native source.*run"):
+            load_run_dossier_v2(directory / "run.json")
+
+    def test_bundle_rejects_rehashed_incomplete_native_trace(self) -> None:
+        for solver in ("reference", "optimized"):
+            with self.subTest(solver=solver):
+                directory, run = self._bare_bundle(f"incomplete-{solver}")
+                name = f"{solver}_trace"
+                trace = json.loads((directory / run["artifacts"][name]["path"]).read_text())
+                trace["events"] = [trace["events"][0], trace["events"][-1]]
+                trace["checkpoints"] = []
+                trace["capacity"].update(truncated=True, checkpoint_interval=0, checkpoint_capacity=0, checkpoints_truncated=False)
+                digest = self._rewrite_bundle_artifact(directory, run, name, trace)
+                run[solver]["trace"]["trace_sha256"] = digest
+                name = f"{solver}_trace_manifest"
+                manifest = json.loads((directory / run["artifacts"][name]["path"]).read_text())
+                manifest["artifacts"]["trace"]["sha256"] = digest
+                run[solver]["trace"]["manifest_sha256"] = self._rewrite_bundle_artifact(directory, run, name, manifest)
+                (directory / "run.json").write_text(json.dumps(run), encoding="utf-8")
+                with self.assertRaisesRegex(PipelineSnapshotError, "trace completeness.*run"):
+                    load_run_dossier_v2(directory / "run.json")
+
+    def test_bundle_binds_native_trace_status_and_solver(self) -> None:
+        for solver in ("reference", "optimized"):
+            for field in ("status", "solver"):
+                with self.subTest(solver=solver, field=field):
+                    directory, run = self._bare_bundle(f"trace-{solver}-{field}", sat=True)
+                    trace_name = f"{solver}_trace"
+                    trace_path = directory / run["artifacts"][trace_name]["path"]
+                    trace = json.loads(trace_path.read_text(encoding="utf-8"))
+                    manifest_name = f"{solver}_trace_manifest"
+                    manifest_path = directory / run["artifacts"][manifest_name]["path"]
+                    manifest = json.loads(manifest_path.read_text(encoding="utf-8"))
+                    if field == "status":
+                        trace["status"] = "unsat"
+                        trace["events"][-1]["status"] = "unsat"
+                        # UNSAT result events require an active cell. Keep the
+                        # altered trace structurally valid so this probes its
+                        # status binding to the run, beyond semantic replay.
+                        trace["events"][-1]["cell"] = next(
+                            cell for cell, domain in enumerate(trace["initial_domains"])
+                            if domain != 0
+                        )
+                        trace["solution_sha256"] = None
+                        manifest["artifacts"]["solution"] = None
+                    else:
+                        trace["solver"] = "optimized" if solver == "reference" else "reference"
+                    digest = self._rewrite_bundle_artifact(directory, run, trace_name, trace)
+                    run[solver]["trace"]["trace_sha256"] = digest
+                    manifest["artifacts"]["trace"]["sha256"] = digest
+                    run[solver]["trace"]["manifest_sha256"] = self._rewrite_bundle_artifact(
+                        directory, run, manifest_name, manifest,
+                    )
+                    (directory / "run.json").write_text(json.dumps(run), encoding="utf-8")
+                    with self.assertRaisesRegex(PipelineSnapshotError, f"trace {field}.*run"):
+                        load_run_dossier_v2(directory / "run.json")
+
     def test_native_coordinator_runs_each_solver_once_in_one_capture(self) -> None:
         case = load_run_case_v2(SAT_CASE, ROOT)
         reference = TraceCaptureOptions(
diff --git a/tools/demo.py b/tools/demo.py
new file mode 100644
index 0000000..4d96abb
--- /dev/null
+++ b/tools/demo.py
@@ -0,0 +1,322 @@
+#!/usr/bin/env python3
+"""Run a CM1-in-3 input through the verified PDF pipeline under one deadline."""
+
+from __future__ import annotations
+
+import argparse
+import hashlib
+import io
+import json
+import math
+import os
+from pathlib import Path
+import shutil
+import signal
+import subprocess
+import sys
+import tempfile
+import time
+
+
+ROOT = Path(__file__).resolve().parents[1]
+
+
+class DemoError(RuntimeError):
+    """A demo prerequisite or complete-output check failed."""
+
+
+def _group_alive(pgid: int) -> bool:
+    """Inspect Linux group members, excluding zombies that only a parent can reap."""
+    try:
+        os.killpg(pgid, 0)
+    except ProcessLookupError:
+        return False
+    for process in Path("/proc").iterdir():
+        if not process.name.isdecimal():
+            continue
+        try:
+            fields = (process / "stat").read_bytes().rsplit(b")", 1)[1].split()
+        except (FileNotFoundError, ProcessLookupError):
+            continue
+        if int(fields[2]) == pgid and fields[0] not in (b"Z", b"X"):
+            return True
+    return False
+
+
+def _stop_group(worker: subprocess.Popen, pgid: int) -> None:
+    # The leader may already have exited. Its saved PGID still owns the children.
+    for sig in (signal.SIGTERM, signal.SIGKILL):
+        try:
+            os.killpg(pgid, sig)
+        except ProcessLookupError:
+            break
+        deadline = time.monotonic() + 0.5
+        while time.monotonic() < deadline:
+            worker.poll()
+            if not _group_alive(pgid):
+                break
+            time.sleep(0.02)
+        if not _group_alive(pgid):
+            break
+    worker.wait(timeout=1)
+    if _group_alive(pgid):
+        raise RuntimeError("demo worker group still has live processes after SIGKILL")
+
+
+def _emit(message: str, *, stream=None) -> None:
+    """Best-effort console output: a stalled consumer cannot delay cleanup.
+
+    Use one nonblocking descriptor write with no Python output buffer. A partial
+    write or EAGAIN drops only the console copy; worker.log retains every byte.
+    In-memory streams used by callers/tests have no descriptor or backpressure.
+    """
+    stream = sys.stdout if stream is None else stream
+    try:
+        descriptor = stream.fileno()
+    except (AttributeError, io.UnsupportedOperation):
+        stream.write(message)
+        stream.flush()
+        return
+    blocking = os.get_blocking(descriptor)
+    try:
+        os.set_blocking(descriptor, False)
+        try:
+            os.write(descriptor, message.encode("utf-8", errors="replace"))
+        except BlockingIOError:
+            pass
+    finally:
+        os.set_blocking(descriptor, blocking)
+
+
+def _forward_log(reader, limit: int = 8192) -> None:
+    data = reader.read(limit)
+    if data:
+        _emit(data.decode("utf-8", errors="replace"))
+
+
+def _supervise(
+    command: list[str],
+    *,
+    cwd: Path,
+    env: dict[str, str],
+    log_path: Path,
+    timeout: float,
+) -> int:
+    """Supervise the fixed worker/toolchain group; retain merged regular-file logs."""
+    deadline = time.monotonic() + timeout
+    pending_signal = 0
+    worker = None
+    pgid = None
+    outcome = 1
+
+    def cancelled(signum, _frame):
+        nonlocal pending_signal
+        if not pending_signal:
+            pending_signal = signum
+
+    previous = {}
+    try:
+        for sig in (signal.SIGINT, signal.SIGTERM):
+            previous[sig] = signal.signal(sig, cancelled)
+        with log_path.open("xb", buffering=0) as log, log_path.open("rb", buffering=0) as reader:
+            worker = subprocess.Popen(
+                command, cwd=cwd, env=env, stdin=subprocess.DEVNULL,
+                stdout=log, stderr=subprocess.STDOUT, start_new_session=True,
+            )
+            pgid = worker.pid
+            while True:
+                if pending_signal:
+                    _emit(f"demo: cancelled by {signal.Signals(pending_signal).name}\n", stream=sys.stderr)
+                    outcome = 128 + pending_signal
+                    break
+                if time.monotonic() >= deadline:
+                    _emit(f"demo: global timeout after {timeout:g} seconds\n", stream=sys.stderr)
+                    outcome = 124
+                    break
+                _forward_log(reader)
+                result = worker.poll()
+                if result is not None:
+                    _forward_log(reader, 65536)
+                    if _group_alive(pgid):
+                        _emit("demo: worker exited with live child processes\n", stream=sys.stderr)
+                        outcome = 1
+                    else:
+                        outcome = result if result >= 0 else 128 - result
+                    break
+                time.sleep(0.02)
+    finally:
+        try:
+            if worker is not None and pgid is not None:
+                _stop_group(worker, pgid)
+        finally:
+            for sig, handler in previous.items():
+                signal.signal(sig, handler)
+    return 128 + pending_signal if pending_signal and outcome == 0 else outcome
+
+
+def _preflight() -> None:
+    """Check installed prerequisites without building, syncing or downloading."""
+    for command in ("uv", "git", "pdflatex"):
+        if shutil.which(command) is None:
+            raise DemoError(f"missing dependency: {command}; run make demo-setup")
+    renderer_python = ROOT / "renderer/.venv/bin/python"
+    if not renderer_python.is_file():
+        raise DemoError("missing renderer environment; run make demo-setup")
+    try:
+        import z3
+        from native._lib import library
+
+        library()
+        z3.get_version_string()
+        subprocess.run(
+            [str(renderer_python), "-c", (
+                "import numpy; from PIL import Image; "
+                "from wang_explain import explain_font; explain_font(14)"
+            )],
+            cwd=ROOT / "renderer", check=True, capture_output=True, text=True,
+            timeout=30,
+        )
+    except (ImportError, OSError, subprocess.SubprocessError) as error:
+        raise DemoError(
+            f"installed dependency check failed: {error}; run make demo-setup"
+        ) from error
+
+
+def _worker(input_path: Path, run_root: Path, event_capacity: int) -> int:
+    try:
+        content = input_path.read_bytes()
+        source_copy = run_root / "input.cm13"
+        with source_copy.open("xb") as target:
+            target.write(content)
+        source_copy.chmod(0o444)
+        metadata = {
+            "original_path": str(input_path),
+            "original_name": input_path.name,
+            "sha256": hashlib.sha256(content).hexdigest(),
+        }
+        with (run_root / "input.json").open("x", encoding="utf-8") as target:
+            json.dump(metadata, target, ensure_ascii=True, indent=2)
+            target.write("\n")
+        print("input=" + json.dumps(metadata, ensure_ascii=True), flush=True)
+        print("Preflight", flush=True)
+        sys.path.insert(0, str(ROOT / "python"))
+        _preflight()
+        from dossier.multi_engine import generate_input_dossier
+        from formats.run_dossier_v2_bundle import load_run_dossier_v2
+        from native.formula_adapter import FormulaLoadError
+
+        try:
+            destination = generate_input_dossier(
+                source_copy, run_root / "dossier", include_pdf=True,
+                event_capacity=event_capacity,
+                progress=lambda label: print(label, flush=True),
+            )
+        except FormulaLoadError as error:
+            raise DemoError(f"malformed input or parser failure: {error}") from error
+        run = load_run_dossier_v2(destination / "run.json")
+        print(f"Verified result: {run['reference']['status'].upper()}", flush=True)
+        return 0
+    except Exception as error:
+        print(f"demo worker: {type(error).__name__}: {error}", file=sys.stderr, flush=True)
+        return 1
+
+
+def _positive_timeout(value: str) -> float:
+    try:
+        seconds = float(value)
+    except ValueError as error:
+        raise argparse.ArgumentTypeError("timeout must be finite and positive") from error
+    if not math.isfinite(seconds) or seconds <= 0:
+        raise argparse.ArgumentTypeError("timeout must be finite and positive")
+    return seconds
+
+
+def _event_capacity(value: str) -> int:
+    try:
+        capacity = int(value)
+    except ValueError as error:
+        raise argparse.ArgumentTypeError("event capacity must be an integer in [2, 100000]") from error
+    if not 2 <= capacity <= 100_000:
+        raise argparse.ArgumentTypeError("event capacity must be an integer in [2, 100000]")
+    return capacity
+
+
+def _new_run(output: Path | None) -> Path:
+    if output is not None:
+        run = output.absolute()
+        try:
+            run.mkdir(parents=True)
+        except FileExistsError as error:
+            raise DemoError(f"output already exists: {run}") from error
+        return run
+    directory = ROOT / "build/demo"
+    directory.mkdir(parents=True, exist_ok=True)
+    return Path(tempfile.mkdtemp(prefix="run-", dir=directory))
+
+
+def _check_complete_output(run_root: Path) -> Path:
+    dossier = run_root / "dossier"
+    for name in ("run.json", "report.tex", "report.pdf", "assets/narrative/manifest.json"):
+        path = dossier / name
+        if not path.is_file() or path.stat().st_size == 0:
+            raise DemoError(f"worker did not produce a complete dossier: missing {name}")
+    with (dossier / "report.pdf").open("rb") as pdf:
+        if pdf.read(5) != b"%PDF-":
+            raise DemoError("worker did not produce a valid PDF header")
+    return dossier
+
+
+def main(arguments: list[str] | None = None) -> int:
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument(
+        "input", nargs="?", default=os.environ.get("TILING_DEMO_INPUT"),
+        help="new CM1-in-3 file",
+    )
+    parser.add_argument(
+        "--output", type=Path,
+        help="new diagnostic run directory (default: unique directory in build/demo)",
+    )
+    parser.add_argument(
+        "--timeout", type=_positive_timeout,
+        default=os.environ.get("TILING_DEMO_TIMEOUT", "300"),
+        help="global timeout in seconds (default: 300)",
+    )
+    parser.add_argument(
+        "--event-capacity", type=_event_capacity, default=100_000,
+        help="maximum events per native trace, 2..100000 (default: 100000)",
+    )
+    args = parser.parse_args(arguments)
+    if not args.input:
+        parser.error("an input file is required: make demo INPUT=path.cm13")
+    if not sys.platform.startswith("linux"):
+        parser.error("the demo currently supports Linux")
+    try:
+        run_root = _new_run(args.output)
+        _emit(f"diagnostics={run_root}\n")
+        environment = os.environ.copy()
+        environment.update(UV_OFFLINE="1", UV_NO_SYNC="1", UV_PYTHON_DOWNLOADS="never")
+        environment.pop("UV_PROJECT_ENVIRONMENT", None)
+        command = [
+            str(ROOT / ".venv/bin/python"), "-u", str(Path(__file__).resolve()),
+            "--_worker", str(Path(args.input).absolute()), str(run_root), str(args.event_capacity),
+        ]
+        result = _supervise(
+            command, cwd=ROOT, env=environment,
+            log_path=run_root / "worker.log", timeout=args.timeout,
+        )
+        if result:
+            _emit(f"demo: no completed dossier; diagnostics retained in {run_root}\n", stream=sys.stderr)
+            return result
+        destination = _check_complete_output(run_root)
+        _emit(f"dossier={destination}\n")
+        _emit(f"pdf={destination / 'report.pdf'}\n")
+        return 0
+    except (OSError, RuntimeError, subprocess.SubprocessError) as error:
+        _emit(f"demo: {error}\n", stream=sys.stderr)
+        return 1
+
+
+if __name__ == "__main__":
+    if len(sys.argv) == 5 and sys.argv[1] == "--_worker":
+        raise SystemExit(_worker(Path(sys.argv[2]), Path(sys.argv[3]), int(sys.argv[4])))
+    raise SystemExit(main())
diff --git a/tools/demo_check.py b/tools/demo_check.py
new file mode 100644
index 0000000..13e7e2f
--- /dev/null
+++ b/tools/demo_check.py
@@ -0,0 +1,238 @@
+#!/usr/bin/env python3
+"""Run six narrated correctness checks using installed native and Z3 tools."""
+
+from __future__ import annotations
+
+import argparse
+import os
+from pathlib import Path
+import subprocess
+import sys
+import tempfile
+import time
+
+
+ROOT = Path(__file__).resolve().parents[1]
+sys.path.insert(0, str(ROOT))
+from tools import demo
+
+
+def _require(condition: bool, message: str) -> None:
+    if not condition:
+        raise demo.DemoError(message)
+
+
+def _expect_status(result, expected: str, engine: str) -> None:
+    observed = result.status.value.upper()
+    if observed == "UNKNOWN":
+        raise demo.DemoError(f"{engine}: UNKNOWN, esito non conclusivo")
+    _require(observed == expected, f"{engine}: atteso {expected}, osservato {observed}")
+
+
+def _preflight() -> None:
+    try:
+        import z3
+        from native._lib import library
+
+        library()
+        z3.get_version_string()
+    except (ImportError, OSError) as error:
+        raise demo.DemoError(
+            f"dipendenza non disponibile: {error}; eseguire make demo-setup"
+        ) from error
+
+
+def _run_checks() -> None:
+    from crosscheck.witness_pipeline import solve_native_and_extract
+    from model.tileset import COLOR_NONE, TILESET
+    from native.formula_adapter import FormulaLoadError, FormulaParseStatus, load_formula
+    from oracles.boolean_solver import solve_boolean
+    from oracles.tiling_check import is_valid_tiling
+    from oracles.tiling_solver import solve_tiling
+    from oracles.witness_check import is_valid_assignment
+
+    sat_path = ROOT / "tests/instances/pipeline_sat.cm13"
+    unsat_path = ROOT / "tests/instances/pipeline_unsat_search.cm13"
+    invalid_path = ROOT / "tests/fuzz/corpus/cm13/malformed_domain.cm13"
+
+    print("[1/6] Input valido: il parser C deve leggere variabili e clausole CM1-in-3.", flush=True)
+    parsed = load_formula(sat_path)
+    _require(
+        parsed.variable_count == 3
+        and parsed.clauses == ((0, 0, 1), (0, 1, 2), (1, 2, 2)),
+        "contenuto inatteso nel caso SAT noto",
+    )
+    print("OK: lette 3 variabili e 3 clausole da pipeline_sat.cm13.", flush=True)
+
+    print("[2/6] Input fuori dominio: una variabile non dichiarata deve essere rifiutata.", flush=True)
+    try:
+        load_formula(invalid_path)
+    except FormulaLoadError as error:
+        _require(
+            error.status is FormulaParseStatus.DOMAIN_ERROR,
+            f"parser: atteso DOMAIN_ERROR, osservato {error.status.name}: {error}",
+        )
+    else:
+        raise demo.DemoError("il parser ha accettato il caso fuori dominio")
+    print("OK: variabile 3 con solo 2 variabili dichiarate rifiutata (DOMAIN_ERROR).", flush=True)
+
+    print("[3/6] SAT noto: il witness reference deve superare verifiche indipendenti.", flush=True)
+    sat_formula, sat_region, sat_result, sat_assignment = solve_native_and_extract(sat_path, optimized=False)
+    _require(sat_formula == parsed, "la formula del solve differisce da quella letta")
+    _expect_status(sat_result, "SAT", "reference SAT")
+    _require(
+        sat_result.tiling is not None
+        and is_valid_tiling(sat_region, TILESET, sat_result.tiling)
+        and sat_assignment is not None
+        and is_valid_assignment(sat_formula, sat_assignment),
+        "reference SAT: witness assente o non valido",
+    )
+    print("OK: tiling verificato; assegnamento estratto x1=0, x2=1, x3=0 valido.", flush=True)
+
+    print("[4/6] UNSAT noto: la clausola (x4,x4,x4) richiede 3*x4=1, impossibile per un booleano.", flush=True)
+    unsat_formula, unsat_region, unsat_result, unsat_assignment = solve_native_and_extract(unsat_path, optimized=False)
+    _require(
+        unsat_formula.variable_count == 4 and (3, 3, 3) in unsat_formula.clauses,
+        "la clausola impossibile manca dal caso UNSAT noto",
+    )
+    _expect_status(unsat_result, "UNSAT", "reference UNSAT")
+    _require(unsat_result.tiling is None and unsat_assignment is None, "UNSAT non deve avere un witness")
+    print("OK: reference restituisce UNSAT senza tiling o assegnamento.", flush=True)
+
+    print("[5/6] Accordo: reference, optimized, Boolean Z3 e Wang Z3 devono confermare i due casi noti.", flush=True)
+    for path, formula, region, expected in (
+        (sat_path, sat_formula, sat_region, "SAT"),
+        (unsat_path, unsat_formula, unsat_region, "UNSAT"),
+    ):
+        # Reference results come from checks 3/4; each other engine runs once.
+        print(f"  {path.name}: optimized", flush=True)
+        optimized_formula, optimized_region, optimized, assignment = solve_native_and_extract(path, optimized=True)
+        _require(optimized_formula == formula and optimized_region == region, "optimized: input o regione differente")
+        _expect_status(optimized, expected, "optimized")
+        if expected == "SAT":
+            _require(
+                optimized.tiling is not None and is_valid_tiling(region, TILESET, optimized.tiling)
+                and assignment is not None and is_valid_assignment(formula, assignment),
+                "optimized: witness assente o non valido",
+            )
+        else:
+            _require(optimized.tiling is None and assignment is None, "optimized UNSAT: witness inatteso")
+
+        print(f"  {path.name}: Boolean Z3", flush=True)
+        boolean = solve_boolean(formula)
+        _expect_status(boolean, expected, "Boolean Z3")
+        if expected == "SAT":
+            _require(
+                boolean.assignment is not None and is_valid_assignment(formula, boolean.assignment),
+                "Boolean Z3: witness assente o non valido",
+            )
+        else:
+            _require(boolean.assignment is None, "Boolean Z3 UNSAT: witness inatteso")
+
+        print(f"  {path.name}: Wang Z3", flush=True)
+        wang = solve_tiling(region, TILESET)
+        _expect_status(wang, expected, "Wang Z3")
+        if expected == "SAT":
+            _require(
+                wang.tiling is not None and is_valid_tiling(region, TILESET, wang.tiling),
+                "Wang Z3: witness assente o non valido",
+            )
+        else:
+            _require(wang.tiling is None, "Wang Z3 UNSAT: witness inatteso")
+        print(f"  Quattro motori concordi: {expected}.", flush=True)
+    print("OK: entrambi gli esiti noti confermati; ogni witness SAT verificato.", flush=True)
+
+    print("[6/6] Witness alterato: una tessera incompatibile deve essere rifiutata dal checker indipendente.", flush=True)
+    # Choose a valid tile ID which violates an imposed boundary color.
+    # The independent checker remains the only judge of the altered witness.
+    change = next(
+        ((index, tile_id) for index, active in enumerate(sat_region.active) if active
+         for tile_id, tile in enumerate(TILESET)
+         if any(required != COLOR_NONE and tile[direction] != required
+                for direction, required in enumerate(sat_region.boundary[index]))),
+        None,
+    )
+    _require(change is not None, "nessuna tessera alterabile nel caso SAT")
+    index, tile_id = change
+    altered = list(sat_result.tiling)
+    original_id = altered[index]
+    altered[index] = tile_id
+    _require(not is_valid_tiling(sat_region, TILESET, altered), "il checker ha accettato il witness alterato")
+    _require(is_valid_tiling(sat_region, TILESET, sat_result.tiling), "il witness originale non è più valido")
+    print(
+        f"OK: cella ({index % sat_region.width},{index // sat_region.width}), "
+        f"tessera {original_id} -> {tile_id}: copia rifiutata; originale ancora valido.",
+        flush=True,
+    )
+
+
+def _worker(run_root: Path) -> int:
+    try:
+        sys.path.insert(0, str(ROOT / "python"))
+        _preflight()
+        _run_checks()
+        with (run_root / "complete").open("x", encoding="ascii") as marker:
+            marker.write("6/6\n")
+        return 0
+    except Exception as error:
+        print(f"demo-check: {type(error).__name__}: {error}", file=sys.stderr, flush=True)
+        return 1
+
+
+def _new_run(output: Path | None) -> Path:
+    if output is not None:
+        run = output.absolute()
+        try:
+            run.mkdir(parents=True)
+        except FileExistsError as error:
+            raise demo.DemoError(f"output already exists: {run}") from error
+        return run
+    directory = ROOT / "build/demo-check"
+    directory.mkdir(parents=True, exist_ok=True)
+    return Path(tempfile.mkdtemp(prefix="run-", dir=directory))
+
+
+def main(arguments: list[str] | None = None) -> int:
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--output", type=Path, help="new diagnostic directory (default: build/demo-check/run-*)")
+    parser.add_argument(
+        "--timeout", type=demo._positive_timeout,
+        default=os.environ.get("TILING_DEMO_TIMEOUT", "300"),
+        help="global timeout in seconds (default: 300)",
+    )
+    args = parser.parse_args(arguments)
+    if not sys.platform.startswith("linux"):
+        parser.error("demo-check currently supports Linux")
+    try:
+        run_root = _new_run(args.output)
+        demo._emit(f"diagnostics={run_root}\n")
+        worker_python = ROOT / ".venv/bin/python"
+        _require(worker_python.is_file(), "Python installato mancante; eseguire make demo-setup")
+        environment = os.environ.copy()
+        environment.update(UV_OFFLINE="1", UV_NO_SYNC="1", UV_PYTHON_DOWNLOADS="never")
+        environment.pop("UV_PROJECT_ENVIRONMENT", None)
+        command = [
+            str(worker_python), "-u", str(Path(__file__).resolve()),
+            "--_worker", str(run_root),
+        ]
+        started = time.monotonic()
+        result = demo._supervise(
+            command, cwd=ROOT, env=environment,
+            log_path=run_root / "worker.log", timeout=args.timeout,
+        )
+        if result:
+            demo._emit(f"demo-check: suite non completata; diagnostica in {run_root}\n", stream=sys.stderr)
+            return result
+        marker = run_root / "complete"
+        _require(marker.is_file() and marker.read_bytes() == b"6/6\n", "suite incompleta: conferma dei sei controlli mancante")
+        demo._emit(f"Superati 6/6 controlli in {time.monotonic() - started:.3f} s.\n")
+        return 0
+    except (OSError, RuntimeError, subprocess.SubprocessError) as error:
+        demo._emit(f"demo-check: {error}\n", stream=sys.stderr)
+        return 1
+
+
+if __name__ == "__main__":
+    if len(sys.argv) == 3 and sys.argv[1] == "--_worker":
+        raise SystemExit(_worker(Path(sys.argv[2])))
+    raise SystemExit(main())
diff --git a/tools/demo_setup.py b/tools/demo_setup.py
new file mode 100644
index 0000000..24d69ef
--- /dev/null
+++ b/tools/demo_setup.py
@@ -0,0 +1,173 @@
+#!/usr/bin/env python3
+"""Check the Linux demo toolchain before setup, then check its two environments."""
+
+from __future__ import annotations
+
+import argparse
+from datetime import datetime, timezone
+from pathlib import Path
+import os
+import shlex
+import shutil
+import subprocess
+import sys
+import tempfile
+
+
+ROOT = Path(__file__).resolve().parents[1]
+SYSTEM_PACKAGES = (
+    "Debian 13: install build-essential python3 git texlive-latex-base; "
+    "Arch/Omarchy: install base-devel python git texlive-latex; "
+    "install uv separately. "
+    "See the README for the setup commands."
+)
+
+
+class SetupError(RuntimeError):
+    """A prerequisite or an installed dependency is not usable."""
+
+
+def run(command: list[str], *, cwd: Path, purpose: str) -> str:
+    try:
+        result = subprocess.run(
+            command, cwd=cwd, check=True, capture_output=True, text=True,
+            timeout=120,
+        )
+    except (OSError, subprocess.SubprocessError) as error:
+        detail = getattr(error, "stderr", "") or getattr(error, "stdout", "")
+        if isinstance(detail, bytes):
+            detail = detail.decode(errors="replace")
+        tail = "\n".join((detail or str(error)).strip().splitlines()[-12:])
+        raise SetupError(f"{purpose} failed:\n{tail}") from error
+    return result.stdout.strip()
+
+
+def configured_command(variable: str, default: str) -> list[str]:
+    try:
+        command = shlex.split(os.environ.get(variable, default))
+    except ValueError as error:
+        raise SetupError(f"Invalid {variable}: {error}") from error
+    executable = shutil.which(command[0]) if command else None
+    if executable is None:
+        raise SetupError(f"Command not found: {shlex.join(command) or default}")
+    # Probes change cwd; preserve the detected path and any wrapper symlink name.
+    command[0] = str(Path(executable).absolute())
+    return command
+
+
+def preflight() -> None:
+    if not sys.platform.startswith("linux"):
+        raise SetupError("The demo setup currently supports Linux.")
+    if sys.version_info < (3, 11):
+        raise SetupError("The setup helper needs Python 3.11 or newer (make PYTHON=...).")
+    if os.environ.get("UV_PROJECT_ENVIRONMENT"):
+        raise SetupError(
+            "Unset UV_PROJECT_ENVIRONMENT: the demo uses separate .venv and "
+            "renderer/.venv directories."
+        )
+    compiler = configured_command("DEMO_SETUP_CC", "cc")
+    uv = configured_command("DEMO_SETUP_UV", "uv")
+    if shutil.which("uv") is None:
+        raise SetupError(
+            "uv must also be on PATH: dossier renderer subprocesses invoke it by name."
+        )
+    if shutil.which("git") is None:
+        raise SetupError("git is missing; dossiers record the repository commit.")
+    if shutil.which("pdflatex") is None:
+        raise SetupError("pdflatex is missing; the demo includes a PDF dossier.")
+    print("[1/3] Checking C17, uv and PDF dependencies...", flush=True)
+    print(run([*uv, "--version"], cwd=ROOT, purpose="uv"), flush=True)
+    with tempfile.TemporaryDirectory(prefix="tiling-demo-setup-") as temporary:
+        scratch = Path(temporary)
+        source = scratch / "check.c"
+        source.write_text(
+            "#include <stdint.h>\n#include <stdlib.h>\n"
+            "_Static_assert(__STDC_VERSION__ >= 201710L, \"C17 required\");\n"
+            "int main(void) { uint32_t value = 17; return value != 17; }\n",
+            encoding="utf-8",
+        )
+        run(
+            [*compiler, "-std=c17", str(source), "-o", str(scratch / "check")],
+            cwd=scratch, purpose="C17 compilation",
+        )
+        run([str(scratch / "check")], cwd=scratch, purpose="C17 executable")
+
+        # The real preamble catches missing packages and T1 fonts. Reuse the
+        # dossier compiler so user-local TeX files cannot hide missing packages.
+        sys.path.insert(0, str(ROOT / "python"))
+        from dossier.tex_compile import TexCompileError, compile_tex_pdf
+
+        template = (ROOT / "templates/run-report-v2.tex").read_text(encoding="utf-8")
+        body = (
+            r"\section{Setup check}" "\n"
+            r"Caf\'e, \textbf{bold}, \texttt{monospace}: $x_1 + x_2 = 1$." "\n"
+            r"\begin{longtable}{ll}Engine & Status \\ Reference & ready\end{longtable}"
+        )
+        (scratch / "report.tex").write_text(
+            template.replace("@@TITLE@@", "Tiling Foundry setup").replace("@@BODY@@", body),
+            encoding="utf-8",
+        )
+        try:
+            compile_tex_pdf(scratch, "pdflatex", datetime(2026, 1, 1, tzinfo=timezone.utc))
+        except TexCompileError as error:
+            tail = "\n".join(str(error).splitlines()[-12:])
+            raise SetupError(f"PDF dependency check failed:\n{tail}") from error
+    print("Prerequisites ready; installing the two locked Python environments.", flush=True)
+
+
+def verify() -> None:
+    print("[2/3] Checking Z3 and the native shared library...", flush=True)
+    core_python = ROOT / ".venv/bin/python"
+    renderer_python = ROOT / "renderer/.venv/bin/python"
+    for interpreter in (core_python, renderer_python):
+        if not interpreter.is_file():
+            raise SetupError(
+                f"Missing environment: {interpreter.relative_to(ROOT)}. "
+                "Run make demo-setup without a custom UV_PROJECT_ENVIRONMENT."
+            )
+    print(run(
+        [str(core_python), "-c", (
+            "import sys; assert sys.version_info >= (3, 11); "
+            "sys.path.insert(0, 'python'); import z3; "
+            "from native._lib import library; library(); "
+            "value = z3.IntVal(1); assert z3.simplify(value + 1).as_long() == 2; "
+            "print('Python ' + sys.version.split()[0] + ', Z3 ' + z3.get_version_string() "
+            "+ ', libwang.so loaded')"
+        )], cwd=ROOT, purpose="Core dependency check",
+    ), flush=True)
+    print("[3/3] Checking the renderer and its image/font support...", flush=True)
+    print(run(
+        [str(renderer_python), "-c", (
+            "import io, sys; assert sys.version_info >= (3, 14); "
+            "import numpy; from PIL import Image, ImageDraw, __version__; "
+            "from wang_explain import explain_font; "
+            "image = Image.fromarray(numpy.zeros((48, 160, 3), dtype=numpy.uint8)); "
+            "ImageDraw.Draw(image).text((0, 0), 'Tiling Foundry', font=explain_font(14)); "
+            "output = io.BytesIO(); image.save(output, format='PNG'); "
+            "output.seek(0); Image.open(output).verify(); "
+            "print('Python ' + sys.version.split()[0] + ', NumPy ' + numpy.__version__ "
+            "+ ', Pillow ' + __version__ + ', PNG and font ready')"
+        )], cwd=ROOT / "renderer", purpose="Renderer dependency check",
+    ), flush=True)
+    print("Demo setup complete. The installed environments support offline runs.", flush=True)
+
+
+def main() -> int:
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("phase", choices=("preflight", "verify"))
+    arguments = parser.parse_args()
+    try:
+        if arguments.phase == "preflight":
+            preflight()
+        else:
+            verify()
+    except (SetupError, OSError) as error:
+        print(f"demo-setup: {error}", file=sys.stderr)
+        if arguments.phase == "preflight":
+            print(SYSTEM_PACKAGES, file=sys.stderr)
+        return 1
+    return 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())
diff --git a/uv.lock b/uv.lock
index 7ed5cb8..e8c04af 100644
--- a/uv.lock
+++ b/uv.lock
@@ -386,7 +386,7 @@ wheels = [
 
 [[package]]
 name = "tiling-foundry"
-version = "0.1.0"
+version = "1.0.0"
 source = { virtual = "." }
 dependencies = [
     { name = "z3-solver" },