diff --git a/harness/pstack/claude-code/skills/statechart/scripts/statechart.mjs b/harness/pstack/claude-code/skills/statechart/scripts/statechart.mjs
index 6e276da3d..236930817 100644
--- a/harness/pstack/claude-code/skills/statechart/scripts/statechart.mjs
+++ b/harness/pstack/claude-code/skills/statechart/scripts/statechart.mjs
@@ -101,7 +101,8 @@ const COMMON = `Both commands
                      files in a temporary folder, and then replaces the whole output folder with
                      it. When runs overlap, the output folder has the files of the run that
                      finished last. The command does not use an output folder that has files that
-                     it did not write. On a filesystem that cannot rename, the command copies the
+                     it did not write. Older output folders without tlc/.written.json need a new
+                     --out folder. On a filesystem that cannot rename, the command copies the
                      files into place, and overlapping runs can mix their files.
   --png              Also render each chart to PNG with npx @mermaid-js/mermaid-cli.
   -h, --help         Print this help, and exit 0.
@@ -651,6 +652,8 @@ function render(charts, shown) {
 function finish({ work, out, inputs }, { files, charts }, ok, png) {
   unchanged(inputs, out);
   const pngs = png ? render(charts, published(work, out)) : [];
+  const tlc = path.join(work, "tlc");
+  fs.writeFileSync(path.join(tlc, WRITTEN), `${JSON.stringify(fs.readdirSync(tlc))}\n`);
   publish(work, out, inputs);
   const written = [...charts, ...pngs, files.stories, files.summary]
     .map((f) => path.basename(f))
@@ -662,21 +665,30 @@ function finish({ work, out, inputs }, { files, charts }, ok, png) {
 
 const published = (work, out) => (file) => rel(path.join(out, path.relative(work, file)));
 
-// Files a run writes at the top of its output folder, and inside tlc/. Only a regular file with one
-// of these names is the run's own; a folder (or a link) under an owned name is not, and neither is
-// anything nested under tlc/ that TLC or this script did not write. publish() removes the previous
-// folder whole, so everything it holds must be ours.
 const OWN =
   /^((chart|bug-\d+(-developer|-layered)?)\.(mmd|png)|stories\.md|summary\.json|\.DS_Store)$/;
-const OWN_TLC = /^([^/]+\.(cfg|out|dot)|regions-(proof|all)\.mmd)$/;
+const WRITTEN = ".written.json";
+
+function foreignTlc(dir) {
+  let written;
+  try {
+    written = JSON.parse(fs.readFileSync(path.join(dir, WRITTEN), "utf8"));
+  } catch {}
+  const own = new Set([".DS_Store"]);
+  if (Array.isArray(written) && written.every((f) => typeof f === "string"))
+    for (const f of [WRITTEN, ...written]) own.add(f);
+  return fs
+    .readdirSync(dir, { withFileTypes: true })
+    .filter((g) => !g.isFile() || !own.has(g.name))
+    .map((g) => `tlc/${g.name}`);
+}
 
 function foreign(dir) {
   try {
     const found = [];
     for (const entry of fs.readdirSync(dir, { withFileTypes: true })) {
       if (entry.name === "tlc" && entry.isDirectory()) {
-        for (const inner of fs.readdirSync(path.join(dir, "tlc"), { withFileTypes: true }))
-          if (!(inner.isFile() && OWN_TLC.test(inner.name))) found.push(`tlc/${inner.name}`);
+        found.push(...foreignTlc(path.join(dir, "tlc")));
       } else if (!(entry.isFile() && OWN.test(entry.name))) found.push(entry.name);
     }
     return found.sort();
diff --git a/harness/pstack/claude-code/skills/statechart/scripts/test/statechart.test.mjs b/harness/pstack/claude-code/skills/statechart/scripts/test/statechart.test.mjs
index d56646118..efa6f474a 100644
--- a/harness/pstack/claude-code/skills/statechart/scripts/test/statechart.test.mjs
+++ b/harness/pstack/claude-code/skills/statechart/scripts/test/statechart.test.mjs
@@ -911,6 +911,7 @@ test("statechart.mjs refuses an output folder with foreign files under tlc/ or b
   // A user's file inside the owned tlc/ folder.
   mkdirSync(join(dir, "nested", "tlc"), { recursive: true });
   writeFileSync(join(dir, "nested", "tlc", "Pay.out"), "");
+  writeFileSync(join(dir, "nested", "tlc", ".written.json"), '["Pay.out"]\n');
   writeFileSync(join(dir, "nested", "tlc", "notes.md"), "mine\n");
   refused("nested", "tlc/notes.md");
   assert.equal(readFileSync(join(dir, "nested", "tlc", "notes.md"), "utf8"), "mine\n");
@@ -936,14 +937,59 @@ test("statechart.mjs refuses an output folder with foreign files under tlc/ or b
   mkdirSync(join(dir, "own", "tlc"), { recursive: true });
   for (const f of ["chart.mmd", "stories.md", "summary.json", ".DS_Store", "bug-1.png"])
     writeFileSync(join(dir, "own", f), "");
-  for (const f of ["Pay.cfg", "Pay.out", "Pay.dot", "Pay-Safe.cfg", "regions-proof.mmd"])
+  const ownTlc = ["Pay.cfg", "Pay.out", "Pay.dot", "Pay-Safe.cfg", "regions-proof.mmd"];
+  for (const f of ownTlc)
     writeFileSync(join(dir, "own", "tlc", f), "");
+  writeFileSync(join(dir, "own", "tlc", ".written.json"), JSON.stringify(ownTlc));
   // The run gets past the ownership check and stops at the next step, the missing mapping.
   const own = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", "own"], dir, env);
   assert.doesNotMatch(own.stderr, /did not write/);
   assert.match(own.stderr, /Wrote Pay\.map\.mjs/);
 });
 
+test("statechart.mjs refuses unrecorded TLC files and invalid ownership records", () => {
+  const dir = mkdtempSync(join(tmpdir(), "statechart-"));
+  writeFileSync(join(dir, "tla2tools.jar"), "");
+  writeFileSync(join(dir, "Pay.tla"), "---- MODULE Pay ----\n====\n");
+  writeFileSync(join(dir, "Pay.cfg"), "SPECIFICATION Spec\n");
+  const env = { TLA2TOOLS: join(dir, "tla2tools.jar") };
+  const out = join(dir, "out");
+  const tlc = join(out, "tlc");
+  for (const name of ["owner-notes.cfg", "owner-notes.out", "owner-notes.dot", "Checkout-backup.cfg"]) {
+    mkdirSync(tlc, { recursive: true });
+    writeFileSync(join(tlc, "Checkout.cfg"), "generated\n");
+    writeFileSync(join(tlc, ".written.json"), '["Checkout.cfg"]\n');
+    writeFileSync(join(tlc, name), "mine\n");
+    const r = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", out], dir, env);
+    assert.equal(r.status, 2, r.stderr);
+    assert.match(r.stderr, /did not write/);
+    assert.ok(r.stderr.includes(`tlc/${name}`), r.stderr);
+    assert.equal(readFileSync(join(tlc, name), "utf8"), "mine\n");
+    rmSync(out, { recursive: true });
+  }
+  for (const record of [null, "{", "{}", '["Pay.cfg", 1]']) {
+    mkdirSync(tlc, { recursive: true });
+    writeFileSync(join(tlc, "Pay.cfg"), "kept\n");
+    if (record !== null) writeFileSync(join(tlc, ".written.json"), record);
+    const r = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", out], dir, env);
+    assert.equal(r.status, 2, r.stderr);
+    assert.match(r.stderr, /did not write/);
+    assert.match(r.stderr, /--out with a new folder/);
+    assert.equal(readFileSync(join(tlc, "Pay.cfg"), "utf8"), "kept\n");
+    rmSync(out, { recursive: true });
+  }
+  for (const kind of ["directory", "symlink"]) {
+    mkdirSync(tlc, { recursive: true });
+    writeFileSync(join(tlc, ".written.json"), '["Pay.cfg"]\n');
+    if (kind === "directory") mkdirSync(join(tlc, "Pay.cfg"));
+    else symlinkSync(join(dir, "Pay.cfg"), join(tlc, "Pay.cfg"));
+    const r = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", out], dir, env);
+    assert.equal(r.status, 2, r.stderr);
+    assert.match(r.stderr, /did not write: tlc\/Pay.cfg/);
+    rmSync(out, { recursive: true });
+  }
+});
+
 test("statechart.mjs exits 2 and names a helper script that cannot start", () => {
   const dir = mkdtempSync(join(tmpdir(), "statechart-"));
   writeFileSync(join(dir, "notes-app.mmd"), fixture("sync.mmd"));
@@ -2810,6 +2856,36 @@ const writeLamp = (dir) => {
   return join(dir, "Lamp-statechart");
 };
 
+test("TLC reruns replace recorded files, remove old rule files, and preserve unrecorded files", needsTlc, () => {
+  const dir = mkdtempSync(join(tmpdir(), "statechart-"));
+  const out = writeLamp(dir);
+  const spec = readFileSync(join(dir, "Lamp.tla"), "utf8").replace(
+    "====",
+    "Safe == on \\in BOOLEAN\n====",
+  );
+  writeFileSync(join(dir, "Lamp.tla"), spec);
+  writeFileSync(join(dir, "Lamp.cfg"), "SPECIFICATION Spec\nINVARIANT Safe\n");
+  const run = () => node("statechart.mjs", ["from-spec", "Lamp.tla"], dir);
+  for (let i = 0; i < 2; i++) {
+    const r = run();
+    assert.equal(r.status, 0, r.stderr);
+    assert.ok(existsSync(join(out, "tlc", "Lamp-Safe.cfg")));
+  }
+  writeFileSync(join(dir, "Lamp.cfg"), "SPECIFICATION Spec\n");
+  const changed = run();
+  assert.equal(changed.status, 0, changed.stderr);
+  assert.equal(existsSync(join(out, "tlc", "Lamp-Safe.cfg")), false);
+  for (const name of ["owner-notes.cfg", "owner-notes.out", "owner-notes.dot", "Lamp-backup.cfg"]) {
+    const file = join(out, "tlc", name);
+    writeFileSync(file, "mine\n");
+    const r = run();
+    assert.equal(r.status, 2, r.stderr);
+    assert.match(r.stderr, /did not write/);
+    assert.equal(readFileSync(file, "utf8"), "mine\n");
+    rmSync(file);
+  }
+});
+
 test("a rerun without --png removes the chart.png of an earlier run", needsTlc, () => {
   const dir = mkdtempSync(join(tmpdir(), "statechart-"));
   const out = writeLamp(dir);
diff --git a/pstack/skills/statechart/scripts/statechart.mjs b/pstack/skills/statechart/scripts/statechart.mjs
index 6e276da3d..236930817 100644
--- a/pstack/skills/statechart/scripts/statechart.mjs
+++ b/pstack/skills/statechart/scripts/statechart.mjs
@@ -101,7 +101,8 @@ const COMMON = `Both commands
                      files in a temporary folder, and then replaces the whole output folder with
                      it. When runs overlap, the output folder has the files of the run that
                      finished last. The command does not use an output folder that has files that
-                     it did not write. On a filesystem that cannot rename, the command copies the
+                     it did not write. Older output folders without tlc/.written.json need a new
+                     --out folder. On a filesystem that cannot rename, the command copies the
                      files into place, and overlapping runs can mix their files.
   --png              Also render each chart to PNG with npx @mermaid-js/mermaid-cli.
   -h, --help         Print this help, and exit 0.
@@ -651,6 +652,8 @@ function render(charts, shown) {
 function finish({ work, out, inputs }, { files, charts }, ok, png) {
   unchanged(inputs, out);
   const pngs = png ? render(charts, published(work, out)) : [];
+  const tlc = path.join(work, "tlc");
+  fs.writeFileSync(path.join(tlc, WRITTEN), `${JSON.stringify(fs.readdirSync(tlc))}\n`);
   publish(work, out, inputs);
   const written = [...charts, ...pngs, files.stories, files.summary]
     .map((f) => path.basename(f))
@@ -662,21 +665,30 @@ function finish({ work, out, inputs }, { files, charts }, ok, png) {
 
 const published = (work, out) => (file) => rel(path.join(out, path.relative(work, file)));
 
-// Files a run writes at the top of its output folder, and inside tlc/. Only a regular file with one
-// of these names is the run's own; a folder (or a link) under an owned name is not, and neither is
-// anything nested under tlc/ that TLC or this script did not write. publish() removes the previous
-// folder whole, so everything it holds must be ours.
 const OWN =
   /^((chart|bug-\d+(-developer|-layered)?)\.(mmd|png)|stories\.md|summary\.json|\.DS_Store)$/;
-const OWN_TLC = /^([^/]+\.(cfg|out|dot)|regions-(proof|all)\.mmd)$/;
+const WRITTEN = ".written.json";
+
+function foreignTlc(dir) {
+  let written;
+  try {
+    written = JSON.parse(fs.readFileSync(path.join(dir, WRITTEN), "utf8"));
+  } catch {}
+  const own = new Set([".DS_Store"]);
+  if (Array.isArray(written) && written.every((f) => typeof f === "string"))
+    for (const f of [WRITTEN, ...written]) own.add(f);
+  return fs
+    .readdirSync(dir, { withFileTypes: true })
+    .filter((g) => !g.isFile() || !own.has(g.name))
+    .map((g) => `tlc/${g.name}`);
+}
 
 function foreign(dir) {
   try {
     const found = [];
     for (const entry of fs.readdirSync(dir, { withFileTypes: true })) {
       if (entry.name === "tlc" && entry.isDirectory()) {
-        for (const inner of fs.readdirSync(path.join(dir, "tlc"), { withFileTypes: true }))
-          if (!(inner.isFile() && OWN_TLC.test(inner.name))) found.push(`tlc/${inner.name}`);
+        found.push(...foreignTlc(path.join(dir, "tlc")));
       } else if (!(entry.isFile() && OWN.test(entry.name))) found.push(entry.name);
     }
     return found.sort();
diff --git a/pstack/skills/statechart/scripts/test/statechart.test.mjs b/pstack/skills/statechart/scripts/test/statechart.test.mjs
index d56646118..efa6f474a 100644
--- a/pstack/skills/statechart/scripts/test/statechart.test.mjs
+++ b/pstack/skills/statechart/scripts/test/statechart.test.mjs
@@ -911,6 +911,7 @@ test("statechart.mjs refuses an output folder with foreign files under tlc/ or b
   // A user's file inside the owned tlc/ folder.
   mkdirSync(join(dir, "nested", "tlc"), { recursive: true });
   writeFileSync(join(dir, "nested", "tlc", "Pay.out"), "");
+  writeFileSync(join(dir, "nested", "tlc", ".written.json"), '["Pay.out"]\n');
   writeFileSync(join(dir, "nested", "tlc", "notes.md"), "mine\n");
   refused("nested", "tlc/notes.md");
   assert.equal(readFileSync(join(dir, "nested", "tlc", "notes.md"), "utf8"), "mine\n");
@@ -936,14 +937,59 @@ test("statechart.mjs refuses an output folder with foreign files under tlc/ or b
   mkdirSync(join(dir, "own", "tlc"), { recursive: true });
   for (const f of ["chart.mmd", "stories.md", "summary.json", ".DS_Store", "bug-1.png"])
     writeFileSync(join(dir, "own", f), "");
-  for (const f of ["Pay.cfg", "Pay.out", "Pay.dot", "Pay-Safe.cfg", "regions-proof.mmd"])
+  const ownTlc = ["Pay.cfg", "Pay.out", "Pay.dot", "Pay-Safe.cfg", "regions-proof.mmd"];
+  for (const f of ownTlc)
     writeFileSync(join(dir, "own", "tlc", f), "");
+  writeFileSync(join(dir, "own", "tlc", ".written.json"), JSON.stringify(ownTlc));
   // The run gets past the ownership check and stops at the next step, the missing mapping.
   const own = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", "own"], dir, env);
   assert.doesNotMatch(own.stderr, /did not write/);
   assert.match(own.stderr, /Wrote Pay\.map\.mjs/);
 });
 
+test("statechart.mjs refuses unrecorded TLC files and invalid ownership records", () => {
+  const dir = mkdtempSync(join(tmpdir(), "statechart-"));
+  writeFileSync(join(dir, "tla2tools.jar"), "");
+  writeFileSync(join(dir, "Pay.tla"), "---- MODULE Pay ----\n====\n");
+  writeFileSync(join(dir, "Pay.cfg"), "SPECIFICATION Spec\n");
+  const env = { TLA2TOOLS: join(dir, "tla2tools.jar") };
+  const out = join(dir, "out");
+  const tlc = join(out, "tlc");
+  for (const name of ["owner-notes.cfg", "owner-notes.out", "owner-notes.dot", "Checkout-backup.cfg"]) {
+    mkdirSync(tlc, { recursive: true });
+    writeFileSync(join(tlc, "Checkout.cfg"), "generated\n");
+    writeFileSync(join(tlc, ".written.json"), '["Checkout.cfg"]\n');
+    writeFileSync(join(tlc, name), "mine\n");
+    const r = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", out], dir, env);
+    assert.equal(r.status, 2, r.stderr);
+    assert.match(r.stderr, /did not write/);
+    assert.ok(r.stderr.includes(`tlc/${name}`), r.stderr);
+    assert.equal(readFileSync(join(tlc, name), "utf8"), "mine\n");
+    rmSync(out, { recursive: true });
+  }
+  for (const record of [null, "{", "{}", '["Pay.cfg", 1]']) {
+    mkdirSync(tlc, { recursive: true });
+    writeFileSync(join(tlc, "Pay.cfg"), "kept\n");
+    if (record !== null) writeFileSync(join(tlc, ".written.json"), record);
+    const r = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", out], dir, env);
+    assert.equal(r.status, 2, r.stderr);
+    assert.match(r.stderr, /did not write/);
+    assert.match(r.stderr, /--out with a new folder/);
+    assert.equal(readFileSync(join(tlc, "Pay.cfg"), "utf8"), "kept\n");
+    rmSync(out, { recursive: true });
+  }
+  for (const kind of ["directory", "symlink"]) {
+    mkdirSync(tlc, { recursive: true });
+    writeFileSync(join(tlc, ".written.json"), '["Pay.cfg"]\n');
+    if (kind === "directory") mkdirSync(join(tlc, "Pay.cfg"));
+    else symlinkSync(join(dir, "Pay.cfg"), join(tlc, "Pay.cfg"));
+    const r = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", out], dir, env);
+    assert.equal(r.status, 2, r.stderr);
+    assert.match(r.stderr, /did not write: tlc\/Pay.cfg/);
+    rmSync(out, { recursive: true });
+  }
+});
+
 test("statechart.mjs exits 2 and names a helper script that cannot start", () => {
   const dir = mkdtempSync(join(tmpdir(), "statechart-"));
   writeFileSync(join(dir, "notes-app.mmd"), fixture("sync.mmd"));
@@ -2810,6 +2856,36 @@ const writeLamp = (dir) => {
   return join(dir, "Lamp-statechart");
 };
 
+test("TLC reruns replace recorded files, remove old rule files, and preserve unrecorded files", needsTlc, () => {
+  const dir = mkdtempSync(join(tmpdir(), "statechart-"));
+  const out = writeLamp(dir);
+  const spec = readFileSync(join(dir, "Lamp.tla"), "utf8").replace(
+    "====",
+    "Safe == on \\in BOOLEAN\n====",
+  );
+  writeFileSync(join(dir, "Lamp.tla"), spec);
+  writeFileSync(join(dir, "Lamp.cfg"), "SPECIFICATION Spec\nINVARIANT Safe\n");
+  const run = () => node("statechart.mjs", ["from-spec", "Lamp.tla"], dir);
+  for (let i = 0; i < 2; i++) {
+    const r = run();
+    assert.equal(r.status, 0, r.stderr);
+    assert.ok(existsSync(join(out, "tlc", "Lamp-Safe.cfg")));
+  }
+  writeFileSync(join(dir, "Lamp.cfg"), "SPECIFICATION Spec\n");
+  const changed = run();
+  assert.equal(changed.status, 0, changed.stderr);
+  assert.equal(existsSync(join(out, "tlc", "Lamp-Safe.cfg")), false);
+  for (const name of ["owner-notes.cfg", "owner-notes.out", "owner-notes.dot", "Lamp-backup.cfg"]) {
+    const file = join(out, "tlc", name);
+    writeFileSync(file, "mine\n");
+    const r = run();
+    assert.equal(r.status, 2, r.stderr);
+    assert.match(r.stderr, /did not write/);
+    assert.equal(readFileSync(file, "utf8"), "mine\n");
+    rmSync(file);
+  }
+});
+
 test("a rerun without --png removes the chart.png of an earlier run", needsTlc, () => {
   const dir = mkdtempSync(join(tmpdir(), "statechart-"));
   const out = writeLamp(dir);