[napetrov]

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

Summary

This PR adds a TLA+ model of the dokimi repo run cell lifecycle. The model covers worker threads, resume, --force reruns, crashes between the artifacts and result.json, Ctrl-C, and what repo report/compare count. TLC is run on it, and the two bugs it found are fixed, each with a test that replays the trace TLC printed.

Property (TLA+)	Holds in code via
P1 a retry is not another sample	one result.json per cell dir; a retry reuses the cell name
P2 only a finished attempt of that cell, with its own files, counts	run_cell rmtree before an attempt, result.json written last; _refuse_shared_cells (new)
P3 no stale attempt overwrites	batch_lock; threads die with the process; _refuse_shared_cells
P4 one execution per report row	check_batch_executions; refuse_mixed_executions (new) in summarize and on compared rows
P5 a partial run is not reported complete	exit code; record_plan + load_cells missing list
P6 Ctrl-C starts no queued cell and does not exit 0	pool.map cancels pending futures (already true; the test pins it)
P7 every invocation ends (liveness)	under explicit weak fairness only

Bugs fixed

1. One cell planned twice. This happens with a repeated --task/--model, or with --model org/m --model org:m, which give the same slug. With --jobs 2, two threads shared one dir: one rmtree'd the other's dir while its agent ran, and result.json ended up beside the other attempt's meta.json and answer. Such a plan is now refused before any agent runs.
2. Two executions pooled in one row. A --force run with another execution that stopped part way left cells of two execution ids, and report/compare pooled them in one row. A harness binary replaced mid-batch does the same. report now refuses the batch, and compare refuses the rows it compares, naming both ids.

A first probe suggested Ctrl-C starts queued cells. That probe used _thread.interrupt_main(), which sends no signal. A real SIGINT wakes the main thread and pool.map cancels the queued cells, so it is not a bug.

Evidence

• formal/repo_batch/run.sh checks each of the 13 configs against its EXPECT line, and all 13 matched:

  Config	Expected result
  fixed	pass
  code_main_* (code before the fixes)	violation
  4 mutations: accept a stale attempt, count every commit, no lock, no cancel guard	violation
  no_fairness	violation of P7
  4 vacuity witnesses	violation

  fixed: 10.3M states generated, 5.75M distinct, depth 28, 432 s. Tools: tla2tools v1.8.0 (sha256 in the README) and Temurin 21.0.5+11. The full table is in formal/repo_batch/README.md.

• tests/test_repo_batch_lifecycle.py has 11 test cases (9 functions, one parametrized three ways). On intel/main 9 of them fail: the duplicate plan ×3, the stopped --force, naming every repeated cell, the case-only refusal, the per-batch mixed-execution refusal and the two compare refusals. The Ctrl-C and crash-then-resume tests characterise existing behaviour and pass on both trees. tests/test_repo_batch_run_script.py (16 test cases, 8 functions, one parametrized nine ways) runs run.sh with relative paths, with only POSIX tools on PATH, and with the verdict cases; all 16 fail on main's script.

• make ci-local: 0 failed, 32 passed, 13 skipped, on the pre-round head. On the round head, the repo, batch, runner, formal and tla tests passed (6430 passed, 3 skipped) before the last run.sh edit; after it, the lifecycle, run-script and unreadable-cell report tests pass on the final tree (190 passed: 11, 16 and 163).

• Local self-review (pr-review, L3, 3 passes, fresh-context reviewers): pass 1 nits and pass 2's stale counts in this description were fixed; pass 3 on the final head has no blocking findings. The passes led to the refusal moving out of load_cells, so hits and clean compared arms are no longer refused, and to the test and doc fixes in commits 2 and 3.

Limits

• The checked instance is small: 2 tasks, 2 workers, 2 execution ids, 3 invocations.
• Not modelled: the batch budget, unsupported tasks, several arms/models, a cell failing inside a live process, and a second Ctrl-C. A second Ctrl-C releases the lock while threads still run; this is pre-existing and listed as an open question.
• Nothing here checks grader, LLM-judge or task validity, or the system as a whole. It shows only that this lifecycle, as modelled, does not miscount or mix the results it is given.
• The open questions are listed in the README:
  • --force together with --max-batch-usd;
  • a grader-written result.json;
  • caps not part of execution.id;
  • run.sh not in CI.

formal/repo_batch/EVALUATOR.md proposes a model-checking grader for agent tasks. The spec and checker are pinned outside the agent's reach. Its outputs are pass, counterexample, timeout or tool error; a timeout is never counted as a pass. A pass is reported as its own measure, not as a quality score.

Merge danger

Medium. repo report/compare now refuse batches they used to pool: an arm/model with cells of two execution ids. The message names both ids and the --force rerun that clears it. repo run now refuses a duplicate cell plan, and two --model names that differ only in case (refused on every file system, since they share one directory on a case-insensitive volume).

🤖 Generated with Claude Code

[codecov-commenter]

⚠️ Please install the to ensure uploads and comments are reliably processed by Codecov.

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 95.72%. Comparing base (f12057b) to head (370be67).
⚠️ Report is 2 commits behind head on main.
❗ Your organization needs to install the Codecov GitHub app to enable full functionality.

Additional details and impacted files

@@           Coverage Diff           @@
##             main     #628   +/-   ##
=======================================
  Coverage   95.71%   95.72%           
=======================================
  Files         415      415           
  Lines       55346    55392   +46     
  Branches     9514     9522    +8     
=======================================
+ Hits        52977    53025   +48     
+ Misses       1466     1465    -1     
+ Partials      903      902    -1     

Files with missing lines	Coverage Δ
dokimi/dokimi/repos/compare.py	100.00% <100.00%> (ø)
dokimi/dokimi/repos/report.py	98.02% <100.00%> (+0.08%)	⬆️
dokimi/dokimi/repos/runner.py	97.36% <100.00%> (+0.13%)	⬆️

... and 3 files with indirect coverage changes

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

[exai-bot]

OpenCodeReview: Commit 370be67 was not reviewed. This PR has reached its review limit (6 reviews).

CI at `370be67`: 10 still running, 3 passing, 1 skipped

Check	Status
Build docs (strict)	still running
CLI interface diff	still running
CodeQL (actions)	still running
CodeQL (python)	still running
External catalog smoke test (uxlfoundation/skills)	still running
Platforms and Python versions	still running
Static checks (ruff, schema, zizmor, licenses, pre-commit, bandit, secrets, changelog, schema com...	still running
benchmark	still running
mypy	still running
self / repo validate	still running

To review this commit: re-request review from exai-bot in the Reviewers list.

<details><summary>Last review (18e2755): 1 medium</summary>

Open threads from the bot: 1

</details>

[Copilot]

Warning

Copilot couldn't run its full agentic review because it didn't start before the timeout. Make sure your repository has a runner available, or add a copilot-code-review.yml file specifying one with the runs-on attribute. See the docs for more details.

Copilot review overview

5 open issues

• The second compare() call uses treatment "guidance:raw", but this test run only created arms… · New
• The error only reports the first duplicated cell even if multiple cells are duplicated, which makes… · New
• This script depends on non-portable tooling/features (grep -P/PCRE, date +%N, and bc) which… · New
• This script depends on non-portable tooling/features (grep -P/PCRE, date +%N, and bc) which… · New
• This script depends on non-portable tooling/features (grep -P/PCRE, date +%N, and bc) which… · New

What changed in this PR

Adds a TLA+ model for the dokimi repo run cell lifecycle and uses it to drive fixes that prevent duplicate cell plans and mixed-execution aggregation in reporting/comparison.

Changes:

• Added formal/repo_batch TLA+ spec + TLC configs + runner script to model-check lifecycle properties.
• Prevented duplicate cell directory plans and added tests that replay TLC counterexamples.
• Refused mixed execution.id rows in repo report and in compared rows for repo compare, with tests and docs updates.

File	Description
dokimi/​dokimi/​repos/​runner.py	Adds _refuse_shared_cells and calls it before any work starts to reject duplicate planned cell directories.
dokimi/​dokimi/​repos/​report.py	Adds refuse_mixed_executions() and enforces it in summarize() to prevent pooling multiple executions into a row.
dokimi/​dokimi/​repos/​compare.py	Uses refuse_mixed_executions() to refuse only mixed rows that are actually compared.
dokimi/​tests/​test_repo_batch_lifecycle.py	Adds regression tests that replay TLC traces for duplicate plans, Ctrl-C cancel behavior, crash/resume, and mixed-execution rows.
dokimi/​formal/​repo_batch/​RepoBatch.tla	Introduces the TLA+ model capturing the cell lifecycle and report/compare counting semantics.
dokimi/​formal/​repo_batch/​run.sh	Adds a helper script to run TLC across configs and validate expected outcomes.
dokimi/​formal/​repo_batch/​cfg/​*.cfg	Adds TLC configurations for “fixed”, pre-fix (“code_main_*”), mutations, fairness, and vacuity witnesses.
dokimi/​formal/​repo_batch/​README.md	Documents mapping from model actions to code and summarizes TLC results and findings.
dokimi/​formal/​repo_batch/​EVALUATOR.md	Proposal doc for a model-checking grader architecture.
dokimi/​formal/​repo_batch/​.gitignore	Ignores TLC output directories/artifacts.
dokimi/​docs/​repo-evaluation-contract.md	Documents new refusal behaviors for repo run duplicate plans and report/compare mixed executions.
dokimi/​changelog.d/​20261111_180000_napetrov_repo-batch-lifecycle.md	Changelog entry describing the fixes and the new formal model.
.github/​.licenserc.yaml	Exempts .tla/.cfg headers from the license header checker.

_{Review effort: Lite}

[vchamarthi]

Review at 0fa65be. 3 new findings: 3 must-fix. In the line comments. Adds a TLA+ model of the repo run cell lifecycle, a refusal for a plan that names one cell twice, and repo report / repo compare refusals for rows whose cells ran under two executions. The plan refusal, the case-only refusal and the run.sh path fixes for TLA2TOOLS_JAR, OUT and the configs hold; the new mixed-execution refusal names a remedy that the batch check refuses; run.sh still fails when JAVA is a relative path; and the Ctrl-C test has no Windows skip.

Verified

• Changed tests: The 12 cases of dokimi/tests/test_repo_batch_lifecycle.py and dokimi/tests/test_repo_batch_run_script.py pass on 0fa65be.
• Merge: 0fa65be merges onto 38d07f9 with no conflict.
• Duplicate-plan refusal: Changing the planned-twice check in dokimi/dokimi/repos/runner.py from > 1 to > 2 makes the refusal tests fail, so they pin the check.
• Relative paths in run.sh: A relative config, jar and OUT resolve from the caller's directory, as test_relative_paths_resolve_from_the_callers_directory pins; JAVA is the exception (see earlier).
• Missing config: run.sh given a config path that does not exist exits non-zero, names the file on stderr, and writes no <name>.log, before TLC starts.
• Execution id type: An execution id that is not a string is counted as unrecorded by refuse_mixed_executions, so it is refused beside a real id.
• Ctrl-c: A Ctrl-C during a batch starts no queued cell: the queued cells are reported as missing, not failed.

Still open from earlier rounds

• #628 (comment): JAVA=./bin/java bash <run.sh> <fixed.cfg>, run from the directory that holds ./bin/java, now gives error rc=127 for fixed (summary NO) and exits 1; run.sh changes into its own directory before it runs "$java" (line 28).

Pre-existing, not blocking

• dokimi/dokimi/repos/batch_ledger.py:59: cell_name maps two different models to one directory, and a later repo run on the same batch reuses the first one's finished cell. Input: repo run --batch b1 --model org/m-1 --task fix_add, then repo run --batch b1 --model org:m-1 --task fix_add. The second run reports 0 ran, 1 already done and returns without error; fix_add__guidance-raw__org_m-1__r1/result.json keeps "model": "org/m-1", so org:m-1 is never run. reused_result (dokimi/dokimi/repos/batch_ledger.py:140) returns the finished cell because the execution id, built in execution_record, does not include the model. The PR's _refuse_shared_cells refuses this collision only inside one plan; across invocations the same bug class is left open. The same two invocations behave the same way on main.

[vlad-perevezentsev]

Review at 27a835a. Both fixes are right: a plan that names one cell directory twice (or two names that differ only in case) is refused before any agent starts, and repo report / repo compare refuse a row whose cells hold two executions. What is left is the wording of the remedy, a Windows skip, a run.sh exit-status check and where the evaluator proposal lives.

Agreed with @vchamarthi: the remedy the mixed-execution message names is refused while another arm holds the older execution; test_ctrl_c_starts_no_queued_cell needs a Windows skip. The relative JAVA path is fixed in 4d51619.

Agreed with @exai-bot: run.sh reports pass without checking TLC's exit status.

Disagreed with @Copilot on the guidance:raw arm in the compare test: replied in its thread.

What I ran, at 27a835a:

• make ci-local --offline: 0 failed, 21 passed, 19 skipped (network-only jobs).
• tests/test_repo_batch_lifecycle.py on the merge-base fc9fbf5: 8 of 10 fail. The two that pass there (Ctrl-C, crash then resume) pin behaviour that already held, as the README says.
• test_ctrl_c_starts_no_queued_cell 40 times in parallel on a loaded host: 40 passed, so the 0.3 s wait is not flaky here.
• TLC itself was not run (no tla2tools.jar or Java here); run.sh was checked through its fake-java tests only.

Checked, no issues

• Call sites: repo compare refuses only the compared rows, after _in_models, and batch names are distinct, so two batches with one name cannot be grouped together. repo report --hits lists cells one by one and pools nothing.
• Legacy cells: a cell with no execution counts as unrecorded, as check_batch_executions does on resume, so the two checks agree.
• Merge: clean into current main (5 commits behind); no open PR conflicts with it.
• License headers: every new file has the SPDX header; .tla and .cfg carry it in TLA+ comments.

[vlad-perevezentsev]

EVALUATOR.md and the "(proposal)" section of README.md are a plan for a feature that does not exist, and AGENTS.md keeps those out of the tree.

AGENTS.md, "What goes in the tree": "Design rationale, status and plans go in the PR description or an issue; the tree has no ADRs or status reports", with dokimi/research/records/ as the one exception. This file starts with "Status: proposal, not implemented", and README.md:140 repeats it.

Suggestion: move the proposal to an issue or a record in dokimi/research/records/, and keep in formal/repo_batch/ only what describes the model and how to run it.

[napetrov]

Waiting on a decision before I change this: where the evaluator proposal lives. Options: (A) one record under dokimi/research/records/, the exception AGENTS.md allows; (B) an issue, and delete EVALUATOR.md and the README section. My recommendation: A, so the design reasoning sits next to the model it describes. The thread stays open until then.

[vchamarthi]

Pushed 1 commit to tla/run-lifecycle (27a835a..783e2ad).

• run.sh counts a pass only with exit 0 and a violation only with exit 12 or 13.
• _check_cell refuses a batch that is not a string.
• The mixed-execution message names a --force run over every arm and model of the batch; changelog and contract say the same.
• test_ctrl_c_starts_no_queued_cell is skipped on Windows.

Threads: 1 fixed, 0 answered as not a defect.
Run: the full suite with main merged in, 19164 passed.

Questions for @napetrov

1. Move formal/repo_batch/EVALUATOR.md and the proposal section of README.md to an issue or dokimi/research/records/? (dokimi/formal/repo_batch/EVALUATOR.md:6)
AGENTS.md keeps plans and status out of the tree; EVALUATOR.md opens with Status: proposal, not implemented and README.md:140 repeats it. Where the proposal lives is the author's call.

• A: Move it to a record in dokimi/research/records/
• B: Open an issue and delete both

[xaleryb]

• Ran at 452f5cd merged with current main: the full suite, ruff, mypy, bandit, the growth and comment-block checks, the strict benchmark docs check, all 13 TLC configs through run.sh, and 13 mutants over the new guards. Everything passes, and all 13 mutants are killed.
• Each earlier point was re-run on its original input and is fixed at the head: the duplicate and case-only cell names, the run.sh path resolution and exit status, the POSIX tools, the mixed-execution remedy text, the Windows skip and the non-string batch.
• Still open: EVALUATOR.md and the README proposal section keep a plan in the tree. AGENTS.md:110-112 puts plans in the PR description or an issue, and allows dokimi/research/records/ as the one in-tree place. Proposal: move the evaluator proposal into a single record under dokimi/research/records/, and keep only the model and how to run it in formal/repo_batch/.

[antonwolfy]

Review at 452f5cd. The fixes are right and the tests pin them: the duplicate-cell and case-only refusals, the mixed-execution refusal in report and on compared rows in compare, and the --force remedy now named in the message. I found no wrong behaviour. Two risks are test gaps that let a real regression through, and there are two nits inline, plus one more in the body. The merge also waits for a decision on where the evaluator proposal lives.

What I ran, on a Linux review host at 452f5cd:

• make ci-local: 29 passed, 3 failed, 13 skipped. The failures are the gitleaks download (HTTP 504) and its scan, and 3 pytest 60 s timeouts in test_import_architecture.py and test_audit_test_quality.py, which are files the PR does not touch and pass when run alone; 19,018 tests passed; changed-line coverage 100%
• Reproductions of the refusals on the runner.py, report.py and compare.py paths, with the LLM transport mocked: duplicate and case-only plans, legacy and unrecorded cells, two batches in one compare, the --model filter, the --force rerun over every arm.
• A mutation run: 21 mutants of the new Python guards, 18 killed, 3 survive (the compare model-filter order and two message strings). 25 mutants of run.sh, 9 survive (see the inline comment).
• The lifecycle tests against the PR's base: they do not collect (refuse_mixed_executions is missing), and the 6 non-string batch cases in test_repo_report_unreadable_cell.py fail there.
• Every non-merge commit has a Signed-off-by.

Open from other reviewers: @vlad-perevezentsev's point that EVALUATOR.md and the README's proposal section keep a plan in the tree, against AGENTS.md, waits for a decision from the author: a record under dokimi/research/records/, or an issue. @xaleryb made the same point.

One more nit. README.md:43 and RepoBatch.tla:133 say _write_json is "mkstemp + os.replace". artifacts.write_json writes a <name>.<pid>.<thread>.tmp sibling and calls os.replace; it does not call mkstemp. Suggestion: write "temp file + os.replace" in both places.

Checked, no issues

• Import order: batch_ledger, report and compare import cleanly in a fresh interpreter, so the new report to batch_ledger import makes no cycle.
• Legacy cells: a batch with no execution records still reports and compares. One recorded cell next to unrecorded ones is refused as unrecorded, as check_batch_executions does.
• Remedy: a --force run over the whole plan clears the mixed state; compare refuses the compared rows only.
• Docs and rules: the changelog fragment format, the mkdocs.yml nav entry for the contract page, the growth baseline and docs code references pass; no generated artifacts are committed.

Bot points I checked that no longer apply at this head (2)

• Copilot's point on the guidance:raw arm in the compare test does not apply: _run always passes --arm guidance:raw, so the batch has that arm and the compared pair exists.
• exai-bot's point on run.sh reporting pass without the exit status does not apply at this head: run.sh:37 takes a pass only with exit 0 and the violation branches only with 12 or 13.

[napetrov]

Re: review by vchamarthi

relative JAVA fails
Fixed in 4d51619; the other two are on head (a24c429).

[napetrov]

Re: review by vlad-perevezentsev

a Windows skip, a run.sh exit-status check
On head (a24c429). The proposal is held on the EVALUATOR.md thread.

[napetrov]

Re: review by antonwolfy

two nits inline, plus one more in the body
Each is handled this round (a24c429).

[napetrov]

Re: comment by xaleryb

Each earlier point ... is fixed at the head
Thanks. The open point is held on the EVALUATOR.md thread (a24c429).

[napetrov]

Re: comment by vchamarthi

1. Move formal/repo_batch/EVALUATOR.md and the proposal section of README.md to an issue or dokimi/research/records/?
   Waiting on a decision before I change this: the same question as on the EVALUATOR.md thread. Options: (A) one record under dokimi/research/records/; (B) an issue, and delete the file and the README section. My recommendation: A, so the design stays next to the model. The round does not change it until then.

[exai-bot]

Must-fix. Impact: the runner silently discards a config's counterexample log when another selected config has the same basename, and the summary cannot distinguish the two inputs. Trigger: invoke run.sh /tmp/before/fixed.cfg /tmp/after/fixed.cfg. Evidence: both inputs set name=fixed, so the second > "$log" truncates the first log; they also share -metadir "$out/states/$name" and the same summary label. Please assign distinct output identifiers to distinct config paths, or reject duplicate basenames before running any checks, and add a two-config regression test. Workaround: use unique basenames or separate invocations with different OUT directories. Severity: medium because this loses verification evidence within the supported explicit-config interface, but does not affect repository-evaluation artifacts.

[antonwolfy]

Review at 2130ad5. The re-review finds no bug or risk in the changes since my last review: the new tests pin the points I raised, and the guards in runner.py, report.py and compare.py hold. One nit inline on run.sh. The merge still waits for the author's decision on where the evaluator proposal lives.

What I ran, on a Linux review host at 2130ad5:

• make ci-local: 33 passed, 0 failed, 14 skipped; the changed-line coverage step passes.
• Mutation run of the new Python guards on a copy: 15 of 16 mutants killed. The one that survives changes only the batch or where label in the refusal message.
• A reproduction of run.sh with a fake java: run.sh before/fixed.cfg after/fixed.cfg writes one fixed.log, passes -metadir out/states/fixed to both runs, and prints two rows labelled fixed.
• Every non-merge commit (16) has a Signed-off-by.

Waits for the author: @vlad-perevezentsev's and @vchamarthi's question on EVALUATOR.md and the README proposal section (a record under dokimi/research/records/, or an issue) waits for a decision, since the author handed the choice back with a recommendation and no change.

Checked, no issues

• Threads from my earlier review: the --model narrowing case, the --task and --reps pin, the run.sh verdict cases and the case-only wording in the changelog and the contract are all present at this head.
• Docs: the message wording, _refuse_shared_cells, has no usable batch and the case-only refusal in the contract, changelog and README match the code.
• Bad batch values: null, list and number exit 2 for both report and compare, with no traceback.

[antonwolfy]

I pushed a commit per nit, up to 18e2755, which fix the nit from my review:

• 18e2755: dokimi/formal/repo_batch/run.sh:24: a repeated cfg basename is refused with exit 2 before any TLC run, and a test covers it.

make ci-local at 18e2755: 33 passed, 0 failed, 14 skipped.

Not approving yet. Still open: @vlad-perevezentsev on EVALUATOR.md and README proposal section: record under dokimi/research/records/ or an issue; author handed the choice back.

[vchamarthi]

Pushed 1 commit to tla/run-lifecycle (18e2755..370be67).

• run_batch cancels queued cells when KeyboardInterrupt arrives while pool.map is still submitting.
  Run: the full suite with main merged in, 20521 passed.
  3 tests in tests/test_repo_compare_interval.py fail on main as well: float summation result differs from the expected value in test_repo_compare_interval.py.

Open threads this head already settles:

• dokimi/formal/repo_batch/run.sh:34 (exai-bot): Fixed on 18e2755 (run.sh: refuse two cfgs with the same basename); run.sh lines 24-32 refuse a repeated basename before any check runs.
• dokimi/formal/repo_batch/run.sh:34 (antonwolfy): Fixed on 18e2755 (run.sh: refuse two cfgs with the same basename); the refusal sits before the check loop, same as the other thread on that line.

The PR description needs these corrections:

• "P6 Ctrl-C starts no queued cell and does not exit 0 | pool.map cancels pending futures (already true; the test pins it)" should read: P6 Ctrl-C starts no queued cell and does not exit 0 | run_batch cancels the queued cells on KeyboardInterrupt, also during submission