Overnight plan (2026-10-10, Dennis asleep)

Goal: as much autonomous progress as possible, with nothing posted or pushed anywhere. Checkpoints are non-blocking (PLAN rule 9). Only check_kill.sh PASS counts as a kill.

Running or launched

| wf_12d28fda-719 | formalize #4 #11 #3 (#4, #11 KILLED) | #3 pending | | wf_85b7385a-683 | batch 2: #1/#10 proof+formalize; twins of #2/#11; deepen round 2 (12 machines) | per chain | | wf_6a281a56-be6 | batch 3: twins (#12-twin, #24, #25) + wave 2 (#29 #33 #37 R2 R4 R5 R8 R9) | per chain | | wf_797b2d5b-1bf | #2 review page (machines/<#2>/review.html) + all-778 dashboard (dashboard/, /) | review + dashboard |

| wf_b7a26ffc-0a4 | funded stages from the decision queue (Dennis: all recommendations): #7 #8 #9 #10 #14 #16 #18 #29 R2 #37 R8 -> high -> proof + 2 skeptic rounds -> formalize | per machine: new status/decision or kill | | wf_40d09972-ac2 | wave 3 observe (pool 3): #28 #30 R3 #35 #36 #26 -> proof -> formalize -> twins | per machine | | background | R5 24 h qsim watch (work/qleft_24h.txt), R9 sim to 1e12 (work/sim_1e12.jsonl) | read once each when done: halt => KILLED_HALT lead; R5 overflow => new decision.json |

| wf_fe36bff3-97e | R5 post-overflow follow-up (detached C run, log machines/1RB1LA_1RC1RE_.../work/r5_post.log) + Wave 4 scout/rank/attack (reports/wave4/) | R5: HALT line or new epoch => tell Dennis; W4: per pick kill / decision | | wf_5b5d8095-a48 | Class 2 close-out (Dennis 10-12): W4-3 table (341/512/588), R4+#32, C2-552; stages -> proof/skeptic/formalize/siblings | per track: kill / decision | | wf_3cc3904c-205 | C2-552 HALT certification + kill (Dennis 10-12): independent re-run, exact steps, Rocq design -> formalize (check_kill --halt) -> audit -> bundle | KILLED_HALT, or stop if the independent run disagrees | | wf_4bd649c4-02c | W4-7 funded grammar2 stage (Dennis 10-12) -> proof -> skeptic -> formalize; covers line 707 | kill or new decision | | wf_34c8d48b-b0e | W4-7 funded invariant stage (Dennis 10-12) -> proof -> skeptic -> formalize; covers line 707 | kill or new decision | | wf_f391b4df-8ba | #14 funded vf_round (Dennis 10-12) -> skeptic 3 -> formalize | kill or new decision | | wf_de202db8-b4c | Wave 5 (Dennis 10-12): scouts -> rank/critic -> attack top 8 (reports/wave5/) | per pick: kill / decision | | wf_d3589503-763 | W5-4 + W5-6 funded stages (Dennis 10-13) -> proof chain | kill or new decision | | wf_753e4201-8a1 | W5-5 halt certification + kill (Dennis 10-13) | KILLED_HALT, or stop | | wf_73ce8ccc-8c5 | Two-PR prep: W4-3 table (A) + C2-552 halting (B), prep only (replaces stopped wf_f133c95e-f33) | texts + verified branches, no push | | wf_6d584590-160 | Site restructure (Dennis 10-13): one nav, Home, Machines, one page per machine, Submissions, Decisions, Reports | new pages + tests + review | | wf_431d67dd-ade | Learning guide (Dennis 10-13) at learn/ | modules + index + glossary | | wf_9c86de6d-ba5 | BEC sweep (Dennis 10-13): rank 21 untouched BEC -> attack top 8 | kills / decisions | | wf_2858ada7-f87 | Wave 6 (Dennis 10-14): scouts -> rank/critic -> attack top 8 (reports/wave6/); plus 693 stage 3 (fund_clock) | per pick: kill / decision | | wf_90f568e8-a70 | Strategy directions 1-4 (Dennis 10-14): ports of upstream twins, K42 atlas, halting search, CB3 study (reports/strategy/directions.md) | kills / reports/k42, reports/cb3 decisions | | wf_f361b4b0-d23 | CB3 closure explorer (Dennis A) + shared attempts ledger (coord/attempts.tsv, tools/attempts.py) | CB3 kills or decision; ledger + coverage report | | wf_5a083869-f1b | Wave 7 (Dennis 10-14): table/cluster-level plan with go/no-go gate, then attack <= 6 picks (reports/wave7/) | per pick: kill / decision | | wf_dd9e98e0-9a8 | Halting hunt + 693 bursts (Dennis 10-13) | kills / decisions |

Chaining (on each completion notification or heartbeat)

1. When wf_abd883b4-076 completes: run the formalize workflow (same script) on every machine of #3/#4/#11/#13 whose status.json is CHECKPOINT_B.
2. When deepen completes: run formalize on any machine it brought to CHECKPOINT_B.
3. When cards v2 completes: re-run tools/card.py --all after any observe.json sync, so the cards reflect the deepen/proof results (deepen agents write to notes.md + deepen.json, not observe.json, to avoid clobbering the cards data pass).
4. Low priority, only if the machine is otherwise idle: #5 cryptid-protocol Rocq rule reduction (7 bounce rules + no-00 invariant, AntiHydra.v style). 4c. Before rebuilding: python3 -B tools/pr_sync.py (read-only gh). If a PR turns merged or gains comments/reviews, tell Dennis (summarize any comment verbatim-ish); a merge moves its machines to "Accepted upstream". The next group goes out only after Dennis says so (order after #3's table: #11's table, #4's table, #12 pair, #8, #30). 4b. Once tools/dashboard.py exists: re-run python3 -B tools/dashboard.py at each check-in (cheap, cached thumbs) so the dashboard stays current.
5. At the end: write reports/overnight-2026-10-10.md (kills, statuses, what needs Dennis, links) and update STATUS.md. Do not commit (Dennis commits on request) and do not post to Discord.

Guardrails

• At most 2 heavy processes per agent. Overnight the machine may be busy, which is fine.
• Never use the windows MCP. Never touch vendor/.
• A kill = check_kill PASS, independently re-run by a second agent.

Reuse

• Formalize script (generic, args = [{rank, tm, template}], pool of 2): [local working file] Run it with Workflow({scriptPath, args}). Template strings per machine: reports/targeting.md §4.2/§4.3 and each machine's proof.md.
• Ledger of launched formalizations (so check-ins never double-launch): reports/overnight-ledger.md
• Watchdog: tools/watchdog.sh (running in the background, log: reports/watchdog.log). Restart it if it isn't running: pgrep -f tools/watchdog.sh.

Resource policy

• Total concurrency target: <= ~14 agents and <= ~28 heavy processes. Don't launch a new formalize batch while load average > 30 or MemAvailable < 6 GB; wait for the next check-in.