diff --git a/harness/pstack/claude-code/skills/statechart/scripts/statechart-help.mjs b/harness/pstack/claude-code/skills/statechart/scripts/statechart-help.mjs
index 1a900fc51..54e22875b 100644
--- a/harness/pstack/claude-code/skills/statechart/scripts/statechart-help.mjs
+++ b/harness/pstack/claude-code/skills/statechart/scripts/statechart-help.mjs
@@ -143,7 +143,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 draw each chart as a PNG. The PNG section tells how.
   --theme NAME       The colors of each PNG: light, dark, or classic. Default: light. It needs
@@ -279,7 +280,8 @@ Reading a chart
 
 Regenerate
   List every rule that is known to break with --expect-broken, the goals and the known bugs. Each
-  run then exits 0 until a rule changes, so one script rebuilds every chart and stops on any change:
+  run then exits 0 until a rule changes, so one script rebuilds every chart and stops when a rule
+  breaks or heals (a chart that only redraws does not stop it):
     set -e
     node statechart.mjs from-spec Code.tla --against Agreed.tla --expect-broken NoLostUpload --png
   A run that leaves a broken rule out of --expect-broken exits 1, and set -e stops the script there.
diff --git a/harness/pstack/claude-code/skills/statechart/scripts/statechart.mjs b/harness/pstack/claude-code/skills/statechart/scripts/statechart.mjs
index 555f10b8c..fb1696ab9 100644
--- a/harness/pstack/claude-code/skills/statechart/scripts/statechart.mjs
+++ b/harness/pstack/claude-code/skills/statechart/scripts/statechart.mjs
@@ -548,6 +548,8 @@ function render(charts, { lib, theme }, shown) {
 function finish({ work, out, inputs }, { files, charts }, ok, renderer) {
   unchanged(inputs, out);
   const pngs = renderer ? render(charts, renderer, published(work, out)) : [];
+  const tlc = path.join(work, "tlc");
+  fs.writeFileSync(path.join(tlc, WRITTEN), `${JSON.stringify(filesUnder(tlc))}\n`);
   publish(work, out, inputs);
   const written = [...charts, ...pngs, files.stories, files.summary]
     .map((f) => path.basename(f))
@@ -579,14 +581,59 @@ function renderFile(input, flags, { lib, theme }) {
 const published = (work, out) => (file) => rel(path.join(out, path.relative(work, file)));
 
 const OWN =
-  /^((chart|bug-\d+(-developer|-layered)?)\.(mmd|png)|stories\.md|summary\.json|tlc|\.DS_Store)$/;
+  /^((chart|bug-\d+(-developer|-layered)?)\.(mmd|png)|stories\.md|summary\.json|\.DS_Store)$/;
+const WRITTEN = ".written.json";
+
+// The regular files under `dir`, as paths relative to it with / separators, in a stable order.
+// A comparing run writes into tlc/fixed/ or tlc/against/, so the record has to reach below the
+// first level.
+function filesUnder(dir, prefix = "") {
+  const found = [];
+  for (const entry of fs.readdirSync(dir, { withFileTypes: true }).sort((a, b) =>
+    a.name.localeCompare(b.name),
+  )) {
+    const at = `${prefix}${entry.name}`;
+    if (entry.isDirectory()) found.push(...filesUnder(path.join(dir, entry.name), `${at}/`));
+    else if (entry.isFile() && at !== WRITTEN) found.push(at);
+  }
+  return found;
+}
+
+// Everything under tlc/ that the previous run did not record. Without a valid record every entry
+// is foreign: an output folder from before the record existed needs a new --out folder, which is
+// cheaper than guessing which of its files were the user's.
+function foreignTlc(dir) {
+  let written;
+  try {
+    written = JSON.parse(fs.readFileSync(path.join(dir, WRITTEN), "utf8"));
+  } catch {}
+  const own = new Set([".DS_Store", WRITTEN]);
+  if (Array.isArray(written) && written.every((f) => typeof f === "string"))
+    for (const f of written) own.add(f);
+  const found = [];
+  const walk = (at, prefix) => {
+    for (const entry of fs.readdirSync(at, { withFileTypes: true })) {
+      const name = `${prefix}${entry.name}`;
+      if (entry.isDirectory()) {
+        // A folder is the run's own only when it holds something the run recorded.
+        if ([...own].some((f) => f.startsWith(`${name}/`))) walk(path.join(at, entry.name), `${name}/`);
+        else found.push(`tlc/${name}`);
+      } else if (!(entry.isFile() && own.has(name))) found.push(`tlc/${name}`);
+    }
+  };
+  walk(dir, "");
+  return found;
+}
 
 function foreign(dir) {
   try {
-    return fs
-      .readdirSync(dir)
-      .filter((f) => !OWN.test(f))
-      .sort();
+    const found = [];
+    for (const entry of fs.readdirSync(dir, { withFileTypes: true })) {
+      if (entry.name === "tlc" && entry.isDirectory()) {
+        found.push(...foreignTlc(path.join(dir, "tlc")));
+      } else if (!(entry.isFile() && OWN.test(entry.name))) found.push(entry.name);
+    }
+    return found.sort();
   } catch (e) {
     if (e.code === "ENOENT") return [];
     throw new CannotFinish(`cannot use ${rel(dir)} as the output folder: ${e.message}`);
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 543fe8d67..539e81850 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
@@ -1536,6 +1536,118 @@ test("statechart.mjs does not use an output folder that has files that it did no
   assert.equal(readFileSync(join(out, "chart.mmd"), "utf8"), "kept\n");
 });
 
+test("statechart.mjs refuses an output folder with foreign files under tlc/ or behind an owned name", () => {
+  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 refused = (out, expected) => {
+    const r = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", out], dir, env);
+    assert.equal(r.status, 2, r.stderr);
+    assert.equal(
+      r.stderr,
+      `${out} has a file that this command did not write: ${expected}. A run puts its files in place of the whole output folder, so pass --out with a new folder.\n`,
+    );
+  };
+
+  // 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");
+
+  // A folder that carries the name of a generated file.
+  mkdirSync(join(dir, "typed", "chart.mmd"), { recursive: true });
+  writeFileSync(join(dir, "typed", "chart.mmd", "notes.md"), "mine\n");
+  refused("typed", "chart.mmd");
+
+  // The same with the ignored Finder file.
+  mkdirSync(join(dir, "finder", ".DS_Store"), { recursive: true });
+  writeFileSync(join(dir, "finder", ".DS_Store", "notes.md"), "mine\n");
+  refused("finder", ".DS_Store");
+
+  // A link under an owned name is not the run's file either.
+  mkdirSync(join(dir, "linked"));
+  writeFileSync(join(dir, "elsewhere.mmd"), "theirs\n");
+  symlinkSync(join(dir, "elsewhere.mmd"), join(dir, "linked", "chart.mmd"));
+  refused("linked", "chart.mmd");
+  assert.equal(readFileSync(join(dir, "elsewhere.mmd"), "utf8"), "theirs\n");
+
+  // The run's own files, including the whole of tlc/, still pass.
+  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), "");
+  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 });
+  }
+  // A comparing run writes into tlc/fixed/ or tlc/against/. Recorded files there pass; a file the
+  // record does not name, or a folder with nothing recorded in it, is reported by its full path.
+  mkdirSync(join(tlc, "fixed"), { recursive: true });
+  writeFileSync(join(tlc, "Pay.cfg"), "generated\n");
+  writeFileSync(join(tlc, "fixed", "Pay.cfg"), "generated\n");
+  writeFileSync(join(tlc, ".written.json"), '["Pay.cfg", "fixed/Pay.cfg"]\n');
+  const nested = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", out], dir, env);
+  assert.doesNotMatch(nested.stderr, /did not write/, nested.stderr);
+  writeFileSync(join(tlc, "fixed", "Pay-backup.cfg"), "mine\n");
+  mkdirSync(join(tlc, "scratch"));
+  const nestedForeign = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", out], dir, env);
+  assert.equal(nestedForeign.status, 2, nestedForeign.stderr);
+  assert.match(nestedForeign.stderr, /2 files that this command did not write, such as tlc\/fixed\/Pay-backup\.cfg/);
+  assert.equal(readFileSync(join(tlc, "fixed", "Pay-backup.cfg"), "utf8"), "mine\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"));
@@ -5844,6 +5956,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-help.mjs b/pstack/skills/statechart/scripts/statechart-help.mjs
index 1a900fc51..54e22875b 100644
--- a/pstack/skills/statechart/scripts/statechart-help.mjs
+++ b/pstack/skills/statechart/scripts/statechart-help.mjs
@@ -143,7 +143,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 draw each chart as a PNG. The PNG section tells how.
   --theme NAME       The colors of each PNG: light, dark, or classic. Default: light. It needs
@@ -279,7 +280,8 @@ Reading a chart
 
 Regenerate
   List every rule that is known to break with --expect-broken, the goals and the known bugs. Each
-  run then exits 0 until a rule changes, so one script rebuilds every chart and stops on any change:
+  run then exits 0 until a rule changes, so one script rebuilds every chart and stops when a rule
+  breaks or heals (a chart that only redraws does not stop it):
     set -e
     node statechart.mjs from-spec Code.tla --against Agreed.tla --expect-broken NoLostUpload --png
   A run that leaves a broken rule out of --expect-broken exits 1, and set -e stops the script there.
diff --git a/pstack/skills/statechart/scripts/statechart.mjs b/pstack/skills/statechart/scripts/statechart.mjs
index 555f10b8c..fb1696ab9 100644
--- a/pstack/skills/statechart/scripts/statechart.mjs
+++ b/pstack/skills/statechart/scripts/statechart.mjs
@@ -548,6 +548,8 @@ function render(charts, { lib, theme }, shown) {
 function finish({ work, out, inputs }, { files, charts }, ok, renderer) {
   unchanged(inputs, out);
   const pngs = renderer ? render(charts, renderer, published(work, out)) : [];
+  const tlc = path.join(work, "tlc");
+  fs.writeFileSync(path.join(tlc, WRITTEN), `${JSON.stringify(filesUnder(tlc))}\n`);
   publish(work, out, inputs);
   const written = [...charts, ...pngs, files.stories, files.summary]
     .map((f) => path.basename(f))
@@ -579,14 +581,59 @@ function renderFile(input, flags, { lib, theme }) {
 const published = (work, out) => (file) => rel(path.join(out, path.relative(work, file)));
 
 const OWN =
-  /^((chart|bug-\d+(-developer|-layered)?)\.(mmd|png)|stories\.md|summary\.json|tlc|\.DS_Store)$/;
+  /^((chart|bug-\d+(-developer|-layered)?)\.(mmd|png)|stories\.md|summary\.json|\.DS_Store)$/;
+const WRITTEN = ".written.json";
+
+// The regular files under `dir`, as paths relative to it with / separators, in a stable order.
+// A comparing run writes into tlc/fixed/ or tlc/against/, so the record has to reach below the
+// first level.
+function filesUnder(dir, prefix = "") {
+  const found = [];
+  for (const entry of fs.readdirSync(dir, { withFileTypes: true }).sort((a, b) =>
+    a.name.localeCompare(b.name),
+  )) {
+    const at = `${prefix}${entry.name}`;
+    if (entry.isDirectory()) found.push(...filesUnder(path.join(dir, entry.name), `${at}/`));
+    else if (entry.isFile() && at !== WRITTEN) found.push(at);
+  }
+  return found;
+}
+
+// Everything under tlc/ that the previous run did not record. Without a valid record every entry
+// is foreign: an output folder from before the record existed needs a new --out folder, which is
+// cheaper than guessing which of its files were the user's.
+function foreignTlc(dir) {
+  let written;
+  try {
+    written = JSON.parse(fs.readFileSync(path.join(dir, WRITTEN), "utf8"));
+  } catch {}
+  const own = new Set([".DS_Store", WRITTEN]);
+  if (Array.isArray(written) && written.every((f) => typeof f === "string"))
+    for (const f of written) own.add(f);
+  const found = [];
+  const walk = (at, prefix) => {
+    for (const entry of fs.readdirSync(at, { withFileTypes: true })) {
+      const name = `${prefix}${entry.name}`;
+      if (entry.isDirectory()) {
+        // A folder is the run's own only when it holds something the run recorded.
+        if ([...own].some((f) => f.startsWith(`${name}/`))) walk(path.join(at, entry.name), `${name}/`);
+        else found.push(`tlc/${name}`);
+      } else if (!(entry.isFile() && own.has(name))) found.push(`tlc/${name}`);
+    }
+  };
+  walk(dir, "");
+  return found;
+}
 
 function foreign(dir) {
   try {
-    return fs
-      .readdirSync(dir)
-      .filter((f) => !OWN.test(f))
-      .sort();
+    const found = [];
+    for (const entry of fs.readdirSync(dir, { withFileTypes: true })) {
+      if (entry.name === "tlc" && entry.isDirectory()) {
+        found.push(...foreignTlc(path.join(dir, "tlc")));
+      } else if (!(entry.isFile() && OWN.test(entry.name))) found.push(entry.name);
+    }
+    return found.sort();
   } catch (e) {
     if (e.code === "ENOENT") return [];
     throw new CannotFinish(`cannot use ${rel(dir)} as the output folder: ${e.message}`);
diff --git a/pstack/skills/statechart/scripts/test/statechart.test.mjs b/pstack/skills/statechart/scripts/test/statechart.test.mjs
index 543fe8d67..539e81850 100644
--- a/pstack/skills/statechart/scripts/test/statechart.test.mjs
+++ b/pstack/skills/statechart/scripts/test/statechart.test.mjs
@@ -1536,6 +1536,118 @@ test("statechart.mjs does not use an output folder that has files that it did no
   assert.equal(readFileSync(join(out, "chart.mmd"), "utf8"), "kept\n");
 });
 
+test("statechart.mjs refuses an output folder with foreign files under tlc/ or behind an owned name", () => {
+  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 refused = (out, expected) => {
+    const r = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", out], dir, env);
+    assert.equal(r.status, 2, r.stderr);
+    assert.equal(
+      r.stderr,
+      `${out} has a file that this command did not write: ${expected}. A run puts its files in place of the whole output folder, so pass --out with a new folder.\n`,
+    );
+  };
+
+  // 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");
+
+  // A folder that carries the name of a generated file.
+  mkdirSync(join(dir, "typed", "chart.mmd"), { recursive: true });
+  writeFileSync(join(dir, "typed", "chart.mmd", "notes.md"), "mine\n");
+  refused("typed", "chart.mmd");
+
+  // The same with the ignored Finder file.
+  mkdirSync(join(dir, "finder", ".DS_Store"), { recursive: true });
+  writeFileSync(join(dir, "finder", ".DS_Store", "notes.md"), "mine\n");
+  refused("finder", ".DS_Store");
+
+  // A link under an owned name is not the run's file either.
+  mkdirSync(join(dir, "linked"));
+  writeFileSync(join(dir, "elsewhere.mmd"), "theirs\n");
+  symlinkSync(join(dir, "elsewhere.mmd"), join(dir, "linked", "chart.mmd"));
+  refused("linked", "chart.mmd");
+  assert.equal(readFileSync(join(dir, "elsewhere.mmd"), "utf8"), "theirs\n");
+
+  // The run's own files, including the whole of tlc/, still pass.
+  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), "");
+  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 });
+  }
+  // A comparing run writes into tlc/fixed/ or tlc/against/. Recorded files there pass; a file the
+  // record does not name, or a folder with nothing recorded in it, is reported by its full path.
+  mkdirSync(join(tlc, "fixed"), { recursive: true });
+  writeFileSync(join(tlc, "Pay.cfg"), "generated\n");
+  writeFileSync(join(tlc, "fixed", "Pay.cfg"), "generated\n");
+  writeFileSync(join(tlc, ".written.json"), '["Pay.cfg", "fixed/Pay.cfg"]\n');
+  const nested = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", out], dir, env);
+  assert.doesNotMatch(nested.stderr, /did not write/, nested.stderr);
+  writeFileSync(join(tlc, "fixed", "Pay-backup.cfg"), "mine\n");
+  mkdirSync(join(tlc, "scratch"));
+  const nestedForeign = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", out], dir, env);
+  assert.equal(nestedForeign.status, 2, nestedForeign.stderr);
+  assert.match(nestedForeign.stderr, /2 files that this command did not write, such as tlc\/fixed\/Pay-backup\.cfg/);
+  assert.equal(readFileSync(join(tlc, "fixed", "Pay-backup.cfg"), "utf8"), "mine\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"));
@@ -5844,6 +5956,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);