@@ -301,6 +301,9 @@ as UDP publication refuses without starting a cold pool. Admitted builds use
 review-only image placeholders for this check; startup still builds or selects
 the real image and repeats its review before graph admission. Missing or invalid
 static-review metadata refuses before boot and names the preflight command.
+Detached `up` identifies a static refusal as “nothing was started” and names the
+configuration fix and preflight command. Failures after startup begins retain
+the guidance to inspect the run and preserve its recovery evidence.
 The standalone preflight does not cover:
 
 - A project with native project inputs: a native project file
@@ -4081,3 +4084,32 @@ A publisher crash has a different effect: the owner reports the exit and keeps
 the services running, with that published port marked down in `ps` and `status`.
 Run `hack down` to stop the project with data retained. A publication notice is
 not evidence that cleanup completed, and no publisher is restarted automatically.
+
+Publisher exit observation never waits for the provider lease in the owner's
+event loop. If another operation holds that lease, `ps` already marks the port
+down and the runtime degraded. The owner retains the unreaped child and retries
+the identity-bound journal commit; it announces the exit only after that commit.
+Ctrl-C and authenticated `down` remain available. Healthy sibling publications
+keep following their admitted restart policies; an exited publisher's own service
+generation cannot recreate that publisher or rearm its route probe.
+If one service has several publications, losing one pauses restart following for
+all that service's publications until an explicit restart; other services continue.
+Replacement readiness checks that replacement's own child and publication, so a
+retained sibling exit (pending or committed) does not stop unrelated services.
+Fresh startup still requires every publisher live. A replacement port conflict
+requires that replacement's committed exit and an occupied port; its own live
+listener is never classified as a conflict because another publisher exited.
+
+New macOS frontend finalization records include the process birth time. Retaining
+recovery can distinguish a reused PID without signalling its replacement. A
+matching zombie also counts as exited. Unreadable identities refuse; records
+without a birth retain their PID-only behavior. Linux does not compare `ps`
+births because clock corrections can change that observation. Failure to capture
+the frontend's own birth falls back to the legacy behavior instead of failing up.
+
+A pool started by a different provider version reports `provider_pin_changed`
+through `ps --json`, detached `up` and `exec`, with the same original-release or
+home-retirement guidance. This does not migrate the pool or permit cleanup by a
+different provider version. When publisher identity cannot be confirmed, recovery
+explains that it waits for the process holding that PID to exit and names
+`hack down --recover` as the retaining retry.
@@ -6,7 +6,17 @@ stateDiagram-v2
     [*] --> ready
     ready --> enrolled : Interrupt
     ready --> enrolled : FrontendLost [lifetime watch]
-    ready --> publisher_down : PublisherCrash [exact Child reaped]
+    ready --> publisher_pending : PublisherCrash
+    publisher_pending --> publisher_down : CommitExit [lease acquired]
+    publisher_pending --> enrolled : Interrupt or FrontendLost
+    publisher_pending --> intent : Recover [owner absent]
+    state "publisher-exit-pending" as publisher_pending
+    note left of publisher_pending
+        Port down; services remain running
+        Provider busy retains the zombie
+        No committed proof or notice yet
+        Retry without blocking stop control
+    end note
     publisher_down --> enrolled : Interrupt or SIGHUP
     publisher_down --> enrolled : FrontendLost [lifetime watch]
     publisher_down --> intent : Recover [owner absent]
@@ -20,7 +30,8 @@ stateDiagram-v2
     ready --> intent : Recover [owner absent]
     enrolled --> intent : Recover [owner absent]
     intent --> intent : StopPublisher [identity matches]
-    enrolled --> bridge_retired : ReleaseBridge [publisher absent]
+    enrolled --> enrolled : CommitExit [lease acquired]
+    enrolled --> bridge_retired : ReleaseBridge [exit proof committed]
     intent --> bridge_retired : ReleaseBridge [proof current]
     bridge_retired --> intent : Recover [owner absent]
     bridge_retired --> stopped : CleanupGuest [proof current]
 
@@ -37,7 +37,7 @@ must be attached to the eventual exact integration revision.
 | Property and critical states | Model coverage | Implementation/regression boundary | Remaining qualification |
 | --- | --- | --- | --- |
 | Native log follower versus lifecycle mutation, frontend loss, stopped container and transport loss | No new state model: the follower observes without a mutation lease and grants no cleanup authority | `provider/graph/log_follow.rs` and its native counterpart pin Ready admission, container and start generation; `provider/engine/log_follow.rs` bounds framing and distinguishes real EOF from stopped-service idle cutoff. `lifecycle_log_follow_tests.rs` keeps the production transport on a fake Engine socket active while acquiring startup and operation leases, with a same-lock contention control and output while each lease is held. `native-log-follow-source.test.ts` guards the observer-only route; process tests cover cancellation, frontend loss, truncated/partial output and idle end reasons | 4 KiB envelopes, 8 KiB wire lines, 64 Ki-character retained line prefixes. The portable lease test fakes identity/state checks; it does not exercise host process/disk auditing, graph admission or the VM relay. Real relay EOF on stop/down/restart, VM loss and concurrent lifecycle latency require Apple Silicon acceptance. No performance or whole-product parity claim. |
-| Foreground group interrupt; publisher exit before authenticated stop; dead owner's pending cleanup enrollment and bridge release | native-publisher-stop | [Process adapter](../../src/backends/native-project-process.ts) isolates Compose owners regardless of hooks; Rust `process::publisher_command` isolates publishers; `legacy_cleanup_enrollment` binds the old coordinator and inventories before a distinct recovery intent. [Group regression](../../tests/native-foreground-group-interrupt.test.ts) signals the whole group for fresh/restore owners; Rust real-publisher process, frontend-loss, exact child-reaping and enrollment tests check grouping, lifetime wakeups and stale selectors. | One graph, one publisher, one crash, one identity replacement and one audited successor boot; 110 states. SIGHUP requests retaining cleanup; a reaped publisher enters an observable publisher-down state until explicit stop. Native process tests and frontend framing/ps tests cover signal delivery and notices. Dependency release is a separate post-completion step; `NoStrandedReservation` rejects success with a held reservation. Real reservation-file regressions check retry, capacity reuse and refusal fences. Separate stopped-receipt and intent-completion commits are collapsed; TypeScript dispatch and Rust completion-digest regressions cover that interruption window. Publication-registry sync/rename is abstracted and covered by portable commit-interruption tests. Kernel identity, socket/inode proofs, guest observations, durable storage and existing next.13 home recovery remain implementation/Apple Silicon VM gates. No eventual recovery is asserted. |
+| Foreground group interrupt; publisher exit before authenticated stop; dead owner's pending cleanup enrollment and bridge release | native-publisher-stop | [Process adapter](../../src/backends/native-project-process.ts) isolates Compose owners regardless of hooks; Rust `process::publisher_command` isolates publishers; `legacy_cleanup_enrollment` binds the old coordinator and inventories before a distinct recovery intent. [Group regression](../../tests/native-foreground-group-interrupt.test.ts) signals the whole group for fresh/restore owners; Rust real-publisher process, frontend-loss, exact child-reaping and enrollment tests check grouping, lifetime wakeups and stale selectors. | One graph, one publisher, one crash, one identity replacement and one audited successor boot; 168 states. Publisher exit observation is separate from lease-bound reaping/proof commitment; `NoUncommittedExit` rejects owner cleanup while proof is pending. A busy lease stutters without delaying stop control. SIGHUP requests retaining cleanup; a reaped publisher enters an observable publisher-down state until explicit stop. Native process tests and frontend framing/ps tests cover signal delivery and notices. Dependency release is a separate post-completion step; `NoStrandedReservation` rejects success with a held reservation. Real reservation-file regressions check retry, capacity reuse and refusal fences. Separate stopped-receipt and intent-completion commits are collapsed; TypeScript dispatch and Rust completion-digest regressions cover that interruption window. Publication-registry sync/rename is abstracted and covered by portable commit-interruption tests. Kernel identity, socket/inode proofs, guest observations, durable storage and existing next.13 home recovery remain implementation/Apple Silicon VM gates. No eventual recovery is asserted. |
 | Exclusive claims; competing writers; partial owner publication | graph-admission, registry-writer, publication-journal, missing-publication-lock, native-frontend-recovery | Admission/registry locks, pending publication and exact saved owner; related runtime ownership tests | Real filesystems, boot/incarnation identity and unsupported writers remain independent. |
 | Interrupted native restart: Ctrl-C or a frontend crash while the old run stops; `up` and `restart` refusing each other | native-restart-intent | The restart's stop requests run in their own process group (`processGroup: "own"` in [native-runtime-client](../../src/backends/native-runtime-client.ts)); a resumed `prepared` intent accepts a graph its owner stopped ([restart](../../src/backends/native-project-restart.ts), [preflight](../../src/backends/native-project-restart-preflight.ts)); [restart regressions](../../tests/native-project-restart.test.ts) send a real group SIGINT and cover the resume; HACK-2035 regressions force SIGINT/SIGTERM child rejection before frontend abort in preflight and down, using the runtime client’s preserved `stopSignal` | The finite model abstracts interrupt delivery as one action and does not prove child-exit versus frontend-handler ordering; deterministic tests cover that classification. A stale restart lock after a frontend crash; down hooks still share the terminal's group; physical guest acceptance. |
 | Foreground Compose startup failing after resources started; unconfirmed cleanup; unauthenticated final inspection | native-startup-owner | `recordFailedStartupOwner` in [native-project-start](../../src/backends/native-project-start.ts) publishes the authenticated failed run with a finalization lifetime; [start regressions](../../tests/native-project-start.test.ts) cover recording, an unauthenticated receipt and a retained mapping | A refused final inspection still leaves only the runtime journal; crash between finalization registration and mapping publication; physical guest acceptance. |
@@ -49,7 +49,7 @@ must be attached to the eventual exact integration revision.
 | Graph cleanup container stop batch: bounded in-flight stops, shared worker queue, connect-stage retry, batch-wide unreachable state, deadline expiry, worker panic | **Coverage gap:** no maintained model covers scheduling inside the stop batch; native-route-stop covers a different stop protocol | `dispatch` and `attempt` in [the stop batch](../../packages/runtime-core/src/provider/engine/stop.rs): at most 4 stops in flight, every worker joined; only `connect`/`connect_timeout` failures retry (25 ms doubling to 500 ms, within the batch deadline and 30 s of a stop's first connect failure); once one stop exhausts its window, later connect failures return at once; a deadline reached during backoff keeps the connect stage; `response`, `timeout` and `transport` never retry. Regressions in the same file's `provider::engine::stop` tests (bounded in-flight socket server, late socket, missing socket, 14-stop retry counts, persistent connect failures, oversleeping backoff, non-retried stages, worker panic) and `fourteen_service_connect_failures_keep_resumable_progress_and_retry_only_unstopped` | Tests cover exact attempt counts and the in-flight bound for fixed interleavings; no model explores all worker schedules or proves at most one delivered request per stop. Assumes a failed connect sent no request bytes and that the stop budget covers fully serialized grace periods. Graph-level resume after a partial batch is covered by tests only. Host qualification of the descriptor-pressure root cause (HACK-1302) remains open. |
 | Concurrent stop/publication; route claim and relay lifetime | native-route-stop, shared-https-lifetime, previous-boot-shared-https, relay-lifecycle-barrier, relay-authorization, relay-staging, relay-fence | Fenced route removal, relay owner, ready/removed protocol, authenticated observations | Native DNS/TLS/browser behavior; old-boot uncertainty and external routing. |
 | Shared host helper instance: overlapping ups, session adoption, stale create decisions, replacement before finalize, epoch-record failure, interrupted cleanup, concurrent down, displaced launches, failed down session stop | shared-helper-instance | `src/lib/project-shared-helpers.ts` (shutdown generation, `assertCurrent`, `SharedHelperSessionOwnership`); `src/lib/project-lifecycle-controller.ts` session decision, the locked creation transaction (revalidate, publish, create, environment, record, stop on failure, all under one lock), launches fenced by the lock and a token check, abort and signal cleanup through the same epoch decision (`runIfOwned`), an unknown exact-presence answer failing the inspection, and the locked conditional finalize; `stopSessionBeforeReleasingHelpers` (down, restart, native retirement keep holders when the session stop fails); `runMuxCommand` bounds every lifecycle and backend mux call so it settles before the lock is released, and reports a timeout as unknown (never absence); `tests/mux-command-timeout.test.ts`; `tests/project-lifecycle-controller-ownership.test.ts`, `tests/project-shared-helpers.test.ts`, `tests/native-project-down.test.ts`, e2e `shared-host-helpers` | Helper holder/rollback and claim protocol are not modeled (claim fixtures cover them); timeout settlement is an assumption the code does not guarantee (a killed tmux client's queued command may still apply, so a late kill or window command can reach a newer session; consequences and the session-ID fence, not in this slice, are in the README); zellij is refused for shared-helper lifecycle sessions (token written after creation); the gap between a down's session stop and its release (an up that captured after the stopping mark can still succeed there) is a documented first-slice limitation; real mux/process/lock-file behavior. |
-| Engine restart policies: stop versus pending restart, guest engine restart, stale incarnations, terminal proof | service-restart-policy | Receipt-admitted policy, disarm-before-stop and `restarting` stop preflight in `shutdown.rs`; admission refusals for incarnation-bound delivery classes in `restart_policy.rs`; owner-driven `Rebind` after full retirement, fresh ownership/attachment checks and a new reservation in `bridges/restart_rebind.rs`; route probe sample-generation rearm; Rust tests for admission, endpoint identity, port-busy refusal, disarm and stop preflight | Real guest engine behavior (crash restart, stop during backoff, disarm before deletion) needs native host evidence; several services, backoff timing and retry counting are not modeled. Same-port/route reachability after a policy restart, route probe rearm and per-slot child retirement still require real-VM host evidence. Rebind abstracts retirement/reservation/publication; relay lifecycle, fence and staging models cover their separate failure boundaries. |
+| Engine restart policies: stop versus pending restart, guest engine restart, stale incarnations, terminal proof | service-restart-policy | Receipt-admitted policy, disarm-before-stop and `restarting` stop preflight in `shutdown.rs`; admission refusals for incarnation-bound delivery classes in `restart_policy.rs`; owner-driven `Rebind` after full retirement, fresh ownership/attachment checks and a new reservation in `bridges/restart_rebind.rs`; route probe sample-generation rearm; Rust tests for admission, endpoint identity, port-busy refusal, disarm and stop preflight; portable selected-child readiness guard plus macOS two-real-child polling regression prevent historical sibling exits from rejecting a replacement or misclassifying its own listener | Real guest engine behavior (crash restart, stop during backoff, disarm before deletion) needs native host evidence; several services, selected-child readiness during sibling failure, backoff timing and retry counting are not modeled. Same-port/route reachability after a policy restart, route probe rearm and per-slot child retirement still require real-VM host evidence. Rebind abstracts retirement/reservation/publication; relay lifecycle, fence and staging models cover their separate failure boundaries. |
 | Foreground Ctrl-C down hooks: concurrent `down`, second interrupt, crash between or during hooks, stop during `up.after`, next generation | native-foreground-down-hooks | Value-free compare-and-swap journal in [down hooks](../../src/backends/native-project-down-hooks.ts), foreground orchestration in [foreground stop](../../src/backends/native-project-foreground-stop.ts) and `hack down` in [native down](../../src/backends/native-project-down.ts); [journal](../../tests/native-project-down-hooks.test.ts), [foreground](../../tests/native-project-start-stop-hooks.test.ts) and [down](../../tests/native-project-down-journal.test.ts) regressions | Durable writes are atomic in the model; real fsync/power loss, a stale journal lock after a crash inside the lock, and the live process-group behavior of the graph owner on a host are not covered. One generation and at most two `down` invocations are explored. |
 | Dependency rebind, automatic refresh, incomplete initializer, terminal reuse | dependency-rebind, dependency-auto-refresh, stopped-pool-startup, restore-history | Dependency claim/readiness, saved execution, restore history and source convergence tests | Actual installer failure, cache corruption, retained application state and resource plateau. |
 | Private environment allocation lifetime: staged values and private file members, crash between record and stage, retirement with the container | **Coverage gap:** no maintained model covers environment or credential delivery; file members share the existing allocation, intent record and retirement, so the state machine is unchanged | `packages/runtime-core/src/provider/environment.rs` (preparation bounds, staging layout, verification), `managed_environment.rs` (envelope v2 refusals, forwarding), `graph/launcher.rs` (read-only binds, overlap refusals) and `environment_recovery.rs` retirement tests | Live VM evidence that only the owning UID reads a member, writes fail read-only and the member is absent after cleanup; refresh or rotation of delivered files is not implemented. |
@@ -73,7 +73,7 @@ liveness/reachability controls have their own documented assumptions.
 
 | Model | Positive distinct states | Configurations |
 | --- | ---: | ---: |
-| [native-publisher-stop](../../tests/models/tla/native-publisher-stop/PublisherStop.tla) | 110 | 6 |
+| [native-publisher-stop](../../tests/models/tla/native-publisher-stop/PublisherStop.tla) | 168 | 7 |
 | [shutdown-rebase](../../tests/models/tla/shutdown-rebase/ShutdownRebase.tla) | 43 | 3 |
 | [native-plan-reconcile](../../tests/models/tla/native-plan-reconcile/Reconcile.tla) | 747,656 | 4 |
 | [native-cache-reconcile](../../tests/models/tla/native-cache-reconcile/CacheReconcile.tla) | 2,208 | 5 |