feat(formal): TLA+ model of the repo run cell lifecycle; fix duplicate-cell plans and mixed-execution rows

.github/.licenserc.yaml

@@ -66,6 +66,9 @@ header:
     # CHANGELOG.md, which carries the header itself.
     - 'dokimi/changelog.d/[0-9]*.md'
     - 'dokimi/changelog.d/fragment_template.md.j2'
+    # TLA+ specs and TLC configs carry the header in TLA+ comments, a style eyes does not know.
+    - 'dokimi/formal/**/*.tla'
+    - 'dokimi/formal/**/*.cfg'
     # Third-party eval files copied unchanged, under their own licenses
     # (dokimi/tests/fixtures/task_formats/MANIFEST.yaml, LICENSES/).
     - 'dokimi/tests/fixtures/task_formats/**'

dokimi/changelog.d/20261111_180000_napetrov_repo-batch-lifecycle.md

@@ -0,0 +1,20 @@
+### Fixed
+
+- **`repo run` refuses a plan that names one cell twice** — a repeated `--task` or `--model`, or two
+  names that share one cell directory (`a/b` and `a:b`), put two runs in one cell directory; with
+  `--jobs 2` each removed the other's files and `result.json` sat beside the other attempt's
+  `meta.json` and answer. The run now stops before any agent starts, naming the cell. Names that
+  differ only in case are refused on every system, since they share one directory on a
+  case-insensitive volume.
+- **`repo report` and `repo compare` refuse an arm and model whose cells hold two executions** — a
+  `--force` run with another execution that stopped part way (Ctrl-C, a crash, a failed cell), or a
+  harness binary replaced while the batch ran, left cells of two executions that were pooled in one
+  row. A batch that reported before can now be refused; the message names both ids, and a `--force`
+  run over every arm and model of the batch with the same `--task` and `--reps` clears it. `repo compare` checks only the rows it compares.
+
+### Added
+
+- **`formal/repo_batch`: a TLA+ model of the `repo run` cell lifecycle** — retries, crashes,
+  resume, `--force`, Ctrl-C and what the report counts, with TLC configs for the code before the
+  fixes, the fixed code, four mutations, a run without fairness and four vacuity witnesses;
+  `run.sh` checks each against its expected result.

dokimi/docs/repo-evaluation-contract.md

@@ -2309,7 +2309,14 @@ python cli.py repo compare repo-runs/authoring --baseline guidance:none --metric
   still run; the file is left in place, and removing it or `--force` runs the
   cell again. The same holds for a finished cell of a task this host cannot
   run, except that `--force` keeps it: once its file is removed, the cell runs
-  on a host that meets the task's requirements. A batch stays on the eval tree it
+  on a host that meets the task's requirements. A `--force` run that stops part
+  way (Ctrl-C, a crash, a failed cell), or a harness binary replaced while the
+  batch runs, can leave finished cells of two `id`s in one arm and model; `repo
+  report` refuses such a batch and `repo compare` such a compared row, naming
+  both `id`s, until a `--force` run over every arm and model of the batch (the same `--task` and `--reps`) reruns them. A plan naming one cell twice (a
+  repeated `--task` or `--model`, or two `--model` strings with one directory
+  name, `a/b` and `a:b`, or names that differ only in case) is refused before any agent starts.
+  Ctrl-C lets the running cells finish and starts no queued one. A batch stays on the eval tree it
   started with: its revision, or for a working tree the digests of its `eval_dir`
   and of the image build context. A batch with a task that
   names a `dokimi:` grader (or a task directory that cannot be read) also stays on the built-in graders' sources.

dokimi/dokimi/repos/compare.py

@@ -124,7 +124,7 @@
 from .compare_tasks import CompareError, select_tasks
 from .compare_values import finite_values, task_values
 from .process_counts import as_measure, process_order, process_values
-from .report import (load_cells, mismatch_warnings, model_mismatch, resolved_models,
+from .report import (load_cells, mismatch_warnings, model_mismatch, refuse_mixed_executions, resolved_models,
                      unmeasured_note, uptake_counts)
 from .useful import USEFUL_MEASURES, useful_arms_line, useful_counts
 
@@ -204,6 +204,7 @@ def compare(batch_dirs: list[Path], baseline: str, treatments: list[str] | None
     treatments = _treatments(cells, baseline, base_sel, treatments, scope)
     compared = _in_models([c for c in cells if any(selector_matches(parse_selector(t), c) for t in [baseline, *treatments])],
                           models)  # a judged-recall file of an excluded arm or model does not count
+    refuse_mixed_executions(compared, "batch")  # only the rows compared: a mixed arm left out does not block
     check_reported(metrics, compared, scope)
     measures = ["gate", "score", *([f"pass^{pass_k}"] if pass_k else []),
                 *(["path_distance"] if path_stability else []), "cost_usd", "turns", "first_prompt_tokens",

dokimi/dokimi/repos/report.py

@@ -63,6 +63,7 @@
 from dokimi.utils import same_model
 
 from .grading import SCORE_BOUND, read_grade_json
+from .batch_ledger import recorded_execution
 from .process_counts import process_line, process_means
 from .runner import UNSUPPORTED_FILE, slug
 from .useful import useful_line, useful_summary
@@ -175,6 +176,8 @@ def _check_cell(path: Path, rec: dict[str, Any]) -> None:
     for key in ("task", "arm", "model"):
         if not isinstance(rec.get(key), str):
             raise CellFileError(f"{path} has no usable `{key}`")
+    if "batch" in rec and not isinstance(rec["batch"], str):
+        raise CellFileError(f"{path} has no usable `batch`")
 
 
 def load_cells(batch_dir: Path) -> tuple[list[dict[str, Any]], list[str]]:
@@ -198,6 +201,20 @@ def load_cells(batch_dir: Path) -> tuple[list[dict[str, Any]], list[str]]:
     return finished, sorted((planned | started) - done - unsupported)
 
 
+def refuse_mixed_executions(cells: list[dict[str, Any]], where: str) -> None:
+    """One (batch, arm, model) ran with one execution: a ``--force`` run that stopped part way, or a harness
+    binary replaced mid-batch, leaves two, and pooling them would blend two setups in one row."""
+    seen: dict[tuple[str, str, str], set[str]] = defaultdict(set)
+    for rec in cells:
+        ran = recorded_execution(rec).get("id")
+        seen[(rec.get("batch", ""), rec["arm"], rec["model"])].add(ran if isinstance(ran, str) else "unrecorded")
+    for (batch, arm, model), ids in sorted(seen.items()):
+        if len(ids) > 1:
+            raise CellFileError(f"{batch or where}: the cells of arm {arm}, model {model} ran with executions "
+                                f"{', '.join(sorted(ids))}; rerun every arm and model of the batch with --force and the batch's --task and "
+                                "--reps, so every cell has one execution, or use another --batch")
+
+
 def load_unsupported(batch_dir: Path) -> list[dict[str, Any]]:
     """Cells the runner did not run on a host that missed their task's ``host`` requirements."""
     out = []
@@ -212,6 +229,7 @@ def load_unsupported(batch_dir: Path) -> list[dict[str, Any]]:
 
 def summarize(batch_dir: Path) -> dict[str, Any]:
     cells, missing = load_cells(batch_dir)
+    refuse_mixed_executions(cells, str(batch_dir))
     groups: dict[tuple[str, str, str], list[dict[str, Any]]] = defaultdict(list)
     for rec in cells:
         groups[(rec["task"], rec["arm"], rec["model"])].append(rec)

dokimi/dokimi/repos/runner.py

@@ -40,7 +40,8 @@
 import sys
 import threading
 import uuid
-from collections.abc import Iterator
+from collections import Counter
+from collections.abc import Callable, Iterator
 from concurrent.futures import ThreadPoolExecutor
 from dataclasses import dataclass
 from pathlib import Path
@@ -372,6 +373,7 @@ def run_batch(ctx: EvalContext, tasks: list[Task], arms: list[str], options: lis
     that cell's error."""
     validate_tasks(tasks)
     cells = [(t, a, o, r) for t in tasks for a in arms for o in options for r in range(1, reps + 1)]
+    _refuse_shared_cells(cells)
     check_batch_executions(batch_dir, options, {cell_name(t.id, a, o.model, r) for t, a, o, r in cells} if force else None)
     host = probe_host(ctx, batch_dir / "_eval")
     _write_json(batch_dir / "_eval" / "host.json", host)
@@ -428,14 +430,39 @@ def one(cell: tuple[Task, str, AgentOptions, int]) -> None:
             state["spent"] += rec["agent"].get("charged_usd", rec["agent"]["cost_usd"]) or 0.0
         _log_cell(log, name, rec)
 
-    with ThreadPoolExecutor(max(1, jobs)) as pool:
-        list(pool.map(one, cells))
+    _map_cells(one, cells, jobs)
     return {"cells": len(cells), "ran": state["ran"], "skipped": state["skipped"],
             "errors": state["errors"], "budget_stopped": state["budget_stopped"],
             "unsupported": state["unsupported"], "unsupported_tasks": unsupported, "probe_failed": probe_failed,
             "spent_usd": round(state["spent"], 6)}
 
 
+def _map_cells(one: Callable[[Any], None], cells: list[Any], jobs: int) -> None:
+    with ThreadPoolExecutor(max(1, jobs)) as pool:
+        try:
+            list(pool.map(one, cells))
+        except KeyboardInterrupt:
+            # pool.map submits every cell before it returns the iterator that cancels the queue, so an
+            # interrupt during submission would otherwise let the queued cells start while the pool exits.
+            pool.shutdown(wait=False, cancel_futures=True)
+            raise
+
+
+def _refuse_shared_cells(cells: list[tuple[Task, str, AgentOptions, int]]) -> None:
+    """Refuse a plan naming one cell directory twice, or two names one case-insensitive volume maps to one
+    directory: with --jobs 2 both would run in it and mix their files (or one would delete the other's)."""
+    names = Counter(cell_name(t.id, a, o.model, r) for t, a, o, r in cells)
+    problems = [f"cell {name} is planned {names[name]} times" for name in sorted(names) if names[name] > 1]
+    by_fold: dict[str, list[str]] = {}
+    for name in names:
+        by_fold.setdefault(name.casefold(), []).append(name)
+    problems += [f"cells {' and '.join(sorted(group))} are one directory on a case-insensitive volume"
+                 for group in by_fold.values() if len(group) > 1]
+    if problems:
+        raise ValueError("; ".join(problems) + " (a repeated --task or --model, two --model strings with one name "
+                         "on disk, or names that differ only in case); give each once")
+
+
 UNSUPPORTED_FILE = "unsupported.json"
 KEPT_HINT = ("this host cannot run the task, so --force keeps the file; remove it, and the cell runs on a host "
              "that meets the task's requirements")

dokimi/formal/repo_batch/.gitignore

@@ -0,0 +1,4 @@
+# Copyright (C) 2026 Intel Corporation
+# SPDX-License-Identifier: Apache-2.0
+out/
+RepoBatch_TTrace_*

dokimi/formal/repo_batch/EVALUATOR.md

@@ -0,0 +1,46 @@
+<!--
+Copyright (C) 2026 Intel Corporation
+SPDX-License-Identifier: Apache-2.0
+-->
+
+# Proposal: a model-checking grader for agent tasks
+
+Status: proposal, not implemented. It would be a `dokimi:` grader (like the built-in ones in
+`dokimi/repos/`) for tasks whose answer is a change to a system with a fixed formal spec.
+
+## Shape
+
+- **Input**: the task's fixed spec (a `.tla` module with the properties, plus one or more `.cfg`
+  files and their `EXPECT` lines), pinned by the task; and the agent's change — either the model
+  of the implementation the agent edited, or the code that a task-owned extractor maps to the
+  model's constants.
+- **Output**, one of four, in `grade.json`:
+  - `pass` — TLC finished every config and each matched its `EXPECT`;
+  - `counterexample` — a property was violated: the property name and the trace;
+  - `timeout` — the state space was not exhausted within the task's limit;
+  - `tool_error` — TLC or the parser failed (syntax error, unknown operator, Java missing).
+
+## Rules
+
+1. **The agent cannot weaken the spec.** The grader reads the spec, configs and `EXPECT` lines from
+   the task's eval tree (pinned in the batch ledger like other grader sources), never from the
+   agent's workspace. A change to those paths in the workspace is reported and ignored.
+2. **The agent cannot swap the checker.** `tla2tools.jar` and the JRE are pinned by SHA-256 in the
+   grader and mounted read-only; TLC runs outside the agent's container. The command line
+   (`-workers`, `-deadlock`, `-config`) is the grader's, not the task's or the agent's.
+3. **A timeout is not a proof.** `timeout` and `tool_error` score as not passed and are reported
+   apart from `counterexample`, so a slow model is not read as a correct one, and a broken tool is
+   not read as an agent failure.
+4. **Vacuity.** Each task ships witness configs that must be violated; if a witness passes after the
+   agent's change (the change made the scenario unreachable), the grade is `counterexample` with
+   the witness named.
+5. **A pass is not a quality score.** It means: in this bounded instance, under the stated fairness
+   assumptions, the listed properties hold. The report shows it as its own measure next to tests and
+   any judge, never folded into one number, and names the instance bounds.
+
+## Limits
+
+- Bounded: only the constants in the configs are checked.
+- The model-to-code link is as good as the extractor or the human mapping (the README's action →
+  code table); a correct model of wrong code passes.
+- Liveness holds only under the fairness the spec assumes.