pelikhan · Oct 10, 2026 · Oct 10, 2026 · Oct 10, 2026 · Oct 10, 2026 · Oct 10, 2026
diff --git a/.github/scripts/work-queue-formal-check.cjs b/.github/scripts/work-queue-formal-check.cjs
@@ -15,6 +15,19 @@ function writeJSON(file, value) {
   fs.writeFileSync(file, `${JSON.stringify(value, null, 2)}\n`);
 }
 
+function readFileDescriptor(fd) {
+  const { size } = fs.fstatSync(fd);
+  if (size === 0) return "";
+  const buffer = Buffer.alloc(size);
+  const bytesRead = fs.readSync(fd, buffer, 0, size, 0);
+  return buffer.subarray(0, bytesRead).toString("utf8");
+}
+
+function writeJSONToFileDescriptor(fd, value) {
+  fs.ftruncateSync(fd, 0);
+  fs.writeSync(fd, `${JSON.stringify(value, null, 2)}\n`, 0, "utf8");
+}
+
 function classify(exitCode, signal, timedOut, log) {
   if (timedOut) return "timed_out";
   if (exitCode === 0 && !signal && log.includes("Model checking completed. No error has been found.") && /(?:^|\n)\d+ states generated, \d+ distinct states found, 0 states left on queue\.(?:\r?\n|$)/.test(log)) return "passed";
@@ -162,8 +175,8 @@ async function runVerification(options) {
   fs.writeFileSync(path.join(bundleDir, "java-version.txt"), `${version.stdout || ""}${version.stderr || ""}`);
   const logPath = path.join(bundleDir, "tlc.log");
   const reservePath = path.join(outputDir, "result-space.reserve");
-  fs.writeFileSync(reservePath, Buffer.alloc(1024 * 1024));
-  const fd = fs.openSync(logPath, "w");
+  fs.writeFileSync(reservePath, Buffer.alloc(1024 * 1024), { flag: "wx", mode: 0o600 });
+  const fd = fs.openSync(logPath, "wx+", 0o600);
   let timedOut = false;
   let spawnError = null;
   /** @type {NodeJS.Timeout | undefined} */
@@ -191,14 +204,17 @@ async function runVerification(options) {
   });
   clearTimeout(timer);
   clearTimeout(killTimer);
-  fs.closeSync(fd);
   let log;
   let checkpoints;
   try {
-    log = fs.readFileSync(logPath, "utf8");
+    log = readFileDescriptor(fd);
     checkpoints = checkpointBundle(stateDir, bundleDir, options.checkpointMaxBytes ?? CHECKPOINT_MAX_BYTES, log.includes("Checkpointing completed"), env);
   } finally {
-    fs.unlinkSync(reservePath);
+    try {
+      fs.closeSync(fd);
+    } finally {
+      fs.unlinkSync(reservePath);
+    }
   }
   const finished = lastMatch(log, /(\d+) states generated, (\d+) distinct states found, (\d+) states left on queue\./g);
   const progress = lastMatch(log, /Progress\((\d+)\).*?: ([\d,]+) states generated.*?, ([\d,]+) distinct states found.*?, ([\d,]+) states left on queue\./g);
@@ -261,9 +277,27 @@ if (require.main === module) {
       console.error(`Formal verification collection failed: ${error.message}`);
       const outputDir = process.env.RESULTS_DIR || "";
       const resultPath = path.join(outputDir, "bundle", "result.json");
-      if (path.isAbsolute(outputDir) && path.resolve(outputDir) !== path.parse(outputDir).root && fs.existsSync(resultPath)) {
-        const result = JSON.parse(fs.readFileSync(resultPath, "utf8"));
-        writeJSON(resultPath, { ...result, status: "tool_error", exhausted: false, error: error.message, finished_at: new Date().toISOString() });
+      if (path.isAbsolute(outputDir) && path.resolve(outputDir) !== path.parse(outputDir).root) {
+        let resultFd;
+        try {
+          resultFd = fs.openSync(resultPath, "r+");
+        } catch (openError) {
+          if (!openError || openError.code !== "ENOENT") throw openError;
+        }
+        if (resultFd !== undefined) {
+          try {
+            const result = JSON.parse(readFileDescriptor(resultFd));
+            writeJSONToFileDescriptor(resultFd, {
+              ...result,
+              status: "tool_error",
+              exhausted: false,
+              error: error.message,
+              finished_at: new Date().toISOString(),
+            });
+          } finally {
+            fs.closeSync(resultFd);
+          }
+        }
       }
       process.exitCode = 1;
     });

diff --git a/.github/scripts/work-queue-formal-check.test.cjs b/.github/scripts/work-queue-formal-check.test.cjs
@@ -47,6 +47,12 @@ if (mode === "passed") {
 } else if (mode === "violation") {
   console.error("Error: Invariant Safety is violated.");
   process.exit(12);
+} else if (mode === "replace_log") {
+  const config = process.argv[process.argv.indexOf("-config") + 1];
+  const logPath = path.join(path.dirname(config), "tlc.log");
+  fs.unlinkSync(logPath);
+  fs.symlinkSync(process.env.FORMAL_TEST_REPLACEMENT_FILE, logPath);
+  process.stdout.write(${JSON.stringify(SUCCESS)});
 } else if (mode === "invariant_false") {
   process.stderr.write(${JSON.stringify(INVARIANT_FALSE)});
   process.exit(151);
@@ -107,6 +113,18 @@ test("only natural exit plus exhaustion is a pass", () => {
   assert.equal(classify(150, null, false, "Error: Parsing failed."), "tool_error");
 });
 
+test("log collection reads the opened file if its path is replaced", async t => {
+  const options = fixture(t);
+  const replacement = path.join(path.dirname(options.javaBin), "replacement.log");
+  fs.writeFileSync(replacement, "replacement content");
+  options.env.FORMAL_TEST_MODE = "replace_log";
+  options.env.FORMAL_TEST_REPLACEMENT_FILE = replacement;
+
+  const result = await runVerification(options);
+
+  assert.equal(result.status, "passed");
+});
+
 for (const { config, moduleName } of CONFIGS) {
   test(`${config}: successful run persists machine-readable evidence and exact sources`, async t => {
     const options = fixture(t, config);

diff --git a/pkg/workflow/maintenance_workflow_generation_fixes_test.go b/pkg/workflow/maintenance_workflow_generation_fixes_test.go
@@ -56,6 +56,33 @@ func TestMaintenanceWorkflowJobMetadata(t *testing.T) {
 	}
 }
 
+func TestMaintenanceWorkflowQuotesCompileGitHubToken(t *testing.T) {
+	token := "${{ secrets.MAINTENANCE_TOKEN }}: 'quoted' # comment \\\n  injected: true"
+	generated, err := buildMaintenanceWorkflowYAML(context.Background(), buildMaintenanceWorkflowYAMLOptions{
+		cronSchedule: "37 0 * * *", scheduleDesc: "Daily", runsOnValue: "ubuntu-slim",
+		actionMode: ActionModeDev, version: "dev", defaultBranch: "main",
+		compileGitHubToken: token,
+	})
+	require.NoError(t, err)
+
+	var doc struct {
+		Jobs map[string]struct {
+			Steps []struct {
+				Env map[string]string `yaml:"env"`
+			} `yaml:"steps"`
+		} `yaml:"jobs"`
+	}
+	require.NoError(t, yamlv3.Unmarshal([]byte(generated), &doc))
+	var got string
+	for _, step := range doc.Jobs["compile-workflows"].Steps {
+		if value, ok := step.Env["GH_AW_MAINTENANCE_GITHUB_TOKEN"]; ok {
+			got = value
+			break
+		}
+	}
+	require.Equal(t, token, got)
+}
+
 func TestMaintenanceWorkflowDisabledManualJobsAcceptedByConfig(t *testing.T) {
 	for _, job := range []string{
 		"run_operation", "cleanup-cache-memory", "update_pull_request_branches",

diff --git a/pkg/workflow/maintenance_workflow_triggers_test.go b/pkg/workflow/maintenance_workflow_triggers_test.go
@@ -233,7 +233,7 @@ func TestGenerateMaintenanceWorkflow_PushTrigger(t *testing.T) {
 		if strings.Contains(jobSection, "contents: write") {
 			t.Errorf("compile-workflows should not request contents: write in PR mode, got:\n%s", jobSection)
 		}
-		if !strings.Contains(yaml, "GH_AW_MAINTENANCE_GITHUB_TOKEN: ${{ secrets.MAINTENANCE_TOKEN }}") {
+		if !strings.Contains(yaml, `GH_AW_MAINTENANCE_GITHUB_TOKEN: "${{ secrets.MAINTENANCE_TOKEN }}"`) {
 			t.Errorf("workflow should use configured maintenance github token secret, got:\n%s", yaml)
 		}
 		if !strings.Contains(yaml, "github-token: ${{ env.GH_AW_MAINTENANCE_GITHUB_TOKEN }}") {

diff --git a/pkg/workflow/maintenance_workflow_yaml_jobs.go b/pkg/workflow/maintenance_workflow_yaml_jobs.go
@@ -651,9 +651,8 @@ func writeMaintenanceCompileWorkflowsTokenStep(b *strings.Builder, opts buildMai
         uses: ` + getCachedActionPinFromResolver("actions/github-script", opts.resolver) + `
 `)
 	if opts.compileGitHubToken != "" {
-		b.WriteString(`        env:
-          GH_AW_MAINTENANCE_GITHUB_TOKEN: ` + opts.compileGitHubToken + `
-`)
+		b.WriteString("        env:\n")
+		writeYAMLEnv(b, "          ", "GH_AW_MAINTENANCE_GITHUB_TOKEN", opts.compileGitHubToken)
 	}
 	b.WriteString(`        with:
 `)

diff --git a/specs/eslint-factory/trace.mjs b/specs/eslint-factory/trace.mjs
@@ -193,9 +193,14 @@ export function validateTrace(trace, entry) {
 
 export function readableTrace(trace, entry) {
   const lines = [`# ${entry.name}`, "", `Expected TLC diagnostic: \`${entry.expected}\`.`, "", "| State | Transition | Original | Phase | Proposed / applied | Readback | Scan / flag | Quality |", "|---|---|---|---|---|---|---|---|"];
-  for (const { number, action, state: s } of trace)
-    lines.push(
-      `| ${number} | ${action.replace(/\|/g, "\\|")} | ${s.original.join(",") || "none"} | ${s.phase.join(", ")} | ${s.proposed.join(",")} / ${s.applied.join(",")} | ${s.verified.join(",")} | ${s.scan} / ${s.lintClean} | ${s.quality} |`
-    );
+  const escapeCell = value =>
+    String(value)
+      .replaceAll("\\", "\\\\")
+      .replaceAll("|", "\\|")
+      .replace(/\r\n|\n|\r/g, "<br>");
+  for (const { number, action, state: s } of trace) {
+    const cells = [number, action, s.original.join(",") || "none", s.phase.join(", "), `${s.proposed.join(",")} / ${s.applied.join(",")}`, s.verified.join(","), `${s.scan} / ${s.lintClean}`, s.quality];
+    lines.push(`| ${cells.map(escapeCell).join(" | ")} |`);
+  }
   return lines.join("\n") + "\n";
 }
diff --git a/specs/eslint-factory/trace.test.mjs b/specs/eslint-factory/trace.test.mjs
@@ -0,0 +1,29 @@
+import assert from "node:assert/strict";
+import { test } from "node:test";
+import { readableTrace } from "./trace.mjs";
+
+test("readable traces escape every cell delimiter and line break", () => {
+  const trace = [
+    {
+      number: 1,
+      action: "Transition | one\nsecond line",
+      state: {
+        original: ["item|one"],
+        phase: ["scan"],
+        proposed: ["candidate"],
+        applied: ["candidate"],
+        verified: ["readback"],
+        scan: "clean",
+        lintClean: ["clean"],
+        quality: "good\\value",
+      },
+    },
+  ];
+
+  const output = readableTrace(trace, { name: "fixture", expected: "NeverWitness" });
+
+  assert.match(output, /Transition \\| one<br>second line/);
+  assert.match(output, /item\\\|one/);
+  assert.match(output, /good\\\\value/);
+  assert.equal(output.split("\n").filter(line => line.startsWith("| 1 |")).length, 1);
+});
diff --git a/specs/work-queue/compare-evaluation.mjs b/specs/work-queue/compare-evaluation.mjs
@@ -16,10 +16,17 @@ const java = process.env.JAVA_BIN || "java";
 const jar = process.env.TLA2TOOLS_JAR;
 assert(jar && path.isAbsolute(jar), "TLA2TOOLS_JAR must be an absolute pinned jar path");
 const hash = value => crypto.createHash("sha256").update(value).digest("hex");
+const readFileDescriptor = fd => {
+  const { size } = fs.fstatSync(fd);
+  if (size === 0) return "";
+  const buffer = Buffer.alloc(size);
+  const bytesRead = fs.readSync(fd, buffer, 0, size, 0);
+  return buffer.subarray(0, bytesRead).toString("utf8");
+};
 assert.equal(hash(fs.readFileSync(jar)), TLC_SHA256, "unexpected TLC jar checksum");
 assert.notEqual(output, path.parse(output).root, "results must not be the filesystem root");
 fs.mkdirSync(output, { recursive: true });
-assert(!fs.existsSync(path.join(output, "comparison.json")), "do not overwrite previous comparison evidence");
+const comparisonFd = fs.openSync(path.join(output, "comparison.json"), "wx", 0o600);
 const cases = [
   ["WorkQueue", "Recovery"],
   ["FairWorkQueue", "FairBatch"],
@@ -118,10 +125,10 @@ WorkResubmissionNoOp == Original!WorkResubmissionNoOp /\\ Revised!WorkResubmissi
   const command = ["-XX:+UseParallelGC", "-Xmx1g", "-cp", jar, "tlc2.TLC", "-workers", "2", "-seed", "1", "-fp", "0", "-config", "Comparison.cfg", "-metadir", "state", "Comparison.tla"];
   const started = Date.now();
   const logPath = path.join(directory, "tlc.log");
-  const fd = fs.openSync(logPath, "w");
+  const fd = fs.openSync(logPath, "wx+", 0o600);
   const checked = spawnSync(java, command, { cwd: directory, timeout: 900_000, killSignal: "SIGINT", stdio: ["ignore", fd, fd] });
+  const log = readFileDescriptor(fd);
   fs.closeSync(fd);
-  const log = fs.readFileSync(logPath, "utf8");
   const diagnostic = mutation === "missing-transition" ? "Action property NextEquivalence is violated" : mutation === "changed-normalization" ? "Invariant ReplayEquivalence is violated" : null;
   const expectedExit = mutation === "missing-transition" ? 13 : mutation ? 12 : 0;
   const status = classify(checked.status, checked.signal, checked.error?.code === "ETIMEDOUT", log);
@@ -148,10 +155,14 @@ WorkResubmissionNoOp == Original!WorkResubmissionNoOp /\\ Revised!WorkResubmissi
   };
   comparisons.push(result);
   const complete = comparisons.length === cases.length;
-  fs.writeFileSync(
-    path.join(output, "comparison.json"),
-    `${JSON.stringify({ complete, passed: complete && comparisons.every(c => c.passed), java_version: javaVersion.stderr, runner_sha256: hash(fs.readFileSync(fileURLToPath(import.meta.url))), comparisons }, null, 2)}\n`
+  fs.ftruncateSync(comparisonFd, 0);
+  fs.writeSync(
+    comparisonFd,
+    `${JSON.stringify({ complete, passed: complete && comparisons.every(c => c.passed), java_version: javaVersion.stderr, runner_sha256: hash(fs.readFileSync(fileURLToPath(import.meta.url))), comparisons }, null, 2)}\n`,
+    0,
+    "utf8"
   );
   console.log(`${name}: ${result.passed ? "expected result" : "FAILED"} (${result.elapsed_seconds}s)`);
   assert(result.passed, `comparison failed; inspect ${logPath}`);
 }
+fs.closeSync(comparisonFd);
diff --git a/specs/work-queue/native_probe.cjs b/specs/work-queue/native_probe.cjs
@@ -63,8 +63,13 @@ function execute(input) {
   }
   let data = input.data;
   if (input.ledger_file) {
-    if (fs.statSync(input.ledger_file).size > 80 * 1024 * 1024) throw new Error("resource_limit: adapter input exceeds 80 MiB");
-    data = fs.readFileSync(input.ledger_file, "utf8");
+    const fd = fs.openSync(input.ledger_file, "r");
+    try {
+      if (fs.fstatSync(fd).size > 80 * 1024 * 1024) throw new Error("resource_limit: adapter input exceeds 80 MiB");
+      data = fs.readFileSync(fd, "utf8");
+    } finally {
+      fs.closeSync(fd);
+    }
   }
   let start = performance.now();
   const commits = queue.parseTransactionLog(data);

diff --git a/specs/work-queue/verify_native_test.py b/specs/work-queue/verify_native_test.py
@@ -22,6 +22,20 @@
 
 
 class IndependentDriverTests(unittest.TestCase):
+    def test_native_adapter_rejects_oversized_ledger_from_open_file(self):
+        with tempfile.TemporaryDirectory() as directory:
+            ledger = Path(directory) / "ledger.jsonl"
+            with ledger.open("wb") as stream:
+                stream.truncate(80 * 1024 * 1024 + 1)
+            result = subprocess.run(
+                ["node", str(Path(__file__).with_name("native_probe.cjs"))],
+                input=json.dumps({"action": "benchmark", "ledger_file": str(ledger)}) + "\n",
+                text=True,
+                capture_output=True,
+                check=True,
+            )
+            self.assertEqual(json.loads(result.stdout)["error"], "resource_limit: adapter input exceeds 80 MiB")
+
     def test_conformance_refuses_missing_positive_before_native_execution(self):
         path = verify.ROOT / "actions/setup/js/work_queue_worker_child_fixtures.json"
         original = path.read_bytes()