diff --git a/harness/pstack/claude-code/skills/statechart/SKILL.md b/harness/pstack/claude-code/skills/statechart/SKILL.md
index f5a64a8db..c832a8bce 100644
--- a/harness/pstack/claude-code/skills/statechart/SKILL.md
+++ b/harness/pstack/claude-code/skills/statechart/SKILL.md
@@ -18,7 +18,7 @@ Work in a scratch folder outside the repo. Write a TLA+ spec and its config. The
 
 `scripts/statechart.ts` is TypeScript, so run it with a runtime that can execute TypeScript.
 
-The first run installs TLC and Java with mise and needs the network.
+The skill runs TLC with [tla-ts](https://github.com/aidenybai/tla-ts) in Node. The first run installs it with npx and needs the network.
 
 ## Write the spec
 
diff --git a/harness/pstack/claude-code/skills/statechart/scripts/run.ts b/harness/pstack/claude-code/skills/statechart/scripts/run.ts
index 4efd368e5..fcd0618d1 100644
--- a/harness/pstack/claude-code/skills/statechart/scripts/run.ts
+++ b/harness/pstack/claude-code/skills/statechart/scripts/run.ts
@@ -67,6 +67,7 @@ export function* fileLines(file: string) {
 const TLC_TOOL =
   "http:tla2tools[url=https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar,checksum=sha256:936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88]@1.7.4";
 const JAVA_TOOL = "java@temurin-25";
+const TLA_TS_PACKAGE = "tla-ts";
 export const PINNED_FLAGS = ["-workers", "1", "-fp", "0", "-lncheck", "final"];
 
 type ChildResult = {
@@ -190,9 +191,21 @@ const runToFiles = (
     });
   });
 
+// tla-ts runs TLC 1.7.4 in Node. TLA_TS_PACKAGE overrides the package that npx installs. If npx
+// cannot install it, or JAVA or TLA2TOOLS is set, TLC runs with Java as before.
 async function findTlc(cwd: string) {
-  const { TLA2TOOLS, JAVA } = process.env;
-  if (TLA2TOOLS) return { jar: TLA2TOOLS, java: JAVA || "java" };
+  const { TLA2TOOLS, JAVA, TLA_TS_PACKAGE: tlaTsPackage = TLA_TS_PACKAGE } = process.env;
+  let npxError = "";
+  if (!JAVA && !TLA2TOOLS) {
+    const r = await runChild(
+      "npx",
+      ["--yes", `--package=${tlaTsPackage}`, "--call", "command -v tla-ts"],
+      { cwd, env: process.env },
+    );
+    if (r.status === 0) return { command: r.stdout.trim(), args: ["-Dtla-ts.tlc=1.7.4"] };
+    npxError = `npx could not install ${tlaTsPackage}: ${r.error?.message ?? r.stderr.trim()}\n`;
+  }
+  if (TLA2TOOLS) return { command: JAVA || "java", args: ["-cp", TLA2TOOLS] };
   const mise = (...args: string[]) =>
     runChild("mise", args, { cwd, env: { ...process.env, MISE_CEILING_PATHS: cwd } });
   const where = () =>
@@ -202,13 +215,13 @@ async function findTlc(cwd: string) {
     const r = await mise("install", JAVA_TOOL, TLC_TOOL);
     if (r.status !== 0)
       throw new Error(
-        `Cannot find TLC: mise install failed: ${r.error?.message ?? r.stderr.trim()}\nOr set TLA2TOOLS to the path of tla2tools.jar, and JAVA to a java binary (Java 11 or later).`,
+        `Cannot find TLC: ${npxError}mise install failed: ${r.error?.message ?? r.stderr.trim()}\nOr set TLA2TOOLS to the path of tla2tools.jar, and JAVA to a java binary (Java 11 or later).`,
       );
     found = await where();
   }
   return {
-    jar: path.join(found[0].stdout.trim(), "tla2tools.jar"),
-    java: JAVA || found[1].stdout.trim(),
+    command: JAVA || found[1].stdout.trim(),
+    args: ["-cp", path.join(found[0].stdout.trim(), "tla2tools.jar")],
   };
 }
 
@@ -282,16 +295,8 @@ export async function check(specFile: string, configFile: string): Promise<Check
       const tmp = path.join(dir, `tmp-${name}`);
       fs.mkdirSync(tmp);
       return runToFiles(
-        tlc.java,
-        [
-          `-Djava.io.tmpdir=${tmp}`,
-          `-DTLA-Library=${folder}`,
-          ...jvm,
-          "-cp",
-          tlc.jar,
-          main,
-          ...args,
-        ],
+        tlc.command,
+        [`-Djava.io.tmpdir=${tmp}`, `-DTLA-Library=${folder}`, ...jvm, ...tlc.args, main, ...args],
         {
           cwd: dir,
           out: path.join(dir, name),
diff --git a/pstack/skills/statechart/SKILL.md b/pstack/skills/statechart/SKILL.md
index f5a64a8db..c832a8bce 100644
--- a/pstack/skills/statechart/SKILL.md
+++ b/pstack/skills/statechart/SKILL.md
@@ -18,7 +18,7 @@ Work in a scratch folder outside the repo. Write a TLA+ spec and its config. The
 
 `scripts/statechart.ts` is TypeScript, so run it with a runtime that can execute TypeScript.
 
-The first run installs TLC and Java with mise and needs the network.
+The skill runs TLC with [tla-ts](https://github.com/aidenybai/tla-ts) in Node. The first run installs it with npx and needs the network.
 
 ## Write the spec
 
diff --git a/pstack/skills/statechart/scripts/run.ts b/pstack/skills/statechart/scripts/run.ts
index 4efd368e5..fcd0618d1 100644
--- a/pstack/skills/statechart/scripts/run.ts
+++ b/pstack/skills/statechart/scripts/run.ts
@@ -67,6 +67,7 @@ export function* fileLines(file: string) {
 const TLC_TOOL =
   "http:tla2tools[url=https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar,checksum=sha256:936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88]@1.7.4";
 const JAVA_TOOL = "java@temurin-25";
+const TLA_TS_PACKAGE = "tla-ts";
 export const PINNED_FLAGS = ["-workers", "1", "-fp", "0", "-lncheck", "final"];
 
 type ChildResult = {
@@ -190,9 +191,21 @@ const runToFiles = (
     });
   });
 
+// tla-ts runs TLC 1.7.4 in Node. TLA_TS_PACKAGE overrides the package that npx installs. If npx
+// cannot install it, or JAVA or TLA2TOOLS is set, TLC runs with Java as before.
 async function findTlc(cwd: string) {
-  const { TLA2TOOLS, JAVA } = process.env;
-  if (TLA2TOOLS) return { jar: TLA2TOOLS, java: JAVA || "java" };
+  const { TLA2TOOLS, JAVA, TLA_TS_PACKAGE: tlaTsPackage = TLA_TS_PACKAGE } = process.env;
+  let npxError = "";
+  if (!JAVA && !TLA2TOOLS) {
+    const r = await runChild(
+      "npx",
+      ["--yes", `--package=${tlaTsPackage}`, "--call", "command -v tla-ts"],
+      { cwd, env: process.env },
+    );
+    if (r.status === 0) return { command: r.stdout.trim(), args: ["-Dtla-ts.tlc=1.7.4"] };
+    npxError = `npx could not install ${tlaTsPackage}: ${r.error?.message ?? r.stderr.trim()}\n`;
+  }
+  if (TLA2TOOLS) return { command: JAVA || "java", args: ["-cp", TLA2TOOLS] };
   const mise = (...args: string[]) =>
     runChild("mise", args, { cwd, env: { ...process.env, MISE_CEILING_PATHS: cwd } });
   const where = () =>
@@ -202,13 +215,13 @@ async function findTlc(cwd: string) {
     const r = await mise("install", JAVA_TOOL, TLC_TOOL);
     if (r.status !== 0)
       throw new Error(
-        `Cannot find TLC: mise install failed: ${r.error?.message ?? r.stderr.trim()}\nOr set TLA2TOOLS to the path of tla2tools.jar, and JAVA to a java binary (Java 11 or later).`,
+        `Cannot find TLC: ${npxError}mise install failed: ${r.error?.message ?? r.stderr.trim()}\nOr set TLA2TOOLS to the path of tla2tools.jar, and JAVA to a java binary (Java 11 or later).`,
       );
     found = await where();
   }
   return {
-    jar: path.join(found[0].stdout.trim(), "tla2tools.jar"),
-    java: JAVA || found[1].stdout.trim(),
+    command: JAVA || found[1].stdout.trim(),
+    args: ["-cp", path.join(found[0].stdout.trim(), "tla2tools.jar")],
   };
 }
 
@@ -282,16 +295,8 @@ export async function check(specFile: string, configFile: string): Promise<Check
       const tmp = path.join(dir, `tmp-${name}`);
       fs.mkdirSync(tmp);
       return runToFiles(
-        tlc.java,
-        [
-          `-Djava.io.tmpdir=${tmp}`,
-          `-DTLA-Library=${folder}`,
-          ...jvm,
-          "-cp",
-          tlc.jar,
-          main,
-          ...args,
-        ],
+        tlc.command,
+        [`-Djava.io.tmpdir=${tmp}`, `-DTLA-Library=${folder}`, ...jvm, ...tlc.args, main, ...args],
         {
           cwd: dir,
           out: path.join(dir, name),