docs(fleet): Fleet 101, a teaching guide to Fleet and its formal models - #329
docs(fleet): Fleet 101, a teaching guide to Fleet and its formal models#329itsHabib wants to merge 3 commits into
Conversation
One document that teaches Fleet top to bottom in the style of docs/workbench-101.md: an orientation block, verified/live/intent markers, a path:line citation for every claim, and a drift log. It covers the five rules, the store and the process that writes each file, the hook's six events, leases and CheckLease, rows and receipts, mail, the watcher's fold and one delivery end to end, and the Quint models (TLC, Apalache, the mutants, and the crash/replacement replay). It records the stuck "starting" launch record as an open gap without fixing it, and notes that the launch/reservation protocol has no model. Linked from cmd/fleet/README.md's Guides section and docs/README.md. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
@codex review |
|
@claude review |
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
|
Claude finished @itsHabib's task in 3m 28s —— View job Review: docs(fleet): Fleet 101
SummaryThis is a high-quality documentation PR with rigorous self-imposed standards. All spot-checked citations are accurate, the structure follows the workbench-101 pattern cleanly, and the drift log alone justifies the PR. The noted findings below are suggestions and minor observations — none are blocking. Spot-checked citations (all passed)
Observations1. Orientation block vs Section 4 completeness The Orientation screen (line 46) says:
Section 4 is more complete:
The Orientation explicitly says "read this for the shape; read the sections for the evidence," so the abbreviation is stylistically appropriate. However, the one omission worth considering: web tools and MCP tools being excluded from the hook has a security/trust implication (an MCP tool that writes files bypasses all lease checks), and this is exactly why Section 4 includes the fuller list. Consider whether the Orientation should at least say "read-only and MCP tools" to set the right mental model before the reader reaches Section 4. 2. Section 11 (line 1200) says:
This is accurate, but a careful reader will immediately ask: "if 3. The guide correctly marks the CI linkage as unproven: "The CI logs do not keep the bridge's log, so the two CI failures are consistent with this mechanism rather than proven to be it." This is the right epistemic standard. The reproduction methodology (serial vs parallel runs; 3/24 failures under load) is solid enough to treat as the likely cause. 4. The guide finds and proves a real weakness:
This is the sharpest finding in the guide. The invariant holds because of how 5. Drift log, second-to-last row:
Verified: 6. The watcher's "transitional interface" paragraph The drift log correctly flags
And notes: "Behind code since #318" and confirmed at 7. Five rules vs Four rules (OVERVIEW.md) The guide says "This guide follows the README" rather than OVERVIEW's four rules. This is a clean decision. The drift log records it at line 1302. Worth flagging for the follow-up where OVERVIEW gets updated: the missing "one holder per key" and "no domain word" from OVERVIEW are load-bearing rules that every operator needs to understand. README link additionsBoth link additions look correct:
The Structure qualityFollows workbench-101.md pattern exactly:
The 34-step delivery walkthrough in Section 8 (process → durable write → code citation for every step) is the guide's highest-value section. This is the kind of mapping that takes weeks to reconstruct from code; having it written down and verified is worth more than the rest of the guide. Minor nits
Findings recorded, not fixed (from PR body)All four recorded findings are correctly marked as not fixed:
VerdictNo blocking issues. The guide is accurate where checked, honest about its own limits, and provides genuine value beyond what's available anywhere else in the tree. The drift log is the most actionable section for follow-up work. The three structural suggestions above (Orientation wording, The PR body's "Do not merge yet" note is respected — flagging here for completeness rather than as a review verdict. |
|
Reviewer: claude |
There was a problem hiding this comment.
🟡 Changes recommended
The guide contains unresolved factual overstatements and misleading explanations that should be corrected before approval.
Get a fresh assessment by requesting another Copilot review.
Pull request overview
Adds an operator-facing Fleet 101 guide covering Fleet behavior, storage, leases, delivery, formal models, and known gaps.
Changes:
- Added
fleet-101.md. - Linked it from both documentation indexes.
- Made no runtime code changes.
File summaries
| File | Description |
|---|---|
docs/README.md |
Links the Fleet 101 guide. |
cmd/fleet/README.md |
Adds the guide under Guides. |
cmd/fleet/docs/fleet-101.md |
Comprehensive Fleet teaching guide; several accuracy corrections remain needed. |
Review details
Suppressed comments (7)
cmd/fleet/docs/fleet-101.md:473
- This overstates the two-record write:
cmdDispatchcallsCmdAssignonly whenslot != ""(cmd/fleet/internal/verbs/work.go:141-148), so an unseated dispatch writes only the dispatch row. Please qualify this paragraph to seated dispatches so operators do not infer that every dispatch has an assignment record.
A dispatch writes two records, the assignment and the row, and a failure between them can
leave an assignment that wakes its worker with no row. This is recorded, not fixed
(`FOLLOWUPS.md:63-79`).
cmd/fleet/docs/fleet-101.md:1304
- This drift entry says the new store table omits paths that the table itself lists:
deliver.json,handoff/,stop/,prs/,cache/github/,inflight/,costs.jsonl,actions.jsonl,hook-errors.jsonl,migrated-keys.v1,watch/delivery/,watch/late.json, andwatch/owner.lockall appear in section 3. Remove the false omission list and retain only the verified mail-path discrepancy.
| the store table | `cmd/fleet/README.md:78-90` | The mail path shows a raw `<tenant>` and `<address>` (`cmd/fleet/README.md:86`); the code uses their SHA-256 digests (`cmd/fleet/internal/fleet/mail_address.go:15-17`). The table also omits `deliver.json`, `handoff/`, `role-handoff/`, `stop/`, `last-word/`, `prs/`, `cache/github/`, `inflight/`, `locks/`, `decisions.jsonl`, `costs.jsonl`, `overrides.jsonl`, `actions.jsonl`, `hook-errors.jsonl`, `migrated-keys.v1`, `watch/delivery/`, `watch/late.json` and `watch/owner.lock` (section 3) |
cmd/fleet/docs/fleet-101.md:99
roles.jsonis present in this new guide itself, so the parenthetical is literally false even though the intended claim about the implementation is sound. Limit this statement to Fleet source code so the guide does not contradict its own text.
never reads Org's registry (`roles.json` appears nowhere in `cmd/fleet`); the two share only
cmd/fleet/docs/fleet-101.md:692
- A successful
rundoes not guaranteeprocess_identity:processIdentityerrors are ignored atruntime.go:148, leaving a valid launch record with only the PID, which later producesunknownstatus. Qualify this as an attempted/available identity so the delivery evidence is not overstated.
| 13 | watcher | on success: launch record rewritten `status: "running"` with `pid` and `process_identity` (the process start time) | `cmd/fleet/internal/watch/runtime.go:147-152` |
cmd/fleet/docs/fleet-101.md:735
fleet receiptis not verifier-only: any live session may record any kind, with role/lane kept as provenance (receipts.go:42-70). This wording contradicts section 6 and can incorrectly teach workers that they cannot publish receipts.
| 28 | verb run by the agent | `acked_at` on each message it handled; a `handoff/` checkpoint; a receipt, if it is a verifier | `cmd/fleet/internal/fleet/mail.go:249-277`, `cmd/fleet/internal/verbs/keys.go:403-427`, `cmd/fleet/internal/verbs/receipts.go:108-129` |
cmd/fleet/docs/fleet-101.md:1077
- The gap is not recoverable only by deleting a file: the guide later documents manually editing the launch record or adding an exit file as another way to make
readLaunchaccept it (lines 1113-1116). Describe this as manual removal or editing, while retaining that no Fleet verb recovers it.
is a **progress** failure: a state from which nothing but a person deleting a file ever leads
back to a directory that can launch. A safety invariant cannot express that. A model of the
cmd/fleet/docs/fleet-101.md:865
- The model explanation conflates the model's atomic
writeaction with the implementation's locking.CheckLeasereturns through an unlocked same-session fast path atpolicy.go:385-391; only the contended acquisition and takeover path is insideKeyLock. Please describe the model step as an abstraction and call out this fast path, otherwise readers may infer that the lock closes races it does not.
- **The decision.** `action write(s)` is `CheckLease`, taken as one atomic step because
the real code runs it under `KeyLock`. Read it next to
`cmd/fleet/internal/fleet/policy.go:392-440`: free takes the key; the holder's own write
proceeds; a rival that is `Alive` or `Unreadable` is refused; a `Dead` rival's branch is
taken over and its resource refused (`cmd/fleet/model/model/reference.qnt:44-71`).
- Files reviewed: 3/3 changed files
- Comments generated: 1
- Review effort level: Lite
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
Copilot: scope at-most-once to started launches (a failed start gives its stamps back); two dispatch records only with --slot; process identity may be missing and then reads unknown; any live session may record a receipt; the model's atomic write abstracts CheckLease, whose holder fast path is unlocked; the stuck record needs removal or editing; roles.json is absent from Fleet's Go source, not from cmd/fleet; name the README's table in the store-table drift row. Claude: name web and MCP tools in the orientation; say present() never calls SessionAlive; cite reassign's dispatch write; note the judge's "12 steps" wording under its output. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
@claude review |
|
Claude finished @itsHabib's task in 3m 22s —— View job Review: docs(fleet): Fleet 101 (round 2)
Copilot Round 1 Findings: All 8 AddressedReviewed 1. Unseated dispatch two-record write (line ~473) 2. Drift entry false omission list (line ~1304) 3. 4. 5. 6. 7. Model atomicity conflated with locking (line ~865) 8. At-most-once claim for failed start (explicit comment) Also confirmed: the Orientation block now reads "Read, Grep, Glob, web and MCP tools never reach it" — matching section 4's fuller list. (The original round 1 review noted this discrepancy; it has been addressed in Independent Review PassNo blocking issues found. One observation worth noting: Present()-and-parent-unverified wording SummaryAll 8 copilot findings from round 1 are correctly addressed. The fixes are technically accurate, consistent with the cited code, and don't introduce new issues. The guide's internal consistency holds — the delivery walkthrough, the No blocking issues. Ready for operator read per PR body. |
|
Reviewer: claude |
Copilot: the orientation now says CheckLease locks only when the key is free or held by someone else, and allows the holder's own write through an unlocked read; walk row 12 is limited to cmd.Start() failures and points at the providerCommand and failed-rewrite paths that leave the starting record (section 11). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
@claude review |
Review disposition after two fix rounds (head d82d654)Status: held for the operator's read. Not for gate or merge until the operator has read the guide. Rounds
The cycle on Residuals: accepted or deferred
|
|
Claude finished @itsHabib's task in 3m 4s —— View job Review: docs(fleet): Fleet 101 (round 3)
Reviewed commit: Round-2 Copilot Fixes: Both Correctly AppliedFix 1 — Orientation locking behavior Copilot flagged that the orientation overstated
This matches Fix 2 — Row 12 start error table Copilot flagged that row 12 claimed every start error rewrites the record to
This is accurate and consistent with Independent Review PassNo new blocking issues. Two observations: 1. Windows parenthetical (optional, carried from round 2) Section 11 (line 1208–1209) reads:
The deeper point — that Windows sessions are always 2. Self-test Q1 alignment with preToolUse order (no issue) Self-test Q1 asks what happens when a session runs Review cycle positionPer SummaryBoth round-2 copilot findings are correctly and precisely fixed. The guide remains internally consistent across all three rounds of review. No blocking issues at this head. Ready for operator read per PR body. |
|
Reviewer: claude |
Independent design review: Fleet 101 (#329)Recommendation: SIMPLIFY. Keep the material, change its job. It is a useful engineering reference and incident investigation, but I would not publish this version as the primary first-reader introduction. Put a short, task-first explanation ahead of it, reconcile the operational guidance, and correct the concrete errors below. Preserve the operator's explicit read/merge hold. Fleet's direction is sound: editable responsibilities, one accountable lead for work, ordinary peer questions, independent occupancy/work/mail, optional Org, and provider adapters beneath one Go watcher. The evidence supports continuing that small design. It does not justify another hierarchy, compulsory lifecycle, policy engine, or general formal-verification platform. Subject and evidence boundaryReviewed 2026-09-12. Remote verified as
These heads/statuses were refreshed before writing this report and rechecked unchanged immediately before publication. API snapshots, test logs and overlay probes are retained with the local review artifact; they are not attached to this comment. Read all 1,331 lines of the proposed guide, both index changes, repository charter/instructions, relevant runtime/model source, installation/onboarding/run/headless/validation guides, and prior review dispositions. There is no scoped #329 has already used its three panel cycles. All three inline threads are resolved/outdated; I verified the ten recorded corrections and do not reopen them. Claude reviewed the final head; Codex's bot review was unavailable due to quota. This report is the requested independent design review, not another panel request or merge authorization. Ranked findings and changes1. High design priority: replace the first-reader path, retain the referenceText: “learn the whole thing from one document. Read it top to bottom” (guide lines 3–7). The orientation says an agent can stop there and return to leases and watcher details (lines 29–30). Demonstrated structure: 13,159 whitespace-delimited words; a complete storage table starts at line 147, while mail starts at 515. There is no opening worked example of a lead answering a worker's routine question, no compact operational kickoff, and no direct initial path through install → run → inspect. A 34-step launch walk is excellent maintainer material. It is a poor prerequisite for dispatching one task. Judgment, not a measured learning result: the proposed reading order optimizes for reconstructing the implementation, not learning to coordinate work. No first-reader trial is retained. The README links it as the first guide, which makes that distinction consequential. Better alternative: reuse Replacement opening:
2. P2 accuracy/clarity: state the actual hook protection boundary before claiming ownership enforcementText: Fleet “refuses the writes that would break ownership” (lines 82–87); “A lease gates the next tool call the hook sees” (line 429). The orientation correctly warns that MCP writes bypass checks, and section 5 correctly describes the Git classifier. It never gives the equally important plain-language consequence for normal shell writes. Demonstrated: Consequence: reaching a hook does not establish branch-lease coverage. This is broader than the already-fixed MCP omission, and independent of the correctly documented surviving-child limitation. It is a misleading summary, not a newly discovered runtime regression. Replacement:
3. P2 current-main drift: refresh the request handoff and #324's actual open questionText: row 11 says the request is copied to stdin by a goroutine (line 692); section 11 calls request loss “open” (1155); The source-snapshot disclaimer is honest: stdin was correct at #324's latest evidence identifies the extensionless Windows binary as a sufficient explanation and asks for a rerun after #325. Its unconditional programmatic-callback patch was not adopted. Real macOS settings-file hooks fired, including SessionEnd. Current official SDK documentation explicitly includes settings-file command hooks when their setting source is enabled. That supports investigating setup first; it does not qualify Windows. Replacement status:
Refresh the current-operation section and immutable source links together. Keep the old race as a case study, with its fix and residual, rather than deleting useful history or silently repinning old line numbers. 4. P2 clarity: define the operational reply/escalation route without implying Org hierarchyText: unacked questions are mailed “to the addressee's parent” (lines 561–567), after Org was introduced as a registry with an optional parent. Demonstrated: Replacement:
Teach “only the top lead routinely asks the operator” as the run's working agreement. Do not enforce mandatory hops or make workers wait for charter traversal. Approval/refusal boundaries still apply wherever the provider or repository requires them. 5. P2 accuracy: self-test Q7 teaches the wrong release ruleText: “The bridge exited 0 but The question is underdetermined. Replacement:
Existing documentation conflicts that affect adoptionThese are disposition work, not fresh runtime bugs. #329 already records much of the drift; do not inflate that into a second finding list. Merely appending another drift ledger leaves several active instructions in disagreement.
The headless guide also calls all of app-server “experimental.” Today's official reference distinguishes a stable surface from opt-in experimental methods. Qualify the particular installed methods/version instead. This is a small external-documentation refresh, not evidence that Fleet's platform integration is qualified. Formal methods and reliability directionProceed with the existing bounded examples. The guide correctly distinguishes model safety, finite-state exploration, synthetic session records, real helper processes, the hand-projected resource trace, and lack of Go refinement. I reran Do not use a bigger model as the next deliverable. The unlabelled-takeover result means the property needs an independent observation of ownership transitions and explicit takeover authorization if that model is extended. Do not add more labels that only the implementation of the mutant can emit. Replay frozen witnesses through ordinary Go paths; add model checking when a specific interleaving question warrants it. Whole-Fleet proof is neither offered nor earned here. The proposed progress property at lines 1084–1091 needs one qualification: “every state has a path back to free” proves recoverability, not that the system will take that path. Eventual recovery needs stated assumptions about watcher restart, scheduling and successful I/O. An indefinitely uncertain effect may correctly require operator action. A bounded claim such as “on the next healthy fold after a proven pre-start failure, this address can retry” is smaller and directly testable. Preserve safety when the provider may have started. Simplify the planned crash-point work into one retained regression and repair. The The first repair should handle a proven no-start error: retain the failure reason, settle the launch as failed, and keep the request eligible. A crash after spawn but before PID publication is a different, uncertain case; do not make it retryable through age or fabricated terminal evidence. Define one supported inspection/recovery action before generalizing a crash injector. The existing manual deletion discussion honestly warns about duplicate launches, but a newcomer should leave with “preserve evidence and escalate an unresolved start,” not a quiz answer encouraging an invented exit file. Keep the existing macOS no-fork observer narrowly scoped. It earned some value through a reproduced pre-turn failure, but it is not a descendant container or a platform-neutral termination guarantee. More OS machinery should follow a measured failure in the intended workload, with an ordinary process-supervision baseline, rather than a desire to make the architecture look complete. What the workload evidence actually supportsThe retained run 7 scorecard reports two workers, one lead, one verifier, a contended bench, 16 Claude turns, two draft PRs, two verify receipts and zero post-start operator interventions. I read its contract and scorecard and checked the retained That is useful real evidence for question/answer, dirty-work continuation, contention relay and lead closure. It is not a current-main full-workflow repeat or controlled evidence of cost superiority. The earlier provider ledger and #318's final comments preserve both failed attempts and version boundaries. Codex has real fresh/resume/cancellation and bounded sandbox evidence; the macOS pre-turn failure probe is controlled injection with explicit recovery, not unattended success. Windows packaging CI and cross-builds do not establish Windows headless hooks or process cleanup. #324 still needs that machine's evidence. Smallest valuable slices and falsifiable criteria
The next broader run should keep tasks, model settings and setup comparable to a desktop baseline and count completed accepted work, operator rescues, idle assigned time, coordination spend and recovery failures. If extra leads or recurring ticks do not reduce an observed bottleneck, remove them. Fresh-agent kickoff using current supported behavior
Validation and handoffAt Only genuinely operator-owned choices remain: whether this should remain a single physical reading artifact; whether the next deployment target is Windows (making #324 qualification the immediate prerequisite); and the authorized boundary/budget for the separate recovery repair and real workload. My defaults are a short front door plus reference, the platform you actually intend to use, and the smallest direct recovery test/repair. More hierarchy and formal tooling need no decision now because they have not earned a place. This comment is the operator-authorized publication of the independent review handoff. No Fleet handoff/receipt was written because the review instruction explicitly forbids runtime-state changes. Next action: operator reads this review and #329; a separately authorized documentation pass can apply the replacements without reopening the exhausted panel cycle. Preserve the merge hold until the operator explicitly releases it. |
Independent review: Fleet 101 and Fleet's directionReviewed 2026-09-12. Verdict: SIMPLIFY. Proceed with editable role prose, optional Org, Fleet-owned occupancy/work/mail, direct peer coordination and one headless launch owner. Preserve Fleet 101's forensic detail as an implementation reference. Replace the compulsory top-to-bottom introduction with a short path through one useful task. Stop treating a future crash harness as a reason to retain a known recoverable runtime defect. #329 remains held for the operator's own read. This review neither supplies merge authority nor requests another review-panel round. Verification used isolated checkouts. This comment publishes the completed review with the operator’s subsequent authorization; it does not authorize implementation or release the merge hold. Writer #5 and Rooms were excluded. Revisions and review state
#329 has three Claude attestations, including its current head. Copilot's three inline threads are resolved and outdated; its latest summary generated zero new comments. Codex review was unavailable through usage limits. Required-looking check entries returned success; that is neither independent factual completeness nor permission to merge. I read the reviews and checked the repaired locking/start-error passages rather than reopening them. The repository's two-fix-round cap has already been reached. The shared checkout contained an unrelated change to Ranked findings and exact correctionsThe order below is practical importance. R1 is an existing reliability/design problem, not a runtime regression introduced by this documentation PR. The remaining findings distinguish #329 text from the wider documentation set. Their corrections are recommendations for the operator's read and a bounded follow-up, not an instruction to restart the exhausted panel. R1 — High design priority: a future experiment should not require keeping a known pre-spawn failure in serviceExact text: “It is being kept unfixed as the first target of the planned crash-point test harness” — Fleet 101, section 11, lines 1152–1153. #330's body likewise says the The guide accurately identifies the problem. The direction is what I challenge. Independent reproduction: a review-only constructor fixture returned an error before spawning anything. On both #329 and current main, the record remained Better alternative: freeze the reproducer against the old SHA and make a focused pre-spawn repair. Prepare the command and its durable request before publishing Proposed correction: “Known constructor failures occur before any process exists and should be recoverable in a focused fix. Preserve the old behavior as a regression fixture. Crashes spanning process start remain a separate, unresolved recovery boundary.” Do not respond by teaching routine JSON deletion. The guide already explains that deletion can permit a second launch while an unrecorded bridge survives. Retained mail bytes also do not establish eventual delivery: stamped unacked mail needs a later session, and an indefinitely blocked address may never get one. R2 — P2, #329: the opening ownership guarantee omits ordinary shell writesExact text: “it refuses the writes that would break ownership” — lines 85–87. The orientation explicitly warns about MCP writes, but not ordinary Bash file writes.
Section 5 lists the recognition rule, but leaves the reader to infer this consequential limitation. “The hook sees it” and “the branch lease checks it” are different questions. Lane resource requirements and provider permissions can still refuse a call for separate reasons. Proposed correction: “Fleet keeps one recorded holder and gates recognized future tool admissions. Ordinary shell programs and redirections can write without a branch-lease check; tools outside the matcher bypass the hook entirely. It does not isolate files or stop already-running effects.” Put this beside the orientation's lease rule, with the Do not try to make shell regexes into a security boundary. Keep separate worktrees as the baseline. A workload requiring effect isolation needs an enforced filesystem/resource boundary or process containment; adding more role permissions does not provide it. R3 — P2, #329: refresh the teaching path for merged #330, not just its “open gap” headingExact text: “with the request on stdin” — delivery step 11, line 692; “A one-shot fold can lose the bridge's request (open; found while writing this guide)” — section 11. The historical snapshot marker is honest. It does not make an obsolete default learning path useful after #330 merged. Current Proposed correction: “Fixed on main by #330 ( Update the orientation, store table, delivery step 11, failure triggers, unmodeled-boundary list, section 11, self-test 13 and attempt glossary together. Retain the old stdin schedule as dated historical evidence in the reference. The statement that command construction “can fail only” on executable lookup or encoding is no longer true. Re-pin changed source citations after the update. #330's own body already requests this reconciliation; do not take over or reopen its fix. R4 — P2, teaching direction: make the simple path primary and hierarchy optional in the actual examplesExact text: “Read it top to bottom” — Fleet 101 lines 3–7. “Decide the tree” and “One overall lead. One lead per bucket of work” — ONBOARDING lines 14–17. Fleet 101 is 1,331 lines. Its first substantive journey is through rules, storage and leases, followed by a 34-step delivery trace and formal methods. This is a valuable maintainer reference, but a costly first encounter. Onboarding's prose calls roles optional while its commands still seed multiple workers and bucket leads. The README's “workers talk to their lead, never to the operator” also presents one workflow as the universal shape. The newer boundary spec and Proposed correction: “Start with one task owner in one worktree and one accountable lead. Add a separate verifier when acceptance requires independent checks. Add a second worker, resource lease or second lead only when the work requires it.” Split the reading paths rather than duplicating their content. Keep a short Fleet 101 with one task, one question, one handoff, one exact-head verification and one failure example. Move or relabel the existing detailed sections as Fleet runtime and model reference. Reuse R5 — P2, #329: distinguish runtime observations from an agent's evidence claim at the point of introductionExact text: “Facts come from hooks, never from an agent” — line 122; “Each is enforced somewhere specific” — lines 106–107; “Done is evidence” — lines 142–145. The detailed receipt section correctly says independence is not checked. The opening still invites the inference that Fleet establishes that a task really passed. Proposed correction: “Runtime activity is observed from hooks and process evidence. Assignments, handoffs and receipts are authored records. Keep receipts lightweight and authority-free. Do not repair the wording by adding an Org permission chain or a mandatory second receipt product. The same distinction belongs in the one-screen orientation; readers are expressly told they can stop there. R6 — P2, #329: “parent” conflates Org discovery with Fleet lateness routingExact text: an overdue question goes “to the addressee's parent” — lines 560–566. Earlier the guide introduces Org's optional parent reference, but never mentions
Proposed correction: “An overdue unacknowledged question is reported to the seat's latest accountable R7 — P2, #329: self-test 7 teaches the wrong release conditionExact text: “The bridge exited 0 but The answer does not follow from the premise. Proposed answer: “Not enough information. Exit alone is insufficient; matching never-started evidence or the supported quiescence proof can also free it. Otherwise it stays reserved.” Alternatively add “and neither other release proof exists” to the question. This is a factual correction, not a demand to change release behavior. R8 — P2, documentation set: platform qualification statements lag the evidence, and #324's current next step is misstatedExact text: “Everything measured so far was measured on a Mac with Claude” — ONBOARDING line 5; “nothing so far is Windows or Codex acceptance” — e2e line 124; “#324, the programmatic-hook follow-up” — Fleet 101 line 1223.
Issue #324's current update reports that macOS SDK-launched settings hooks do fire, including SessionEnd. It points to the extensionless Windows binary as a sufficient explanation and requests a Windows rerun using Proposed correction: “Bounded macOS workflows have been exercised with both providers; this larger scenario and Windows headless behavior require their own evidence. #324 awaits a Windows rerun after #325. Additional hook registration is conditional on that result.” Link the existing evidence ledger instead of duplicating a timeless qualification claim. Do not implement the obsolete patch from the issue body. What the code and evidence supportProceed with the role boundary. Org's actual Proceed with provider-neutral coordination, with bounded adapter claims. Go owns scheduling/reservations; the embedded bridge translates Claude SDK or Codex app-server lifecycle. Neither adapter should own another scheduler, mailbox or organizational policy. Protocol fixtures and recorded workflows establish useful mechanism behavior. They do not establish equal operating cost, identical platform guarantees, or effortless headless setup. Codex hook trust, Claude settings, and the macOS-only process observer remain explicit adapter differences. Keep leads useful rather than hierarchical. Their job is to answer routine scope/fact questions, reconcile evidence, unblock actual contention and retain accountability. Peers can answer one another directly. Decisions outside their scope still belong with the operator. A child-to-parent-only route or an extra lead for every repository would add delays without demonstrated benefit. Hooks are admission guards; OS observation is narrower than OS isolation. The existing no-fork observer is a defensible bounded cleanup mechanism: it arms before exec and requires matching attempt evidence. It does not contain descendants, and any fork disqualifies the no-fork proof. Normal provider-terminal evidence is not an all-descendant quiescence theorem. Keep the existing conservative resource rule. Choose a process-scope/fencing experiment only for a concrete workload with surviving effects; do not start a generic OS or sandbox project from this review. The formal work is useful, but its strongest contribution is a counterexample. I independently ran The models assume atomic admission and omit the watcher launch protocol, arbitrary shell writes, real hooks, restart/PID reuse, multi-key behavior and filesystem failures. QuiescentBranch's guard is an oracle. No safety-model result proves implementation refinement or eventual progress. Process-kill tests also do not qualify power-loss durability of multi-file state. Keep these scope boundaries with the model output. A later repair of Smallest valuable next step and experimentNext reliability change: the pre-spawn constructor-failure repair in R1, with one regression that fails on current main and passes after the change. Keep one adjacent control for a possibly-started attempt remaining reserved. This needs neither a generic crash injection framework nor a new launch state machine. The proposed fresh-agent kickoff appended below names the exact starting head, checks and exclusions. Next teaching change: after the operator reads #329, promote one short workflow and preserve the long text as its linked reference. Make R2/R3/R5–R8 concrete residual corrections, not another broad review exercise. Next usefulness trial, when separately authorized: use a real small repository bug with one owner and one independent verifier. Compare the existing desktop/native coordination baseline with Fleet mail plus watcher on matched tasks and acceptance. Record operator rescues, coordination turns/cost, idle assigned time, preserved dirty work and time to an independently checked draft. Use both providers only if parity is the question being tested. Run 7 is positive coordination evidence, but its actual deliverable is a four-line Markdown file with prescribed unit questions and a bench script. It is not evidence of better software delivery. Its reported 16 turns, $3.44 and zero rescues are scorecard observations, not independently recomputed raw telemetry in this review. The exact frozen runtime SHA is also not supplied by “ For the next small trial, require no lost work, no unsafe overlap and no manual JSON repair. Predeclare the maximum spend and compare completed acceptance, not token counts alone. If Fleet does not reduce operator intervention or meaningful waiting enough to justify its setup and coordination cost, retain the desktop baseline and stop expanding the runtime. Add neither hierarchy nor formal machinery to rescue a failed usefulness hypothesis. Verification record and limitationsAt pristine #329 head:
At pristine current main: Tools: Go 1.26.5, darwin/arm64; Node v26.5.1; Quint 0.32.0; Codex CLI 0.153.4. Logs and probe source are retained in the originating Codex task; local-only paths are not presented as GitHub-accessible evidence. The two review-only path mistakes were corrected before the recorded model/probe runs; no failing substantive check was discarded or converted to a pass. Full repository-wide tests, live provider calls, Windows execution, raw private rehearsal telemetry and real-harness shell admission were not rerun. Existing CI and rehearsal observations are identified as retrieved evidence above. Read scope: repository AGENTS/CLAUDE and design charter; the complete #329 guide and diff; Fleet README, install, overview, minimum, onboarding, run-a-fleet, headless, e2e and provider validation guides; Org guide and actual card implementation; the full Org/Fleet boundary spec; relevant followups; Go admission/lease/session/role/receipt/mail/delivery/recovery code; the complete Node bridge and macOS observer; model ledgers, source map, reference/crash models, mutants and process replay; both PRs' reviews and #324 updates; run-7 contract and scorecard. Citations point to the examined revisions, not an assumption that the shared installed Fleet binary matches them. Proposed fresh-agent kickoff (separate implementation scope)Proposed fresh-agent kickoff: Fleet pre-spawn recoveryThis is a proposed task for the operator to adopt after reading the review. The current review did not authorize implementation, remove #329's hold, or supersede the operator's earlier choice to retain the gap. Do not execute this packet merely because it exists. If adopted, use this prompt:
Separate follow-up only after this slice: characterize the genuine watcher-death window before and after process start, keeping an ambiguous surviving provider reserved. Extend recovery only when the implementation can distinguish no process from possibly surviving effects. A generic harness is justified only if repeated concrete cases need the shared mechanism. |
|
Workbench queue ownership is now tracked in the local Fleet improvement task. Preserving the operator-read/no-Gate/no-merge hold at head |
|
The operator requested concrete teaching improvements and left the Workbench/Fleet document structure to us. Follow-up #335 now reconciles both independent SIMPLIFY reviews at Workbench 101 is the short entry/reading map; Fleet 101 stays a focused linked chapter beside install/run guides. This PR's detailed text is retained as a dated runtime/model reference. The new path covers one assignment, a peer question, handoff and exact-head completion, and corrects the shell-write boundary, authored receipt claims, lateness routing, historical transport and qualification wording. A separate independent verifier passed the final documentation head; validation and per-finding dispositions are in #335. This replaces the proposed first-reader structure, not your review history. #329 stays open and held for operator read; no merge, closure, Gate call or fourth reviewer-panel cycle is being performed. Runtime defects remain with the existing Fleet reliability owner. |
Summary
Adds
cmd/fleet/docs/fleet-101.md: a teaching guide to Fleet and its formal models, written so the operator can learn the whole thing from one document. It followsdocs/workbench-101.md: a one-screen orientation,verified/live/intentmarkers, apath:linecitation for every claim, and a drift log at the end. It is linked from the Guides section ofcmd/fleet/README.mdand fromdocs/README.md.Do not merge yet. This is an operator-facing teaching doc. It is held for the operator's own read: no gate run and no merge until they have read it and said so.
What it covers
~/.fleet, with the process that writes each file: hook, verb, watcher, the watcher's exit goroutine, the Node bridge, the macOS process observer.verbs/role.go:141,:167): Read, Grep, Glob and MCP tools never reach it.CheckLease; dead vs unreadable holders; takeover, revoke and release; wherepreWriteVerdictsandswitchDestinationsapply it; what a lease does not stop.fleet done.TestCrashReplacementModelTracereplays the frozen trace against real Go and a real process tree.Findings recorded, not fixed
startinglaunch record (deliberately unfixed; kept as the first target of the planned crash-point harness). If the watcher dies betweenrun()writing the launch record asstartingand rewriting it asrunning,readLaunchrefuses every fold,watch releaseandwatch cancelboth refuse (processStateisunknownfor pid 0), and the reserved mail stays stamped. Only deleting the launch file by hand clears it. Re-verified at5f9d837and again atea76b62with a throwaway test (not committed). The same state is reachable without a crash whenproviderCommandreturns an error (watch/runtime.go:134-137). The Simplify Org roles and make headless Fleet observable #310 review raised this as P2-5; it never reached that PR's dispositions orFOLLOWUPS.md.main's red CI).provider.Commandpasses the request viacmd.Stdin = strings.NewReader(...), soos/execcopies it from a goroutine;fleet watch --oncecan exit before the copy, and the bridge dies on empty stdin (SyntaxError: Unexpected end of JSON input) with its mail stamped and the directory reserved. Reproduced 3 of 24 runs under parallel load atea76b62.main's CI failures atdelivery-scenario.py:121(on779cb75andea76b62) are consistent with it; the CI logs don't keep the bridge log, so that link is not proven. The fix is split into its own task, not this PR.present()applies no age limit (watch/deliver.go:374-393). A throwaway test confirmed a 30-day-oldparent-unverifiedrecord, whichSessionAlivecalls dead, still prevents a launch.noSilentResourceTakeoverpasses because no action in the reference records aSilentfact; its mutant fails it only because the mutant adds that label itself. A scratch copy of the mutant without the label passes all four invariants under TLC. The "no silent resource takeover" property holds by construction ofwrite/takeover, but no invariant checks it.--max-steps. Measured at 6, 12, 20 and 30 steps (reference modules) and 3 and 12 (crash modules): TLC explores the complete reachable graph every time (325, 349, 20 and 26 distinct states, nothing left on the queue). The "to twelve steps" wording inmodel/README.md,CLAIMS.md,CRASH-REPLACEMENT.mdandjudge.shunderstates the result.watch/; the README and the boundary spec still call provider sessions future work;fleet donedoes not read receipts posted to pull requests.Validation
mainatea76b62(Record run 7 and clear a stale refusal from completed turns #328). Everypath:linecitation (422 unique) resolves to an existing range, and each was read against the cited code; citations in files Record run 7 and clear a stale refusal from completed turns #328 changed were re-pinned after the rebase.(cd cmd/fleet/model && ./judge.sh)on macOS, Quint 0.32.0:ALL CHECKS PASSat5f9d837(exit 0, 33 s) and again after rebasing ontoea76b62. The output is reproduced in section 9.gofmt -l .clean;go vet ./...clean;golangci-lint run ./...0 issues;go test ./...ok (88 packages).No code changes.
🤖 Generated with Claude Code