diff --git a/config/models.yaml b/config/models.yaml
index af2af4b..f8cb770 100644
--- a/config/models.yaml
+++ b/config/models.yaml
@@ -26,13 +26,14 @@ models:
   # Anthropic Claude
   claude:
     provider: "anthropic"
-    model_name: "claude-sonnet-4-20250514"
+    # Sonnet 4 (claude-sonnet-4-20250514) retired 2026-06-15; switched to the
+    # current Opus tier on 2026-06-30. Opus 4.8 removes the sampling params:
+    # temperature/top_p/top_k now return a 400, so they are intentionally absent.
+    model_name: "claude-opus-4-8"
     api_key_env: "ANTHROPIC_API_KEY"
-    temperature: 0.1
-    # claude-sonnet-4 rejects max_tokens > 64000 (API: "maximum allowed
-    # number of output tokens for claude-sonnet-4-20250514"); probed 2026-06-09.
+    # Opus 4.8 supports up to 128000 output tokens; kept at 64000 to match the
+    # prior run's cap and stay within non-streaming timeout limits.
     max_tokens: 64000
-    top_p: 0.9
 
   deepseek_tencent:
     provider: "deepseek"
diff --git a/data/patches/spin_2thread_ktest.patch b/data/patches/spin_2thread_ktest.patch
new file mode 100644
index 0000000..133570a
--- /dev/null
+++ b/data/patches/spin_2thread_ktest.patch
@@ -0,0 +1,46 @@
+--- a/ostd/src/sync/spin_trace_tests.rs
++++ b/ostd/src/sync/spin_trace_tests.rs
+@@ -98,7 +98,35 @@
+         crate::early_println!("Expected trace count: 18 events");
+         crate::early_println!("- 6 tests × 3 events each (TryAcquire + Success + Release) = 18 total");
+     }
+-    
++
++    /// Two-actor contention scenario matching the JS-SAM 2-thread spin model.
++    /// A single-CPU ktest can't spawn a real 2nd thread that blocks (a blocking
++    /// lock() from actor 1 while actor 0 holds would spin forever), so the 2nd
++    /// actor's contention is expressed via try_lock, which fails without blocking.
++    #[ktest]
++    fn test_spin_2thread() {
++        crate::early_println!("=== 2-Thread SpinLock Trace Start ===");
++        let lock = Arc::new(SpinTrace::<u32, PreemptDisabled>::new(0));
++
++        // actor 0 acquires (blocking): TryAcquireBlocking(0) + AcquireSuccess(0)
++        let g0 = lock.lock_with_thread_id(0);
++        // actor 1 attempts while 0 holds -> AcquireFail(1) (contention, no deadlock)
++        assert!(lock.try_lock_with_thread_id(1).is_none());
++        // actor 0 releases: Release(0)
++        drop(g0);
++        // actor 1 acquires (blocking): TryAcquireBlocking(1) + AcquireSuccess(1)
++        let g1 = lock.lock_with_thread_id(1);
++        // actor 0 attempts while 1 holds -> AcquireFail(0)
++        assert!(lock.try_lock_with_thread_id(0).is_none());
++        // actor 1 releases: Release(1)
++        drop(g1);
++        // actor 0 non-blocking acquire when free -> AcquireSuccess(0)
++        let g0b = lock.try_lock_with_thread_id(0).expect("lock is free");
++        drop(g0b); // Release(0)
++
++        crate::early_println!("=== 2-Thread SpinLock Trace Complete ===");
++    }
++
+     #[ktest]
+     fn test_tla_trace_simple() {
+         crate::early_println!("=== TLA+ SpinLock Randomized Trace Test Start ===");
+@@ -212,4 +240,4 @@
+             _ => unreachable!(),
+         }
+     }
+-}
++}
+\ No newline at end of file
diff --git a/data/sys_traces/spin/spin_2thread.ndjson b/data/sys_traces/spin/spin_2thread.ndjson
new file mode 100644
index 0000000..a4788a6
--- /dev/null
+++ b/data/sys_traces/spin/spin_2thread.ndjson
@@ -0,0 +1,8 @@
+{"action": "AcquireLock", "data": {"thread": 0, "callType": "lock"}, "pre_state": {"lockHeld": false, "lockHolder": null}, "post_state": {"lockHeld": true, "lockHolder": 0}}
+{"action": "AcquireLock", "data": {"thread": 1, "callType": "try"}, "pre_state": {"lockHeld": true, "lockHolder": 0}, "post_state": {"lockHeld": true, "lockHolder": 0}}
+{"action": "ReleaseLock", "data": {"thread": 0}, "pre_state": {"lockHeld": true, "lockHolder": 0}, "post_state": {"lockHeld": false, "lockHolder": null}}
+{"action": "AcquireLock", "data": {"thread": 1, "callType": "lock"}, "pre_state": {"lockHeld": false, "lockHolder": null}, "post_state": {"lockHeld": true, "lockHolder": 1}}
+{"action": "AcquireLock", "data": {"thread": 0, "callType": "try"}, "pre_state": {"lockHeld": true, "lockHolder": 1}, "post_state": {"lockHeld": true, "lockHolder": 1}}
+{"action": "ReleaseLock", "data": {"thread": 1}, "pre_state": {"lockHeld": true, "lockHolder": 1}, "post_state": {"lockHeld": false, "lockHolder": null}}
+{"action": "AcquireLock", "data": {"thread": 0, "callType": "try"}, "pre_state": {"lockHeld": false, "lockHolder": null}, "post_state": {"lockHeld": true, "lockHolder": 0}}
+{"action": "ReleaseLock", "data": {"thread": 0}, "pre_state": {"lockHeld": true, "lockHolder": 0}, "post_state": {"lockHeld": false, "lockHolder": null}}
diff --git a/docs/js_sam_first_experiment.md b/docs/js_sam_first_experiment.md
new file mode 100644
index 0000000..1430847
--- /dev/null
+++ b/docs/js_sam_first_experiment.md
@@ -0,0 +1,323 @@
+# First End-to-End JS-SAM Experiment on SysMoBench
+
+**Task:** `spin` (Asterinas OS spinlock) · **Backend:** JS-SAM · **Model:** Claude
+Opus 4.8 · **Method:** `direct_call`
+**Date:** 2026-06-30 · **Host:** Windows 11, Docker Desktop 4.80 (engine 29.6.1)
+
+---
+
+## Abstract
+
+We ran the first complete, four-phase SysMoBench evaluation of the **JS-SAM**
+backend — JavaScript specifications written in the [SAM
+pattern](https://sam.js.org) — on the `spin` task, using Claude Opus 4.8 to
+generate the specification. All four phases produced real results: syntax
+(Phase 1), bounded model checking (Phase 2), transition validation against
+**real kernel-captured traces** (Phase 3), and invariant verification (Phase 4).
+
+The headline result is a **Phase 3 score of 87.5% (7/8 trace windows)**. The
+single failing window is diagnostic rather than incidental: the generated model
+reproduces blocking `lock()` acquisitions correctly but its non-blocking
+`try_lock` acquire never actually takes the lock — a defect observable only when
+acquiring from a free state, and caught precisely because the model was replayed
+against transitions captured from the real Asterinas spinlock.
+
+Reaching a real Phase 3 number required standing up a kernel trace-capture
+harness from scratch (the trace corpus is not shipped with the benchmark) and
+authoring a 2-thread instrumentation scenario matching what the JS-SAM prompt
+models. Several cross-platform defects in the harness were fixed along the way,
+making JS-SAM runnable on a Windows host.
+
+---
+
+## 1. Background and objective
+
+SysMoBench evaluates AI systems on formally modeling real concurrent/distributed
+systems across four automated phases. JS-SAM is the benchmark's first
+**non-formal-language** backend: instead of TLA+/Alloy/CSP, the model emits an
+executable JavaScript module following the SAM pattern (actions propose, a model
+accepts, state is a pure function of the model). It tests a distinct hypothesis:
+
+> Can an LLM produce a correct system specification in a pattern it sees
+> constantly in training (JavaScript) more readily than in formal languages it
+> rarely sees?
+
+This experiment is the first data point toward that question: a full run of one
+model on one task, establishing that the JS-SAM pipeline works end-to-end and
+producing a per-phase score profile for later comparison against the formal
+backends.
+
+### Integration decisions (from the maintainers)
+
+Four open questions from the JS-SAM spec were resolved by the upstream
+maintainer prior to this run, and shaped it:
+
+1. **In scope** — JS-SAM is a valid leaderboard backend.
+2. **Traces** — trace sets are not fixed data; they are generated on demand by
+   instrumenting the real system. The maintainers' `spin` captures use three
+   threads; the JS-SAM prompt models two. The two cannot share a trace set, so
+   **JS-SAM must generate its own traces at the granularity it models** (two
+   threads), using the existing instrumentation
+   (`data/patches/asterinas_tla_trace.patch`, `task.yaml > tv.harness`) as a
+   reference. This directly motivated the Phase 3 work below.
+3. **Depth bound** — `depthMax` is a per-task config value with a documented
+   default; 6 is the default for `spin`.
+4. **Shared invariant translation** — only TLA+ has the agent-based invariant
+   translator; Alloy, PAT, and JS-SAM fall back to a direct API call.
+   Generalizing the agent translator is deferred future work.
+
+---
+
+## 2. Environment and configuration
+
+| Component | Value |
+|---|---|
+| Host OS | Windows 11, Git Bash + PowerShell |
+| Container runtime | Docker Desktop 4.80, engine 29.6.1 (WSL2 backend) |
+| JS-SAM sandbox image | `node:20-slim` (throwaway container per helper call) |
+| Generation model | `claude` → `claude-opus-4-8` (Anthropic API via LiteLLM) |
+| Task | `spin` — Asterinas `ostd/src/sync/spin.rs` |
+| Generation method | `direct_call` (single prompt) |
+| Exploration depth (Phase 2/4) | `depthMax = 6` |
+
+Two configuration corrections were required before any run:
+
+- The `claude` model entry pointed at `claude-sonnet-4-20250514`, which
+  **retired 2026-06-15** and returned `not_found_error`. Repointed to
+  `claude-opus-4-8`.
+- Opus 4.8 rejects `temperature`/`top_p`/`top_k` (HTTP 400); the LiteLLM adapter
+  was sending them unconditionally. Both fixes are described in §5.
+
+---
+
+## 3. Method
+
+Each phase evaluates the **same** generated specification (`spin.js`, produced
+once by Opus 4.8 in Phase 1) so the four scores describe one artifact. The
+JS-SAM backend shells out to a Node helper (`tools/js-sam/cli.mjs`) inside a
+locked-down Docker container (`--network none`, read-only rootfs, non-root user,
+CPU/memory/PID caps); the container is the trust boundary for model-generated
+JavaScript.
+
+- **Phase 1 — compilation_check:** parse + module-load + structural contract
+  check of the generated module.
+- **Phase 2 — runtime_check:** bounded exploration of the model's own state
+  space by the sam-pattern explorer at `depthMax 6`; a second identical
+  exploration detects nondeterminism.
+- **Phase 3 — transition_validation (direct path):** each captured
+  `(pre_state, action, post_state)` window is replayed —
+  `setState(pre)`, `actions[name](data)`, then `getState()` is diffed against
+  `post` under the projection rule (only keys present in the trace's post-state
+  must match; model-only bookkeeping is ignored). This is the direct path — no
+  coding-agent orchestration — because SAM *is* `model.present(action(data))`.
+- **Phase 4 — invariant_verification:** three expert spinlock invariants are
+  translated to JavaScript predicates (direct API call) and checked by the
+  explorer.
+
+---
+
+## 4. Phase 3: capturing real spinlock traces
+
+Phase 3 is the only phase requiring data external to the model, and no `spin`
+trace corpus ships with the benchmark. Producing a legitimate trace set meant
+building and running the instrumented Asterinas kernel and folding its output
+into the JS-SAM state schema. This section documents that pipeline because it is
+the experiment's main methodological contribution.
+
+### 4.1 Pipeline
+
+1. **Source at a compatible revision.** The reference instrumentation patch does
+   **not** apply to Asterinas `main`; it applies cleanly at tag **v0.16.0**,
+   which also matches the toolchain bundled in the
+   `asterinas/asterinas:0.16.0-20250822` image. We clone v0.16.0.
+2. **Instrumentation.** Apply `data/patches/asterinas_tla_trace.patch` (the
+   reference TLA+-trace instrumentation, which adds `ostd/src/sync/spin_trace.rs`
+   emitting serial JSON events) plus a new **2-thread ktest** (§4.2).
+3. **Build + run.** Inside the image: install `cargo-osdk`, `make initramfs`,
+   and `cargo osdk test --features tla-trace --qemu-args='-accel tcg'
+   test_spin_2thread`. The kernel boots under QEMU (software TCG) and the ktest
+   emits trace events over the serial port.
+4. **Parse.** `scripts/harness/spin/parse_traces.py` folds the event stream into
+   `(pre, post)` NDJSON windows.
+
+### 4.2 Authoring a 2-thread contention scenario
+
+The reference spin ktests are **single-actor** (all operations attributed to
+thread 0), so they never exercise the contention (`trying`/failed-acquire)
+behavior the JS-SAM model represents across two threads. A blocking `lock()`
+from a second actor in a single-CPU ktest would spin forever (deadlock), so the
+new `test_spin_2thread` expresses the second actor's contention with a
+**non-blocking `try_lock`** that fails without blocking:
+
+```
+actor0.lock()      -> TryAcquireBlocking(0), AcquireSuccess(0)   // 0 holds
+actor1.try_lock()  -> AcquireFail(1)                             // contention, no deadlock
+actor0.release()   -> Release(0)
+actor1.lock()      -> TryAcquireBlocking(1), AcquireSuccess(1)   // 1 holds
+actor0.try_lock()  -> AcquireFail(0)                             // contention
+actor1.release()   -> Release(1)
+actor0.try_lock()  -> AcquireSuccess(0)                          // try from free succeeds
+actor0.release()   -> Release(0)
+```
+
+### 4.3 Event → state mapping
+
+The kernel emits low-level events
+(`TryAcquireBlocking`, `AcquireSuccess`, `AcquireFail`, `Release`). The parser
+folds them into windows keyed on the **objective, model-independent** spinlock
+state `{lockHeld, lockHolder}` — the real observable lock ownership — and lets
+the projection rule ignore the model's internal `threadStatus`/`callType`
+bookkeeping. This keeps the traces faithful to the *system* rather than tailored
+to any one model:
+
+| Kernel event | Model window |
+|---|---|
+| `TryAcquireBlocking(t)` | folded (pre-step of a blocking acquire; emits no window) |
+| `AcquireSuccess(t)` | `AcquireLock` → lock held by `t` (`callType` `lock` if preceded by `TryAcquireBlocking`, else `try`) |
+| `AcquireFail(t)` | `AcquireLock` (`callType` `try`) → ownership unchanged (contention does not steal the lock) |
+| `Release(t)` | `ReleaseLock` → lock free |
+
+The 10 emitted events fold to **8 windows** at
+`data/sys_traces/spin/spin_2thread.ndjson`.
+
+The whole capture is reproducible via `scripts/harness/spin/run.sh`.
+
+---
+
+## 5. Engineering contributions
+
+The following defects were found and fixed to make the run possible; each is a
+self-contained commit on the `full-stack` branch.
+
+1. **Cross-platform JS-SAM Docker sandbox** (`tla_eval/languages/js_sam.py`).
+   The sandbox was POSIX-host-only: it called `os.getuid()`/`getgid()` (absent
+   on Windows) and mounted the helper and spec at their host paths (invalid
+   container destinations for Windows `C:\` paths). Fixed by decoupling host
+   paths from fixed in-container mount points (`/opt/js-sam`, `/work`),
+   normalizing `-v` sources to forward slashes, rewriting `specPath` to the
+   container path, and selecting a non-root `--user` behind a
+   `hasattr(os, "getuid")` guard. Behavior is unchanged on Linux/macOS; the
+   backend now runs on a Windows host. (Upstreamable.)
+2. **Model refresh** (`config/models.yaml`, `tla_eval/models/litellm_adapter.py`).
+   Repointed `claude` to `claude-opus-4-8` and added
+   `_should_omit_sampling_params()` so `temperature`/`top_p`/`top_k` are dropped
+   for models that reject them (Opus 4.7+, Fable 5, Mythos 5) — LiteLLM's
+   `drop_params` does not yet cover these models.
+3. **UTF-8 console output** (`scripts/run_benchmark.py`). The result summary
+   printed `✓`/`✗`, which raised `UnicodeEncodeError` on a Windows cp1252
+   console after a successful evaluation; std streams are now reconfigured to
+   UTF-8.
+4. **`states_explored` for non-TLA+ backends** (`ModelCheckOutcome`,
+   `js_sam.py`, `runtime_check.py`, `manual_invariant_evaluator.py`). The metric
+   was hardcoded to 0 for any non-TLA+ backend even though the JS-SAM helper
+   already reports `stepsExplored`; it is now threaded through (and the invariant
+   evaluator's top-level field, previously 0 for all backends, is populated).
+5. **Spin Phase-3 trace harness** (`scripts/harness/spin/*`,
+   `data/patches/spin_2thread_ktest.patch`, `data/sys_traces/spin/*`). §4.
+
+Cross-platform frictions resolved during the capture: patch pinned to v0.16.0;
+CRLF normalization of both the Asterinas clone (`core.autocrlf`) and the patch
+files; and building on an ext4 docker volume because the Windows bind-mount does
+not support `fallocate` (needed to build the initramfs image).
+
+---
+
+## 6. Results
+
+All four phases evaluate the same Opus 4.8 `spin.js`.
+
+| Phase | Metric | Result | Detail |
+|---|---|---|---|
+| 1 | compilation_check | **PASS** | 0 syntax errors, 0 semantic errors |
+| 2 | runtime_check | **PASS** | 326,592 states explored (`depthMax 6`), 0 violations, no deadlock |
+| 3 | transition_validation | **PASS** | **87.5% (7/8 windows)** — AcquireLock 80% (4/5), ReleaseLock 100% (3/3) |
+| 4 | invariant_verification | **PASS** | 3/3 invariants: MutualExclusion, LockStatusConsistency, NoDeadlock |
+
+### The Phase 3 discrepancy
+
+The single failing window is an `AcquireLock` where the trace expects
+`{lockHeld: true, lockHolder: 0}` but the model produced `{lockHeld: false,
+lockHolder: null}` — i.e., the model failed to acquire a **free** lock via the
+`try_lock` (`callType: "try"`) path. The pattern is precise:
+
+- Blocking `lock()` acquisitions (`callType: "lock"`) reproduce correctly.
+- A failed `try_lock` under contention passes (ownership is unchanged either
+  way, so the mismatch is masked).
+- A `try_lock` that **should succeed** from a free lock exposes the defect: the
+  generated model's `try` acquire never takes the lock.
+
+This is a genuine modeling gap in the Opus 4.8 specification, surfaced only
+because the model was checked against transitions observed in the real kernel —
+the intended value of transition validation.
+
+---
+
+## 7. Discussion
+
+- **The JS-SAM pipeline is viable end-to-end**, including on a non-Linux host,
+  and produces a full four-phase score profile suitable for later comparison
+  against the formal-language backends.
+- **Phase 3 has teeth.** Even a small, deterministic trace set (8 windows)
+  discriminated correct from incorrect transitions and localized a specific
+  defect in the generated model. The `try_lock`-from-free case is a good example
+  of a transition that syntactic and self-consistency checks (Phases 1–2) and
+  invariant checking (Phase 4) all pass while the model is still wrong about
+  real behavior.
+- **Objective-state windows are robust.** Keying traces on `{lockHeld,
+  lockHolder}` and relying on the projection rule kept the trace corpus
+  independent of the model under test, which is the correct stance for a
+  ground-truth oracle.
+
+---
+
+## 8. Limitations and threats to validity
+
+- **Single model, single task, single generation.** No cross-model or
+  cross-language comparison yet; the central JS-SAM hypothesis is not answered by
+  one data point.
+- **Small, single-scenario trace set.** Eight windows from one deterministic
+  ktest. Contention is expressed via `try_lock` on a single CPU rather than true
+  SMP concurrency, so scenarios like a thread blocking-then-acquiring on release
+  are not represented. Broader coverage (more scenarios, more interleavings)
+  would strengthen Phase 3.
+- **Invariant translation used the direct API call**, per JS-SAM's current
+  policy, not the agent-based translator TLA+ uses (Open Question 4).
+- **Non-blocking-only second actor.** The 2-thread ktest models contention
+  faithfully for lock ownership but does not capture a real waiter's blocking
+  wakeup.
+
+---
+
+## 9. Future work
+
+1. **Broaden the spin trace corpus** — additional `test_spin_*` scenarios
+   (blocking waiter released and acquiring, longer interleavings) for richer
+   Phase 3 coverage.
+2. **Run additional models and record the score profiles** to begin answering
+   the JS-SAM hypothesis (e.g., Sonnet 4.6, Haiku 4.5).
+3. **A second JS-SAM task** with richer control state (`ringbuffer`/`locksvc`)
+   once trace harnesses exist for them.
+4. **Generalize the agent invariant translator** so JS-SAM (and Alloy/PAT) can
+   share the TLA+ approach instead of falling back to a direct call.
+
+---
+
+## 10. Reproducibility
+
+```bash
+# Phases 1/2/4 (generation + evaluation), one metric per invocation:
+python scripts/run_benchmark.py --task spin --method direct_call \
+  --model claude --language JS-SAM --metric compilation_check
+#   ... runtime_check / invariant_verification
+
+# Phase 3: capture traces, then validate.
+bash scripts/harness/spin/run.sh          # -> data/sys_traces/spin/spin_2thread.ndjson
+python scripts/run_benchmark.py --task spin --method direct_call \
+  --model claude --language JS-SAM --metric transition_validation --yes \
+  --spec-file <generated spin.js>
+```
+
+Requirements: Docker (with the `node:20-slim` and
+`asterinas/asterinas:0.16.0-20250822` images), Node ≥ 20, `ANTHROPIC_API_KEY` in
+`.env`. The JS-SAM sandbox and the Phase-3 capture both run under Docker Desktop
+on Windows after the fixes in §5.
diff --git a/scripts/harness/spin/.gitattributes b/scripts/harness/spin/.gitattributes
new file mode 100644
index 0000000..048c212
--- /dev/null
+++ b/scripts/harness/spin/.gitattributes
@@ -0,0 +1,4 @@
+# These scripts run inside a Linux container (build_and_test.sh) or drive it
+# (run.sh); they must keep LF endings even when checked out on Windows, or bash
+# fails on the CR (`$'\r': command not found`).
+*.sh text eol=lf
diff --git a/scripts/harness/spin/build_and_test.sh b/scripts/harness/spin/build_and_test.sh
new file mode 100644
index 0000000..23209c7
--- /dev/null
+++ b/scripts/harness/spin/build_and_test.sh
@@ -0,0 +1,40 @@
+#!/bin/bash
+# In-container build + run of the Asterinas 2-thread spin trace ktest.
+#
+# Runs inside asterinas/asterinas:0.16.0-20250822. The patched source is
+# bind-mounted read-only at /src (host FS — may not support fallocate), so we
+# build on an ext4 docker volume at /build where mke2fs/fallocate work. /build
+# persists across runs, so re-runs after editing the ktest are incremental.
+#
+# Emits kernel serial JSON on stdout: lines like
+#   {"seq":N,"thread":T,"lock":0,"state":"locked|unlocked","action":A,"actor":T}
+# which scripts/harness/spin/parse_traces.py folds into NDJSON windows.
+set -e
+export PATH=/nix/store/4zpvbvn0cvmmn9k05b1qgr5xh7i6r9ka-nix-2.31.1/bin:$PATH
+echo 'connect-timeout = 60000' >> /etc/nix/nix.conf
+
+if [ ! -f /build/Makefile ]; then
+  echo "===== populating /build from /src (first run) ====="
+  cp -a /src/. /build/
+fi
+# Refresh instrumentation + tests so edits take effect on incremental re-runs.
+cp -f /src/ostd/src/sync/spin_trace.rs       /build/ostd/src/sync/spin_trace.rs
+cp -f /src/ostd/src/sync/spin_trace_tests.rs /build/ostd/src/sync/spin_trace_tests.rs
+
+cd /build
+echo "===== installing cargo-osdk ====="
+OSDK_LOCAL_DEV=1 cargo install cargo-osdk --path osdk --locked
+echo "===== make initramfs ====="
+make initramfs
+echo "===== cargo osdk test (test_spin_2thread) ====="
+cd ostd
+# Capture the test's real exit code: under set -e a bare $? after a failing
+# command is unreachable (the script would have aborted), so the DONE line
+# would always print rc=0. Disable -e around the call, record rc, re-exit.
+set +e
+timeout 1200 cargo osdk test --features tla-trace --target-arch x86_64 \
+  --qemu-args='-accel tcg' test_spin_2thread 2>&1
+rc=$?
+set -e
+echo "===== DONE rc=$rc ====="
+exit "$rc"
diff --git a/scripts/harness/spin/parse_traces.py b/scripts/harness/spin/parse_traces.py
new file mode 100644
index 0000000..a156e34
--- /dev/null
+++ b/scripts/harness/spin/parse_traces.py
@@ -0,0 +1,120 @@
+#!/usr/bin/env python3
+"""Fold Asterinas spin-trace serial events into JS-SAM (pre, post) NDJSON windows.
+
+Input: the docker/QEMU run log (mixed build output + kernel serial JSON events of
+the form emitted by ostd/src/sync/spin_trace.rs):
+
+    {"seq":N,"thread":T,"lock":0,"state":"locked|unlocked","action":A,"actor":T}
+
+Output: one NDJSON file of event-form windows (see
+tla_eval/evaluation/semantics/trace_loader.py), each line:
+
+    {"action": "AcquireLock"|"ReleaseLock", "data": {...},
+     "pre_state": {...}, "post_state": {...}}
+
+The window state is the *objective, model-independent* spinlock state
+{lockHeld, lockHolder} — the real lock ownership observed by the kernel. JS-SAM's
+Phase-3 projection rule only requires the trace's post_state keys to match the
+model, so the model's internal threadStatus/callType bookkeeping is ignored and
+the traces stay faithful to the system rather than tailored to any one model.
+
+Event -> model action mapping:
+  TryAcquireBlocking(t)  pre-step of a blocking lock(); folded, emits no window
+  AcquireSuccess(t)      AcquireLock: lock becomes held by t
+                         (callType "lock" if preceded by TryAcquireBlocking, else "try")
+  AcquireFail(t)         AcquireLock (callType "try"): contention — ownership unchanged
+  Release(t)             ReleaseLock: lock becomes free
+  StopSpinning(t)        internal spin step; skipped
+
+Usage:
+  parse_traces.py <input_log> <output_ndjson>
+"""
+
+import json
+import re
+import sys
+from pathlib import Path
+
+EVENT_RE = re.compile(r'\{"seq":\d+[^{}]*"action":"[^"]*"[^{}]*\}')
+
+
+def extract_events(log_text):
+    events = []
+    for match in EVENT_RE.findall(log_text):
+        try:
+            event = json.loads(match)
+        except json.JSONDecodeError:
+            continue
+        if "action" in event and "thread" in event:
+            events.append(event)
+    return events
+
+
+def fold_windows(events):
+    lock_held = False
+    lock_holder = None
+    blocking = {}  # thread -> True after a TryAcquireBlocking, cleared on its acquire
+    windows = []
+
+    for event in events:
+        action = event["action"]
+        thread = event["thread"]
+
+        if action == "TryAcquireBlocking":
+            blocking[thread] = True
+            continue
+        if action == "StopSpinning":
+            continue
+
+        pre = {"lockHeld": lock_held, "lockHolder": lock_holder}
+
+        if action == "AcquireSuccess":
+            call_type = "lock" if blocking.pop(thread, False) else "try"
+            lock_held, lock_holder = True, thread
+            windows.append({
+                "action": "AcquireLock",
+                "data": {"thread": thread, "callType": call_type},
+                "pre_state": pre,
+                "post_state": {"lockHeld": lock_held, "lockHolder": lock_holder},
+            })
+        elif action == "AcquireFail":
+            blocking.pop(thread, None)
+            # Failed contention: the lock stays with its current holder.
+            windows.append({
+                "action": "AcquireLock",
+                "data": {"thread": thread, "callType": "try"},
+                "pre_state": pre,
+                "post_state": {"lockHeld": lock_held, "lockHolder": lock_holder},
+            })
+        elif action == "Release":
+            lock_held, lock_holder = False, None
+            windows.append({
+                "action": "ReleaseLock",
+                "data": {"thread": thread},
+                "pre_state": pre,
+                "post_state": {"lockHeld": lock_held, "lockHolder": lock_holder},
+            })
+
+    return windows
+
+
+def main():
+    if len(sys.argv) != 3:
+        print(__doc__)
+        sys.exit(2)
+    log_path = Path(sys.argv[1])
+    out_path = Path(sys.argv[2])
+
+    events = extract_events(log_path.read_text(encoding="utf-8", errors="replace"))
+    windows = fold_windows(events)
+
+    out_path.parent.mkdir(parents=True, exist_ok=True)
+    with out_path.open("w", encoding="utf-8") as f:
+        for window in windows:
+            f.write(json.dumps(window) + "\n")
+
+    print(f"wrote {len(windows)} windows from {len(events)} events -> {out_path}")
+
+
+if __name__ == "__main__":
+    main()
diff --git a/scripts/harness/spin/run.sh b/scripts/harness/spin/run.sh
new file mode 100644
index 0000000..7d0c0c9
--- /dev/null
+++ b/scripts/harness/spin/run.sh
@@ -0,0 +1,69 @@
+#!/usr/bin/env bash
+# scripts/harness/spin/run.sh — capture Asterinas spinlock execution traces for
+# the JS-SAM Phase-3 (transition validation) direct path.
+#
+# Produces a 2-thread (pre, post) NDJSON trace set at
+#   data/sys_traces/spin/spin_2thread.ndjson
+# from a real run of the instrumented Asterinas spinlock under QEMU.
+#
+# Pipeline:
+#   1. Clone Asterinas at v0.16.0 (matches the docker image toolchain; the
+#      reference patch does not apply to current main) with LF line endings.
+#   2. Apply data/patches/asterinas_tla_trace.patch (reference TLA+ trace
+#      instrumentation) + data/patches/spin_2thread_ktest.patch (adds the
+#      2-actor `test_spin_2thread` ktest — the reference tests are single-actor).
+#   3. Build + run the ktest under QEMU-TCG inside the asterinas image, on an
+#      ext4 docker volume (the source may be on a host FS without fallocate).
+#   4. Fold the kernel serial JSON into JS-SAM windows via parse_traces.py.
+#
+# Requires: docker, the asterinas/asterinas:0.16.0-20250822 image, git, python3.
+# Windows note: run from Git Bash with Docker Desktop; the CRLF and fallocate
+# handling below is what makes the Linux-oriented flow work on a Windows host.
+set -euo pipefail
+
+SCRIPT_DIR=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)
+PROJECT_ROOT=$(cd "$SCRIPT_DIR/../../.." && pwd)
+
+SRC="${ASTERINAS_SOURCE_DIR:-$PROJECT_ROOT/artifacts/spin}"
+IMAGE="${ASTERINAS_DOCKER_IMAGE:-asterinas/asterinas:0.16.0-20250822}"
+REF_PATCH="$PROJECT_ROOT/data/patches/asterinas_tla_trace.patch"
+ADD_PATCH="$PROJECT_ROOT/data/patches/spin_2thread_ktest.patch"
+TRACES_OUT="${TRACES_OUT:-$PROJECT_ROOT/data/sys_traces/spin/spin_2thread.ndjson}"
+LOG="${LOG:-$PROJECT_ROOT/artifacts/spin_capture.log}"
+
+# 1-2. Clone + patch (idempotent: skip if already instrumented). The guard is
+# a sentinel written only after BOTH patches apply — checking for a file the
+# first patch creates would leave a half-patched checkout unrecoverable if the
+# second apply fails (set -e aborts, the next run would skip the whole block).
+SENTINEL="$SRC/.sysmobench_instrumented"
+if [ ! -e "$SENTINEL" ]; then
+  echo "[run.sh] cloning asterinas v0.16.0 (LF) into $SRC" >&2
+  rm -rf "$SRC"
+  git -c core.autocrlf=false clone --depth 1 --branch v0.16.0 \
+    https://github.com/asterinas/asterinas.git "$SRC"
+  git -C "$SRC" config core.autocrlf false
+  # Patches (and the sysmobench checkout) may carry CRLF on Windows; normalize
+  # to LF before applying so the emitted Rust/shell files build in Linux.
+  echo "[run.sh] applying reference + 2-thread patches" >&2
+  tr -d '\r' < "$REF_PATCH" | git -C "$SRC" apply --whitespace=nowarn
+  tr -d '\r' < "$ADD_PATCH" | git -C "$SRC" apply --whitespace=nowarn
+  touch "$SENTINEL"
+fi
+
+# 3. Build + run under QEMU, capturing serial output. Source is read-only; the
+# build happens on the ext4 volume `spin-work`; cargo cache on `spin-cargo`.
+echo "[run.sh] building + running test_spin_2thread under QEMU (see $LOG)" >&2
+docker run --rm --privileged \
+  -v "$SRC:/src:ro" \
+  -v "$SCRIPT_DIR:/harness:ro" \
+  -v "spin-work:/build" \
+  -v "spin-cargo:/root/.cargo" \
+  "$IMAGE" bash /harness/build_and_test.sh > "$LOG" 2>&1 || {
+    echo "[run.sh] docker run failed; tail of $LOG:" >&2
+    tail -40 "$LOG" >&2
+    exit 1
+  }
+
+# 4. Parse serial JSON -> NDJSON windows.
+python3 "$SCRIPT_DIR/parse_traces.py" "$LOG" "$TRACES_OUT"
+echo "[run.sh] traces written to $TRACES_OUT" >&2
diff --git a/scripts/run_benchmark.py b/scripts/run_benchmark.py
index 865b400..be0d80f 100644
--- a/scripts/run_benchmark.py
+++ b/scripts/run_benchmark.py
@@ -43,6 +43,15 @@
 logging.basicConfig(level=logging.INFO, format='[%(levelname)s] %(message)s')
 logger = logging.getLogger(__name__)
 
+# The result summaries print status glyphs (✓ / ✗ / ⏭) that crash on consoles
+# whose default encoding can't represent them (e.g. Windows cp1252). Force the
+# std streams to UTF-8; a no-op where they already speak it.
+for _stream in (sys.stdout, sys.stderr):
+    try:
+        _stream.reconfigure(encoding="utf-8")
+    except (AttributeError, ValueError):
+        pass
+
 
 def _display_evaluation_results(eval_result):
     """Print a unified summary across SyntaxEvaluationResult / SemanticEvaluationResult / TransitionValidationResult."""
diff --git a/tests/test_evaluation/test_trace_loader.py b/tests/test_evaluation/test_trace_loader.py
index 1fbc678..eacdbef 100644
--- a/tests/test_evaluation/test_trace_loader.py
+++ b/tests/test_evaluation/test_trace_loader.py
@@ -113,17 +113,20 @@ def test_direct_path_dispatches_to_backend(self, tmp_path, monkeypatch):
         assert result.per_action_pass_rates == {"AcquireLock": 1.0}
 
     def test_missing_traces_reported_cleanly(self, tmp_path, monkeypatch):
+        from tla_eval.evaluation.semantics import trace_loader
         from tla_eval.evaluation.semantics.transition_validation import (
             TransitionValidationEvaluator,
         )
 
+        def raise_missing_traces(task_name):
+            raise FileNotFoundError(f"Trace folder not found for task '{task_name}'")
+
+        monkeypatch.setattr(trace_loader, "load_trace_windows", raise_missing_traces)
+
         spec = PROJECT_ROOT / "tests" / "fixtures" / "js_sam" / "specs" / "spin-good.js"
         evaluator = TransitionValidationEvaluator(
             language="JS-SAM", workspace_root=str(tmp_path)
         )
-        # No monkeypatch: the real spin traces_folder (data/sys_traces/spin)
-        # is not checked into the repository, so the loader must fail with an
-        # actionable message rather than a crash.
         result = evaluator.evaluate(
             generation_result=SimpleNamespace(metadata={}),
             task_name="spin",
diff --git a/tla_eval/evaluation/semantics/manual_invariant_evaluator.py b/tla_eval/evaluation/semantics/manual_invariant_evaluator.py
index c040e48..7322327 100644
--- a/tla_eval/evaluation/semantics/manual_invariant_evaluator.py
+++ b/tla_eval/evaluation/semantics/manual_invariant_evaluator.py
@@ -949,6 +949,9 @@ def evaluate(self,
             invariant_results = outcome.cases
             result.model_checking_successful = any(c.success for c in invariant_results)
             result.model_checking_time = sum(c.elapsed_seconds for c in invariant_results)
+            result.states_explored = sum(
+                c.metadata.get("states_explored", 0) for c in invariant_results
+            )
 
             passed_count = sum(1 for c in invariant_results if c.success)
             total_count = len(invariant_results)
diff --git a/tla_eval/evaluation/semantics/runtime_check.py b/tla_eval/evaluation/semantics/runtime_check.py
index 2c7bea6..d06ce2f 100644
--- a/tla_eval/evaluation/semantics/runtime_check.py
+++ b/tla_eval/evaluation/semantics/runtime_check.py
@@ -646,7 +646,7 @@ def evaluate(self,
             # Other backends may not provide these; default to safe values.
             violations: List[str] = []
             deadlock = False
-            states = 0
+            states = mc_outcome.states_explored or 0
             if self.language.lower() in ("tla+", "tla", "tlaplus", "tla_plus"):
                 try:
                     runner = TLCRunner(timeout=self.timeout)
diff --git a/tla_eval/languages/js_sam.py b/tla_eval/languages/js_sam.py
index 00ec74d..a2534bd 100644
--- a/tla_eval/languages/js_sam.py
+++ b/tla_eval/languages/js_sam.py
@@ -65,6 +65,13 @@
 _SANDBOX_CPUS = "2"
 _SANDBOX_PIDS = "256"
 
+# Fixed in-container mount points, kept independent of the host paths so the
+# sandbox works regardless of host path shape (POSIX paths and Windows C:\
+# paths alike). cli.mjs resolves node_modules from its own location, so the
+# whole helper dir is mounted and the spec is mounted under a separate dir.
+_CONTAINER_HELPER_DIR = "/opt/js-sam"
+_CONTAINER_WORK_DIR = "/work"
+
 # Bench-wide exploration depth for the sam-pattern behavior explorer
 # (Phases 2 and 4). Deliberately a single constant rather than per-task
 # config: revisit when a second task lands (spec Open Question 3).
@@ -113,6 +120,29 @@ def _force_remove_container(name: str) -> None:
 _helper_call_counter = 0
 
 
+def _docker_mount_source(path: Path) -> str:
+    """Host path for a ``docker -v`` source, normalized to forward slashes.
+
+    Docker accepts forward-slash paths on every platform; on Windows this
+    avoids backslash ambiguity in the ``-v src:dst`` argument (the drive-letter
+    colon, e.g. ``C:``, is handled by Docker Desktop's volume parser).
+    """
+    return str(path).replace("\\", "/")
+
+
+def _sandbox_user_args() -> List[str]:
+    """``--user`` args that run the sandbox as a non-root user.
+
+    On POSIX hosts, match the host uid:gid so the read-only bind mounts are
+    guaranteed readable. Windows has no ``os.getuid``/``getgid`` and Docker
+    Desktop maps bind mounts readable to any container user, so fall back to a
+    fixed non-root uid there.
+    """
+    if hasattr(os, "getuid"):
+        return ["--user", f"{os.getuid()}:{os.getgid()}"]
+    return ["--user", "1000:1000"]
+
+
 def _run_helper(
     subcommand: str, request: Dict[str, Any], timeout: int
 ) -> Tuple[Optional[Dict[str, Any]], Optional[str]]:
@@ -133,21 +163,28 @@ def _run_helper(
     _helper_call_counter += 1
     container_name = f"sysmobench-jssam-{os.getpid()}-{_helper_call_counter}"
 
-    # The helper (cli.mjs + node_modules) and, for spec-bound subcommands, the
-    # single generated spec file. The helper only reads these; all output is
-    # JSON on stdout. cli.mjs resolves node_modules from its own location, so
-    # mounting HELPER_DIR at the same path keeps that working in-container.
-    mounts = ["-v", f"{HELPER_DIR}:{HELPER_DIR}:ro"]
+    # Mount the helper (cli.mjs + node_modules) at a fixed container path; the
+    # in-container layout is then independent of the host path shape, and the
+    # spec is mounted under a separate dir below. The helper only reads these;
+    # all output is JSON on stdout. cli.mjs resolves node_modules from its own
+    # location (its NODE_PATH setup), so any consistent mount point works.
+    mounts = ["-v", f"{_docker_mount_source(HELPER_DIR)}:{_CONTAINER_HELPER_DIR}:ro"]
+
+    # Rewrite specPath to where the spec is mounted *inside* the container.
+    # Copy the request so the caller's dict is not mutated.
+    request = dict(request)
     spec_path = request.get("specPath")
     if spec_path:
         sp = Path(spec_path).resolve()
-        mounts += ["-v", f"{sp}:{sp}:ro"]
+        container_spec = f"{_CONTAINER_WORK_DIR}/{sp.name}"
+        mounts += ["-v", f"{_docker_mount_source(sp)}:{container_spec}:ro"]
+        request["specPath"] = container_spec
 
     cmd = [
         "docker", "run", "--rm", "-i",
         "--name", container_name,
         "--network", "none",
-        "--user", f"{os.getuid()}:{os.getgid()}",
+        *_sandbox_user_args(),
         "--read-only",
         "--tmpfs", "/tmp",
         "-e", "HOME=/tmp",
@@ -155,9 +192,9 @@ def _run_helper(
         "--cpus", _SANDBOX_CPUS,
         "--pids-limit", _SANDBOX_PIDS,
         *mounts,
-        "-w", str(HELPER_DIR),
+        "-w", _CONTAINER_HELPER_DIR,
         DOCKER_IMAGE,
-        "node", str(HELPER_CLI), subcommand,
+        "node", f"{_CONTAINER_HELPER_DIR}/cli.mjs", subcommand,
     ]
     try:
         proc = subprocess.run(
@@ -371,6 +408,7 @@ def run_model_checker(
             elapsed_seconds=elapsed,
             error_message="; ".join(errors) if errors else None,
             classification=response.get("classification"),
+            states_explored=response.get("stepsExplored"),
         )
 
     # ---- Phase 3 (direct path) ------------------------------------------
@@ -547,7 +585,7 @@ def check_invariants(
             if r.get("counterexample"):
                 metadata["counterexample"] = r["counterexample"]
             if r.get("stepsExplored") is not None:
-                metadata["steps_explored"] = r["stepsExplored"]
+                metadata["states_explored"] = r["stepsExplored"]
 
             outcome.cases.append(
                 InvariantCaseResult(
diff --git a/tla_eval/languages/result_types.py b/tla_eval/languages/result_types.py
index b757f8e..46a8ce4 100644
--- a/tla_eval/languages/result_types.py
+++ b/tla_eval/languages/result_types.py
@@ -31,6 +31,7 @@ class ModelCheckOutcome:
     elapsed_seconds: float = 0.0
     error_message: Optional[str] = None
     classification: Optional[str] = None  # e.g. "violation", "deadlock", "timeout", "parse_error"
+    states_explored: Optional[int] = None  # steps/states the checker explored, when the backend reports it
 
 
 @dataclass
diff --git a/tla_eval/models/litellm_adapter.py b/tla_eval/models/litellm_adapter.py
index 0914509..db2de8d 100644
--- a/tla_eval/models/litellm_adapter.py
+++ b/tla_eval/models/litellm_adapter.py
@@ -281,6 +281,25 @@ def _supports_missing_api_key(self) -> bool:
     def _should_omit_top_p(self) -> bool:
         return self.litellm_model.startswith("openai/gpt-5")
 
+    def _should_omit_sampling_params(self) -> bool:
+        """Whether to drop temperature/top_p/top_k for this model.
+
+        Claude Opus 4.7+, Fable 5, and Mythos 5 removed the sampling
+        parameters and return a 400 ("`temperature` is deprecated for this
+        model") if any are sent. litellm's drop_params does not yet cover
+        these newer models, so the request must omit them here.
+        """
+        model = self.litellm_model.lower()
+        return any(
+            tag in model
+            for tag in (
+                "claude-opus-4-8",
+                "claude-opus-4-7",
+                "claude-fable-5",
+                "claude-mythos-5",
+            )
+        )
+
     def _build_completion_params(
         self,
         prompt: str,
@@ -312,15 +331,17 @@ def _build_completion_params(
         if model_max_tokens is not None:
             params["max_tokens"] = model_max_tokens
 
+        omit_sampling = self._should_omit_sampling_params()
+
         model_temperature = self.config.get(
             "temperature",
             generation_config.temperature,
         )
-        if model_temperature is not None:
+        if model_temperature is not None and not omit_sampling:
             params["temperature"] = model_temperature
 
         model_top_p = self.config.get("top_p", generation_config.top_p)
-        if model_top_p is not None and not self._should_omit_top_p():
+        if model_top_p is not None and not self._should_omit_top_p() and not omit_sampling:
             params["top_p"] = model_top_p
 
         if generation_config.stop_sequences: