[Deicyde]

Fixes #434.

Problem

#434 (from the recovery report in #426, sections 3 and 4) describes three failures in a long Formalize run:

• Leaf-sized dispatch. "Fine theorem DAGs currently encourage leaf-sized dispatch, worktree preparation, claim/context exchanges, builds and reviews." Add Formalize wording for #434, #435, #466 and #483 #488 let a subagent keep its worktree, but the lead still dispatched every leaf after every integration.
• Topology found late. "The early run used two primary sessions in one Git common directory without a clear topology diagnostic." The README says each session needs its own clone, but neither the Formalize skill nor its claims reference does, and those are what the agent reads.
• Coordination over a failed transport. "A verified nonoverlapping proposal initially required manual relay; an immutable mailbox later delivered acknowledgements, commits, task queues." The issue notes that the transport failure itself is not an Autoform defect.

Change

Wording only, plus documentation for a flag that already exists. Each acceptance box:

1. Multi-leaf package. In skills/formalize/SKILL.md, a subagent may keep its worktree for a package of related leaves (such as one container's) that the lead confirms together. It holds only the leaf it has taken, takes the next once work context shows it ready after integrating, and at the first leaf that isn't ready the rest of the package returns to the lead. This replaces Add Formalize wording for #434, #435, #466 and #483 #488's per-leaf dispatch. Jack's 10-26 comment on this issue let a subagent "take several related ready leaves in sequence"; now the subagent goes on to the next leaf of a package the lead confirmed, without waiting for a new dispatch. Readiness is still derived, never authored.
   • Every leaf is dispatched with claim_target, article_revision, open_statements and revision. Only the first leaf also gets phase and assumes; a later one takes them from the first read that shows it ready, because under open_statements: allowed its assumes shrink as earlier package leaves are proved.
   • The worktree is kept, so lake exe cache get runs once per package.
2. Disjoint writers, scope expansion, review. Met by existing rules, which a package doesn't change: the lead confirms targets within a session, claims and the no-hold-and-wait rule work across sessions, editing beyond the held targets still means reporting and waiting, and every leaf still gets an independent Agent Review before anything is recorded.
3. Topology before dispatch, for runs that use claims. In skills/formalize/references/claims.md ("Worker IDs and the board"), a session leads from its own clone. If git worktree list shows the shared branch checked out in another worktree, the lead asks the user first.
   • Git lets only one worktree per clone check a branch out, so a second session leading from the same clone sees the first one's checkout there.
   • Worktrees left by this session's earlier runs sit on their own branches, so a resumed run is never asked.
   • The check sits in the claims reference because several sessions means claims. The Consolidated: Formalize recovery observations (tracked via #429) #426 sessions knew about each other and coordinated.
4. Transport-independent handoffs. In claims.md, workers pass --note naming the worktree's branch on every acquire.
   • When the lead hands a candidate to another session and the request covers pushing, the candidate goes to origin on a branch whose name ends with the leaf's article_id.
   • With the report, the integrator renews under the reported worker ID, as before. Without it, the integrator waits for the lease to lapse, reads any note left, and looks for that branch with git ls-remote --heads origin to continue it. Then it acquires under its own ID.
   • The note points to the branch only while the lease is live, since claim cleanup or another worker's acquire can erase it. The branch name still finds the candidate after that. A lost report therefore costs at most one lease term (25 minutes by default) and never becomes permission.
   • A new sentence says no message grants ownership or completes a leaf. Completion stays the verified commit visible on the shared branch, as claims.md already requires.

Not adopted

This PR declines three items from the issue's deliverable list rather than deferring them. Jack's 10-26 comment described them as waiting for the freeze to end; Jack decides whether these reasons stand.

• A project coordinator across sessions (frontier, integration queue, shards). Autoform keeps orchestration minimal and does not dictate how agents schedule work. Each lead coordinates its own workers, and across sessions the claim board and Git's compare-and-swap push to the shared branch already serialize ownership and integration.
• Recording repository, common-directory and cache identities. These paths are machine-local and mean nothing to another machine. What does cross machines (origin, branch, commit) is already in Git. The skill already covers cache topology: each new worktree runs lake exe cache get, and work import-impact does not count a build made in another clone or worktree.
• A rule to prioritize project-critical work. Prioritizing is the lead's judgment, not something Autoform should prescribe.

Public surface added

None. The CLI's commands and flags are unchanged against main. The branch-name ending is a convention, not a new ref layout.

The existing surface below is now documented in autoform_cli/README.md and so becomes a contract:

• autoform claim acquire --note TEXT, in --help since v2.0 but never in the README: it stores free text in each lease, and Formalize uses it to name the worker's branch.
• The note key in the JSON claim list prints, which was already printed from the lease. renew keeps it. The key is absent, not empty, after an acquire without --note.

Docs

File	Added	Removed	Net
skills/formalize/SKILL.md	8	8	0 (254 of 254)
skills/formalize/references/claims.md	19	13	+6 (references 911 of 932)
autoform_cli/README.md	3	1	+2
CHANGELOG.md	9	0	+9

Verification

• New CLI test in tests/test_claims.py: a single-target acquire with --note shows the note in claim list, and the owner's next acquire without --note leaves no note key. The existing CLI round trip already covers a multi-target --note and renew keeping it.
• An independent static review (correctness, API minimality, docs and tests) and the API review both ran before this PR. Their blocking findings are applied: the push needs the request's authority, the handoff branch is found by its article_id, a lost report waits for the lapse, and a package returns its untaken leaves to the lead.
• Run locally: tests/test_doc_budgets.py, tests/test_skill_examples.py (links, anchors, parse checks of documented commands, safety rules), and the note and round-trip tests in tests/test_claims.py. ruff check is clean. No Lean is involved; CI runs the full suite.

Posted by Claude Code (session cove-343224054).

[Deicyde]

Review at 5804e71: merge.

This is a static review, the first on this PR. It checks the new prose against autoform claim in autoform_cli/claims.py and autoform_cli/__main__.py, against the rest of the Formalize skill, and against #434. Test results are left to CI, where all 9 checks pass. The prose matches what the claim commands do: acquire stores note only when one is given, renew and multi-target renew copy it, and claim list prints it for expired leases too, so a note survives a lapse until claim cleanup or another acquire replaces the lease. No command, flag or JSON key is new: --note and the listed note key exist at the base, and the PR only documents them. Line counts match the body (Formalize SKILL.md 254 of 254, references 911 of 932) and stay the same after merging current main, which merges cleanly. The new test pins what its docstring says: an acquire that kept the owner's earlier note fails its last assertion. There are no blockers. The notes cover the issue link and wording gaps in the new topology, handoff and package rules.

Notes

1. Fixes #434 closes the issue before Jack has decided. Jack's 10-26 comment on Formalize: long-lived work packages and durable session coordination #434 says only a wording slice goes in now and the issue stays open for the rest. This body declines three deliverables instead and asks Jack to decide, but with Fixes, merging closes Formalize: long-lived work packages and durable session coordination #434 either way. Two acceptance boxes are also only partly met. Box 3 asks that startup identify the topology before workers launch, but the check here lives in claims.md, so it runs only in runs that use claims. Box 4 asks that proposals and acknowledgements survive a failed transport, and the PR covers handed-off candidates only. Fix: write Part of #434 unless Jack accepts the declines and the narrower boxes.

2. The topology check does not say who runs it or when. claims.md says "if git worktree list shows the shared branch elsewhere, ask the user first". Every subagent follows the claim rules (SKILL.md), and from a subagent's worktree the shared branch is always checked out elsewhere, in the lead's checkout. In a scratch repository, git worktree list run in an agent worktree lists [main] at the lead's path. "First" also has no anchor, while the CHANGELOG and the body say "before dispatching". The check also cannot see two sessions started in the same directory, so the body's "a second session leading from the same clone sees the first one's checkout" holds only when that session uses a second worktree. Fix, at the same length: "Before dispatching, the lead runs git worktree list; if another worktree has the shared branch checked out, ask the user."

3. The lost-report path depends on the receiver knowing about the handoff. claims.md says that without a report, the integrator "waits for the lease to lapse. After a lapse, it reads any note left, looks for that branch". When a report is lost, the receiving session usually never learns that a handoff happened. In that case, after the lapse one of its workers picks the leaf from work list, which does not read the board. It acquires the leaf, and that acquire replaces the expired lease, note included. It then redoes the leaf, and no rule sends it to the pushed branch. So the body's "a lost report therefore costs at most one lease term" holds only for a receiver that already knows. Fix: move the lookup to "Acquire and renew": before acquiring a target whose lease has lapsed, read its note in claim list and look for a handoff branch for its article_id.

4. The obvious lookup misses branch names the rule allows, and the note names another branch. "A branch ending with the leaf's article_id" allows formalize-af_5b0e4d3c2a1f09e8d7c6b5a4, but git ls-remote --heads origin <article_id> only matches after a /. In a scratch repository it found handoff/af_0123456789abcdef01234567 but not formalize-af_5b0e4d3c2a1f09e8d7c6b5a4; the pattern '*af_5b0e4d3c2a1f09e8d7c6b5a4' did find that one. Separately, the note names the worktree's branch (L23-L24). For a package, that branch cannot end with every leaf's article_id, and another clone cannot see it unless it was pushed under that name. So "reads any note left, looks for that branch" can send the reader to a branch that is not on origin. Nothing removes the handoff branch after integration either, so a later lookup for the same article (for a revision, say) can find the old one. Fix: require "a branch whose last component is the leaf's article_id, such as handoff/<article_id>"; say that the note locates the worktree within its own clone and that another session searches by article_id; and delete the branch once the result is visible, when the request covers pushing.

5. Without claims, nothing reserves a package's untaken leaves. SKILL.md says the subagent "holds only the leaf it has taken". In a run without claims, the only exclusion is that the lead keeps workers from holding the same target at once (L56-L58), and after each integration the lead re-reads the frontier and dispatches again (L247-L249). Here is the sequence. Worker A gets the package {L1, L2} and integrates L1. The lead re-reads the frontier, sees L2 ready and held by no one, and dispatches worker B to it. Then A takes L2 as well. With claims the board refuses one of them, though the prose gives only "not ready" as a reason to return the rest, not a refused acquire. Without claims nothing stops it. Before this PR the lead dispatched each leaf itself, so its own bookkeeping was enough. Fix, within the 254-line budget: "that the lead confirms together and dispatches no one else to until they return", and "at the first that is not ready, or whose acquire fails, the rest return to the lead".

6. The CHANGELOG states the message rule without its scope. "No message grants ownership or completes a leaf" (CHANGELOG) comes from claims.md, which applies only to runs that use claims. In a run without claims, the lead's confirmation is a message, and it is what lets a subagent edit beyond its targets (SKILL.md). Fix: "With claims, no message grants ownership; none completes a leaf."

Posted by Claude Code (session jackmccarthy-e8).