diff --git a/.github/workflows/spec.yml b/.github/workflows/spec.yml
new file mode 100644
index 0000000000..05fa3ce2f6
--- /dev/null
+++ b/.github/workflows/spec.yml
@@ -0,0 +1,73 @@
+name: formal specs
+
+# Re-checks the Git-on-object-storage models whenever they, or the script that
+# runs them, change. docs/spec/check.sh model-checks the protocol with TLC and
+# requires every seeded design error to be detected; docs/spec/lean holds a
+# machine-checked proof of the pointer discipline for unbounded parameters.
+
+on:
+  push:
+    branches: [main]
+    paths:
+      - "docs/spec/**"
+      - ".github/workflows/spec.yml"
+  pull_request:
+    paths:
+      - "docs/spec/**"
+      - ".github/workflows/spec.yml"
+
+permissions: {}
+
+concurrency:
+  group: spec-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  tlc:
+    name: TLC model check
+    runs-on: ubuntu-latest
+    # About three minutes on 16 cores; the hosted runner has fewer.
+    timeout-minutes: 45
+    permissions:
+      contents: read
+    steps:
+      - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        with:
+          persist-credentials: false
+      # The runner image provides Java; check.sh fetches TLC at a pinned
+      # version and verifies its SHA-256 before running it.
+      - name: Model-check the protocol and the seeded design errors
+        run: docs/spec/check.sh
+
+  lean:
+    name: Lean proof
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    permissions:
+      contents: read
+    env:
+      ELAN_VERSION: v4.2.4
+      ELAN_SHA256: 42b94d4244e8353142c456ec0e4ca6528fd898a6c604d4059f494e706e431f63
+    steps:
+      - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        with:
+          persist-credentials: false
+      - name: Install elan (pinned, hash-checked)
+        run: |
+          set -euo pipefail
+          archive=elan-x86_64-unknown-linux-gnu.tar.gz
+          curl -fsSL -o "$RUNNER_TEMP/$archive" \
+            "https://github.com/leanprover/elan/releases/download/$ELAN_VERSION/$archive"
+          echo "$ELAN_SHA256  $RUNNER_TEMP/$archive" | sha256sum -c -
+          tar -xzf "$RUNNER_TEMP/$archive" -C "$RUNNER_TEMP"
+          "$RUNNER_TEMP/elan-init" -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      # The toolchain is the one named in docs/spec/lean/lean-toolchain.
+      - name: Check the proof
+        working-directory: docs/spec/lean
+        run: |
+          set -euo pipefail
+          lake build 2>&1 | tee "$RUNNER_TEMP/lean.log"
+          # A proof that used `sorry` would build with a warning and would
+          # list `sorryAx` among the axioms it depends on.
+          ! grep -E "sorryAx|declaration uses 'sorry'" "$RUNNER_TEMP/lean.log"
diff --git a/Justfile b/Justfile
index e3e00a1ef2..7281f69788 100644
--- a/Justfile
+++ b/Justfile
@@ -545,7 +545,9 @@ test-unit:
         # off_mode_precedence_tests, and the git object-store
         # client and conformance-probe tests (api::git::store::tests and
         # ::fault_probe, which serves a fake S3 on loopback; the live-MinIO
-        # ::probe module stays opt-in). All are infra-free
+        # ::probe module stays opt-in), and the git push publish decision
+        # (api::git::cas_publish::tests and transport::track_c_tests, whose
+        # Postgres/MinIO cases are #[ignore]d). All are infra-free
         # and finish in well under a second with no DATABASE_URL, so none wait
         # out the sqlx acquire timeout. `--bin buzz-relay` adds main.rs's
         # `tests::` module (JWKS refresh cadence) and `composition_tests::`
@@ -563,7 +565,7 @@ test-unit:
         # cross-node fan-out ordering and drops; its hung-delivery case fakes a
         # database that never answers on loopback, and none use DATABASE_URL.
         cargo nextest run -p buzz-relay --lib --bin buzz-relay \
-            -E 'test(/^api::media_access::tests::/) + test(/^handlers::media_access::tests::/) + test(/^subscription::tests::/) + test(/^handlers::multinode_fanout::tests::/) + test(/^api::admin::/) + test(/^access::tests::/) + test(/^api::git::transport::access_log_tests::/) + test(=api::bridge::postgres_tests::nip98_replay_check_logs_only_its_refusal) + test(=api::bridge::postgres_tests::warn_only_artifact_read_lines_keep_the_filter_summary) + test(=connection::tests::close_totals_count_frames_the_writer_flushed) + test(=connection::tests::dispatcher_counts_each_req_and_count_frame_once) + test(=handlers::req::tests::unqueued_eose_logs_aborted_not_served) + test(=api::bridge::postgres_tests::reject_code_keeps_only_a_known_prefix) + test(=api::bridge::postgres_tests::nip98_replay_check_fails_closed_when_guard_errors) + test(=api::bridge::postgres_tests::verify_bridge_auth_rejects_nip98_event_signed_for_wrong_communitys_host) + test(=api::bridge::postgres_tests::verify_bridge_auth_can_require_payload_tag_for_json_body_endpoints) + test(=api::bridge::postgres_tests::verify_bridge_auth_accepts_nip98_event_signed_for_matching_host) + test(=api::bridge::postgres_tests::moderation_read_query_bearing_nip98_event_verifies_with_matching_query) + test(=api::bridge::postgres_tests::moderation_read_query_bearing_nip98_event_rejected_against_bare_path) + test(=api::bridge::postgres_tests::moderation_read_audit_query_bearing_nip98_event_verifies) + test(=api::bridge::postgres_tests::moderation_read_restricted_no_query_still_verifies) + test(=connection::tests::aborting_lifecycle_owner_is_drop_safe) + test(=connection::tests::shutdown_terminalizes_auth_stalled_on_database_before_late_success) + test(=connection::terminal_close_delivery_tests::upgrade_would_deny_line_without_auth_logs_absent_at_close) + test(=handlers::event::tests::observer_owner_cache_is_scoped_to_community) + test(=state::tests::shared_counter_between_direct_and_fanout) + test(=connection::tests::startup_cancellation_writes_one_close_line) + test(=connection::tests::connection_limit_refusal_writes_one_close_line) + test(=connection::tests::dropped_authenticated_handler_writes_one_close_line) + test(=connection::tests::missed_pongs_close_with_their_reason_and_count) + test(=connection::tests::client_reply_to_a_jittered_restart_closes_as_shutdown) + test(=connection::tests::client_close_racing_a_policy_disconnect_keeps_the_policy_reason) + test(=connection::tests::server_close_reason_ranks_shutdown_policy_then_cancellation) + test(=connection::tests::auth_timeout_after_a_rejected_auth_closes_as_auth_failed) + test(=connection::tests::close_totals_count_a_batch_flushed_by_the_drain_after_cancellation) + test(=connection::tests::close_totals_skip_a_frame_the_socket_rejects) + test(=connection::tests::close_totals_skip_frames_stranded_by_a_failed_flush) + test(=connection::tests::read_before_login_logs_one_denial_from_the_handler) + test(=connection::tests::read_refused_by_a_full_handler_semaphore_logs_one_denial) + test(=connection::tests::saturated_handler_write_line_records_whether_its_ok_was_queued) + test(=connection::tests::read_refused_by_unavailable_admission_logs_one_denial) + test(=handlers::auth::tests::repeat_auth_after_a_terminal_logs_one_denial) + test(=nip_fi_upgrade::tests::deny_protected_logs_one_denied_auth_line) + test(=api::bridge::moderation_refusal_tests::moderation_lookup_failure_is_unavailable) + test(/^push_runtime::/) + test(/^operator_listener::tests::/) + test(/^handlers::channel_authz::/) + test(/^handlers::moderation_authz::/) + test(/^handlers::side_effects::tests::/) + test(/^handlers::coalesced_refresh::tests::/) + test(/^handlers::system_channels::tests::/) + test(/^nip11::tests::/) + test(/^storage_sweep::tests::/) + test(/^nip_fi_core::tests::/) + test(/^nip_fi_http::tests::/) + test(/^nip_fi_policy::tests::/) + test(/^nip_fi_config::tests::/) + test(/^nip_fi_resolver::tests::/) + test(/^readiness::tests::/) + test(/^router::tests::/) + test(/^api::parse_query_tests::/) + test(/^api::db_read_error_tests::/) + test(/^api::profiles::/) + test(/^api::bridge::search_slots::tests::/) + test(/^api::git::transport::off_mode_precedence_tests::/) + test(/^api::git::store::tests::/) + test(/^api::git::store::fault_probe::/) + test(/^audio::join::tests::/) + test(/^audio::handler::tests::/) + test(/^nip_fi_gate::tests::/) + test(/^nip_fi_session::tests::/) + test(/^nip_fi_shadow::tests::/) + test(/^nip_fi_shadow_session::tests::/) + test(/^startup_steps::tests::/) + test(/^mesh_boot::tests::/) + test(/^telemetry::tests::/) + test(/^config::tests::/) + test(=state::tests::accessible_channel_invalidation_is_scoped_to_community) + test(=state::tests::accessible_channels_join_member_and_open_halves) + test(=state::tests::channel_deleted_invalidation_is_scoped_to_community) + test(=state::tests::neither_a_confirmed_inactive_community_nor_a_failed_lookup_admits_the_socket) + test(=state::tests::periodic_revalidation_disconnects_inside_the_fenced_callback) + test(=state::tests::bare_community_disconnect_fails_closed_when_the_fence_is_unavailable) + test(=connection::tests::send_loop_sends_policy_close_when_community_is_archived) + test(=state::tests::community_disconnect_then_nip_fi_keeps_community_deleted_reason) + test(=state::tests::disconnect_community_wins_reason_losing_nip_fi_does_not_enqueue_frame) + test(=handlers::req::tests::timed_out_historical_read_deregisters_before_closed) + test(=handlers::req::tests::superseded_timeout_leaves_replacement_intact) + test(=handlers::req::tests::search_claim_retires_live_and_yields_to_replacement) + test(=handlers::req::tests::failed_search_closes_without_eose_or_trying_later_filters) + test(=handlers::req::tests::concurrent_claims_and_stale_teardowns_keep_the_last_owner) + test(=handlers::req::tests::timeout_closed_is_emitted_before_a_replacement_can_claim) + test(=handlers::req::tests::revoke_then_replacement_keeps_replacement_whole) + test(=handlers::req::tests::revoke_of_a_replaced_holder_spares_the_pending_replacement) + test(=handlers::req::tests::superseded_or_closed_requests_cannot_claim) + test(=connection::tests::close_fences_a_req_whose_handler_has_not_run) + test(=connection::tests::only_the_newest_same_id_req_answers) + test(=handlers::req::tests::claims_after_connection_cleanup_are_refused) + test(=handlers::req::tests::dropped_terminal_frame_cancels_connection) + test(=handlers::req::tests::revoke_dropped_terminal_frame_cancels_connection) + test(=handlers::req::tests::count_fallback_covers_filters_that_can_match_private_deletions) + test(=handlers::req::tests::count_fallback_fetches_one_extra_candidate) + test(=handlers::req::tests::group_state_t_and_creator_tags_reach_sql_only_for_group_state_kinds) + test(=handlers::req::tests::empty_filter_sets_match_nothing_in_sql) + test(=api::bridge::postgres_tests::bridge_search_mode_extension_accepts_prefix_snake_or_camel_case) + test(=api::bridge::postgres_tests::bridge_search_sort_extension_selects_newest_only_when_named) + test(=api::invites::postgres_tests::restriction_tests::postgres_tests::destructive_fixture_rejects_shared_database_urls) + (kind(bin) & (test(/^tests::/) + test(/^composition_tests::/) + test(/^env_filter_tests::/)) - test(/^tests::postgres_tests::/))'
+            -E 'test(/^api::media_access::tests::/) + test(/^handlers::media_access::tests::/) + test(/^subscription::tests::/) + test(/^handlers::multinode_fanout::tests::/) + test(/^api::admin::/) + test(/^access::tests::/) + test(/^api::git::transport::access_log_tests::/) + test(=api::bridge::postgres_tests::nip98_replay_check_logs_only_its_refusal) + test(=api::bridge::postgres_tests::warn_only_artifact_read_lines_keep_the_filter_summary) + test(=connection::tests::close_totals_count_frames_the_writer_flushed) + test(=connection::tests::dispatcher_counts_each_req_and_count_frame_once) + test(=handlers::req::tests::unqueued_eose_logs_aborted_not_served) + test(=api::bridge::postgres_tests::reject_code_keeps_only_a_known_prefix) + test(=api::bridge::postgres_tests::nip98_replay_check_fails_closed_when_guard_errors) + test(=api::bridge::postgres_tests::verify_bridge_auth_rejects_nip98_event_signed_for_wrong_communitys_host) + test(=api::bridge::postgres_tests::verify_bridge_auth_can_require_payload_tag_for_json_body_endpoints) + test(=api::bridge::postgres_tests::verify_bridge_auth_accepts_nip98_event_signed_for_matching_host) + test(=api::bridge::postgres_tests::moderation_read_query_bearing_nip98_event_verifies_with_matching_query) + test(=api::bridge::postgres_tests::moderation_read_query_bearing_nip98_event_rejected_against_bare_path) + test(=api::bridge::postgres_tests::moderation_read_audit_query_bearing_nip98_event_verifies) + test(=api::bridge::postgres_tests::moderation_read_restricted_no_query_still_verifies) + test(=connection::tests::aborting_lifecycle_owner_is_drop_safe) + test(=connection::tests::shutdown_terminalizes_auth_stalled_on_database_before_late_success) + test(=connection::terminal_close_delivery_tests::upgrade_would_deny_line_without_auth_logs_absent_at_close) + test(=handlers::event::tests::observer_owner_cache_is_scoped_to_community) + test(=state::tests::shared_counter_between_direct_and_fanout) + test(=connection::tests::startup_cancellation_writes_one_close_line) + test(=connection::tests::connection_limit_refusal_writes_one_close_line) + test(=connection::tests::dropped_authenticated_handler_writes_one_close_line) + test(=connection::tests::missed_pongs_close_with_their_reason_and_count) + test(=connection::tests::client_reply_to_a_jittered_restart_closes_as_shutdown) + test(=connection::tests::client_close_racing_a_policy_disconnect_keeps_the_policy_reason) + test(=connection::tests::server_close_reason_ranks_shutdown_policy_then_cancellation) + test(=connection::tests::auth_timeout_after_a_rejected_auth_closes_as_auth_failed) + test(=connection::tests::close_totals_count_a_batch_flushed_by_the_drain_after_cancellation) + test(=connection::tests::close_totals_skip_a_frame_the_socket_rejects) + test(=connection::tests::close_totals_skip_frames_stranded_by_a_failed_flush) + test(=connection::tests::read_before_login_logs_one_denial_from_the_handler) + test(=connection::tests::read_refused_by_a_full_handler_semaphore_logs_one_denial) + test(=connection::tests::saturated_handler_write_line_records_whether_its_ok_was_queued) + test(=connection::tests::read_refused_by_unavailable_admission_logs_one_denial) + test(=handlers::auth::tests::repeat_auth_after_a_terminal_logs_one_denial) + test(=nip_fi_upgrade::tests::deny_protected_logs_one_denied_auth_line) + test(=api::bridge::moderation_refusal_tests::moderation_lookup_failure_is_unavailable) + test(/^push_runtime::/) + test(/^operator_listener::tests::/) + test(/^handlers::channel_authz::/) + test(/^handlers::moderation_authz::/) + test(/^handlers::side_effects::tests::/) + test(/^handlers::coalesced_refresh::tests::/) + test(/^handlers::system_channels::tests::/) + test(/^nip11::tests::/) + test(/^storage_sweep::tests::/) + test(/^nip_fi_core::tests::/) + test(/^nip_fi_http::tests::/) + test(/^nip_fi_policy::tests::/) + test(/^nip_fi_config::tests::/) + test(/^nip_fi_resolver::tests::/) + test(/^readiness::tests::/) + test(/^router::tests::/) + test(/^api::parse_query_tests::/) + test(/^api::db_read_error_tests::/) + test(/^api::profiles::/) + test(/^api::bridge::search_slots::tests::/) + test(/^api::git::transport::off_mode_precedence_tests::/) + test(/^api::git::store::tests::/) + test(/^api::git::store::fault_probe::/) + test(/^api::git::cas_publish::tests::/) + test(/^api::git::transport::track_c_tests::/) + test(/^audio::join::tests::/) + test(/^audio::handler::tests::/) + test(/^nip_fi_gate::tests::/) + test(/^nip_fi_session::tests::/) + test(/^nip_fi_shadow::tests::/) + test(/^nip_fi_shadow_session::tests::/) + test(/^startup_steps::tests::/) + test(/^mesh_boot::tests::/) + test(/^telemetry::tests::/) + test(/^config::tests::/) + test(=state::tests::accessible_channel_invalidation_is_scoped_to_community) + test(=state::tests::accessible_channels_join_member_and_open_halves) + test(=state::tests::channel_deleted_invalidation_is_scoped_to_community) + test(=state::tests::neither_a_confirmed_inactive_community_nor_a_failed_lookup_admits_the_socket) + test(=state::tests::periodic_revalidation_disconnects_inside_the_fenced_callback) + test(=state::tests::bare_community_disconnect_fails_closed_when_the_fence_is_unavailable) + test(=connection::tests::send_loop_sends_policy_close_when_community_is_archived) + test(=state::tests::community_disconnect_then_nip_fi_keeps_community_deleted_reason) + test(=state::tests::disconnect_community_wins_reason_losing_nip_fi_does_not_enqueue_frame) + test(=handlers::req::tests::timed_out_historical_read_deregisters_before_closed) + test(=handlers::req::tests::superseded_timeout_leaves_replacement_intact) + test(=handlers::req::tests::search_claim_retires_live_and_yields_to_replacement) + test(=handlers::req::tests::failed_search_closes_without_eose_or_trying_later_filters) + test(=handlers::req::tests::concurrent_claims_and_stale_teardowns_keep_the_last_owner) + test(=handlers::req::tests::timeout_closed_is_emitted_before_a_replacement_can_claim) + test(=handlers::req::tests::revoke_then_replacement_keeps_replacement_whole) + test(=handlers::req::tests::revoke_of_a_replaced_holder_spares_the_pending_replacement) + test(=handlers::req::tests::superseded_or_closed_requests_cannot_claim) + test(=connection::tests::close_fences_a_req_whose_handler_has_not_run) + test(=connection::tests::only_the_newest_same_id_req_answers) + test(=handlers::req::tests::claims_after_connection_cleanup_are_refused) + test(=handlers::req::tests::dropped_terminal_frame_cancels_connection) + test(=handlers::req::tests::revoke_dropped_terminal_frame_cancels_connection) + test(=handlers::req::tests::count_fallback_covers_filters_that_can_match_private_deletions) + test(=handlers::req::tests::count_fallback_fetches_one_extra_candidate) + test(=handlers::req::tests::group_state_t_and_creator_tags_reach_sql_only_for_group_state_kinds) + test(=handlers::req::tests::empty_filter_sets_match_nothing_in_sql) + test(=api::bridge::postgres_tests::bridge_search_mode_extension_accepts_prefix_snake_or_camel_case) + test(=api::bridge::postgres_tests::bridge_search_sort_extension_selects_newest_only_when_named) + test(=api::invites::postgres_tests::restriction_tests::postgres_tests::destructive_fixture_rejects_shared_database_urls) + (kind(bin) & (test(/^tests::/) + test(/^composition_tests::/) + test(/^env_filter_tests::/)) - test(/^tests::postgres_tests::/))'
         # Note on audio::join::tests scope: the full suite is infra-free (no DB,
         # no Redis). The infra-free audio/FI regression witnesses — bootstrap
         # ordering barrier, CommitConfirmed arm, pending-close invisibility,
diff --git a/crates/buzz-relay/src/api/git/cas_publish.rs b/crates/buzz-relay/src/api/git/cas_publish.rs
index 50bb36d818..438c16a4f7 100644
--- a/crates/buzz-relay/src/api/git/cas_publish.rs
+++ b/crates/buzz-relay/src/api/git/cas_publish.rs
@@ -1,30 +1,34 @@
-//! Push commit point — content-addressed pack + manifest CAS (§Push step 2–7).
+//! Push commit point — content-addressed pack + manifest CAS (§Push steps 3–7
+//! of `docs/git-on-object-storage.md`).
 //!
-//! Pure async function over the spec's commit primitives. Given the post-
-//! receive-pack repository workspace and the object-store client, this:
+//! This module holds the two halves of what happens after `git receive-pack`
+//! returns.
 //!
-//! 1. Reads the current pointer → `(e, d_before)` (§Push step 3).
-//! 2. Fetches `m_before` via `get_verified(d_before)` (§Push step 3) —
-//!    digest-verified so a corrupt manifest fails closed, not silently.
-//! 3. Snapshots refs + HEAD off the workspace (the receive-pack's published
-//!    state, by which point the pre-receive hook has enforced fast-forward /
-//!    branch-protection against the parent's refs).
-//! 4. Normally captures the new objects as a delta pack via `git pack-objects
+//! **Deciding (§Push step 3).** [`snapshot_workspace`] reads the refs and HEAD
+//! that receive-pack left in the workspace, and [`push_disposition`] compares
+//! them with the refs the workspace was hydrated from. Only a push that
+//! changed refs is published.
+//!
+//! **Publishing (§Push steps 4–7).** [`cas_publish`] takes that snapshot and
+//! the [`ParentState`] the workspace was hydrated from. It never re-reads the
+//! pointer before the conditional write. It:
+//!
+//! 1. Normally captures the new objects as a delta pack via `git pack-objects
 //!    --revs --stdout` over `(refs_after) --not (refs_before-tips)` (§Push
-//!    step 1–2). Before the manifest reaches its pack cap, compaction instead
+//!    step 4). Before the manifest reaches its pack cap, compaction instead
 //!    captures the complete `refs_after` closure into bounded replacement
 //!    packs. Empty output for a ref-less repository is allowed.
-//! 5. `put_pack` (content-addressed, create-only, idempotent — §Push step 2).
+//! 2. `put_pack` (content-addressed, create-only, idempotent — §Push step 5).
 //!    The key is derived from `sha256(bytes)` by the store layer.
-//! 6. Composes `m_after`: normal pushes use parent packs ∪ new pack;
+//! 3. Composes `m_after`: normal pushes use parent packs ∪ new pack;
 //!    compaction replaces the pack list with the newly captured full closure.
-//!    Both retain the parent digest and post-push refs (§Push step 5).
-//! 7. `put_manifest` (content-addressed, create-only, idempotent — §Push
-//!    step 6).
-//! 8. `put_pointer(IfMatch(e) | IfNoneMatchStar)` — the CAS (§Push step 7).
+//!    Both retain the parent digest and post-push refs. `put_manifest`
+//!    (content-addressed, create-only, idempotent — §Push step 6).
+//! 4. `put_pointer(IfMatch(e) | IfNoneMatchStar)` — the CAS (§Push step 7),
+//!    with `e` taken from the `ParentState`.
 //!    - `Won` → return `CasSuccess { manifest, manifest_key }`. The caller
-//!      then derives kind:30618 against `m_after` (Sami's
-//!      `manifest_event::build_ref_state_event`) and constructs the
+//!      then derives kind:30618 against `m_after`
+//!      (`manifest_event::build_ref_state_event`) and constructs the
 //!      success response — the *fence* in §Push step 8.
 //!    - `LostRace` → re-read the pointer to fetch the winner's manifest,
 //!      then return `CasError::Conflict { winner_manifest,
@@ -32,11 +36,11 @@
 //!      the caller's diagnostic + future cache; the loser's ephemeral
 //!      tempdir dies on scope exit, so there's no disk to reconcile.
 //!      **No retry.** The losing push's receive-pack output was derived
-//!      against the now-superseded parent; reusing it would violate
-//!      `Inv_RefDerivedFromParent` (§Mechanized Verification). The client
-//!      re-runs `git push`, which re-hydrates and re-runs receive-pack
-//!      against the advanced state — that is the only safe retry, and
-//!      `git`'s own machinery already does it.
+//!      against the now-superseded parent, so nothing computed from it may
+//!      be published (the model's seeded error `stale-base` is that
+//!      mistake; see §Mechanized Verification). The client re-runs
+//!      `git push`, which re-hydrates and re-runs receive-pack against the
+//!      advanced state.
 //!
 //! ## Fence positioning
 //!
@@ -47,11 +51,9 @@
 //!
 //! ## What this function deliberately does *not* do
 //!
-//! - **No retry on `LostRace`.** Per spec §Push step 7 "GOTO 3 (retry) or
-//!   respond non-ff": both arms are safe; we take the non-ff arm because
-//!   reusing receive-pack's output against a moved parent isn't safe and
-//!   re-hydrating from inside the handler is expensive. Sami's TLA-action
-//!   guidance is explicit: retry would change the TLA action.
+//! - **No retry on `LostRace`.** See above: re-using receive-pack's output
+//!   against a moved parent is unsafe, and re-hydrating from inside the
+//!   handler is expensive.
 //! - **No kind:30618 emission.** That is the *derived* publication after a
 //!   successful CAS. Caller passes `m_after` into
 //!   `manifest_event::build_ref_state_event` *after* this returns `Ok`.
@@ -59,7 +61,7 @@
 //!   CAS, never the commit."
 //! - **No advisory lock.** Spec §Push, "No advisory lock in v1": writer
 //!   serialization is the CAS. Adding a per-repo mutex would hide the
-//!   exact contention `Inv_NoFork` proves safe.
+//!   exact contention the refinement check (`Inv_NoFork`) covers.
 
 use std::collections::{BTreeMap, BTreeSet};
 use std::path::{Path, PathBuf};
@@ -72,8 +74,8 @@ use tokio::process::Command;
 use tracing::{debug, warn};
 
 use crate::api::git::manifest::{
-    pointer_key, Manifest, ManifestError, MANIFEST_VERSION, MAX_MANIFEST_PACKS, MAX_MANIFEST_REFS,
-    PACK_COMPACTION_THRESHOLD,
+    next_published_at, pointer_key, Manifest, ManifestError, MANIFEST_VERSION, MAX_MANIFEST_PACKS,
+    MAX_MANIFEST_REFS, PACK_COMPACTION_THRESHOLD,
 };
 use crate::api::git::store::{CasOutcome, ETag, GitStore, Precond, StoreError};
 use buzz_core::TenantContext;
@@ -196,7 +198,7 @@ pub struct CasSuccess {
     pub manifest_key: String,
 }
 
-/// Resolved view of the pre-push pointer (§Push step 3 output).
+/// Resolved view of the pre-push pointer (§Push step 1 output).
 ///
 /// **The CAS write is predicated on `if_match`** — the caller must load
 /// this *before* running receive-pack against the hydrated workspace, and
@@ -239,6 +241,7 @@ impl ParentState {
                 refs: BTreeMap::new(),
                 packs: Vec::new(),
                 parent: None,
+                published_at: None,
             },
         }
     }
@@ -260,16 +263,112 @@ impl ParentState {
     }
 }
 
-/// Read `refs/*` + symbolic-HEAD from the workspace.
+/// Ref state of a workspace: every ref and the symbolic HEAD.
 ///
-/// HEAD is the symref target (e.g. `refs/heads/main`), unprefixed — the
-/// manifest stores published ref state, not protocol formatting. Detached
-/// HEAD or no HEAD yields an empty string.
-async fn snapshot_workspace_state(
-    repo_path: &Path,
-    scratch_dir: &Path,
-) -> Result<(BTreeMap<String, String>, String), CasError> {
+/// This is the relay's only evidence of what `git receive-pack` did. Both the
+/// decision whether to publish ([`push_disposition`]) and the published
+/// manifest ([`cas_publish`]) are computed from one value of this type, so
+/// they cannot disagree about what the push changed.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct WorkspaceState {
+    /// Every ref in the workspace, mapped to the object id it names.
+    pub refs: BTreeMap<String, String>,
+    /// The symbolic-ref target of `HEAD` (for example `refs/heads/main`), or
+    /// an empty string when `HEAD` is detached or missing.
+    pub head: String,
+}
+
+/// What a finished `git receive-pack` run obliges the relay to do.
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum PushDisposition {
+    /// The workspace refs equal the refs it was hydrated from. There is
+    /// nothing to publish; the client is answered with git's own output.
+    RelayOnly,
+    /// The workspace refs changed and git exited normally. The change must
+    /// be published before the client is told anything.
+    Publish,
+    /// The workspace refs changed but git exited abnormally. Its report to
+    /// the client may be incomplete, so nothing is published and the request
+    /// fails.
+    Abort,
+}
+
+/// Decide what to do with a finished push from the refs it left behind.
+///
+/// The decision compares the workspace refs with the refs the workspace was
+/// hydrated from. It does not read git's report-status stream, for two
+/// reasons. A client chooses whether that stream exists, and git exits zero
+/// both for a request that carries no commands and for one a hook declined, so
+/// the stream cannot show that a push was authorized. And a push that updates
+/// one ref and is refused another reports both outcomes, so an `ng` line does
+/// not show that nothing changed.
+///
+/// The decision is sound under one assumption about git: `receive-pack`
+/// changes a ref only by applying a command the client submitted, and only
+/// after the pre-receive hook accepted the whole command list. Then changed
+/// refs imply an accepted push. Unchanged refs imply that any `ok` git
+/// reported belongs to a command that asked for the value the ref already
+/// had, which is true of the published state the workspace was hydrated
+/// from, so git's report can be passed on as it is.
+/// `docs/spec/GitOnObjectStore.tla` states this as `Disposition` and checks
+/// it against the legacy rule.
+pub fn push_disposition(
+    exited_ok: bool,
+    parent_refs: &BTreeMap<String, String>,
+    workspace_refs: &BTreeMap<String, String>,
+) -> PushDisposition {
+    if workspace_refs == parent_refs {
+        PushDisposition::RelayOnly
+    } else if exited_ok {
+        PushDisposition::Publish
+    } else {
+        PushDisposition::Abort
+    }
+}
+
+/// Parse `git for-each-ref --format='%(refname) %(objectname)'` output.
+///
+/// Every line must be a ref name, one space, and a 40-hex object id. Anything
+/// else is an error: a line that is skipped would publish a manifest without
+/// that ref, which deletes the ref for every later reader.
+fn parse_ref_snapshot(stdout: &[u8]) -> Result<BTreeMap<String, String>, CasError> {
+    let text = std::str::from_utf8(stdout)
+        .map_err(|e| CasError::PackCapture(format!("for-each-ref output is not UTF-8: {e}")))?;
+    let mut refs = BTreeMap::new();
+    for line in text.lines() {
+        let well_formed = line.split_once(' ').filter(|(name, oid)| {
+            !name.is_empty() && oid.len() == 40 && oid.chars().all(|c| c.is_ascii_hexdigit())
+        });
+        let Some((name, oid)) = well_formed else {
+            return Err(CasError::PackCapture(format!(
+                "for-each-ref returned a malformed line: {line:?}"
+            )));
+        };
+        if refs.len() >= MAX_MANIFEST_REFS && !refs.contains_key(name) {
+            return Err(CasError::ResourceLimit(format!(
+                "workspace contains more than {MAX_MANIFEST_REFS} refs"
+            )));
+        }
+        refs.insert(name.to_string(), oid.to_string());
+    }
+    Ok(refs)
+}
+
+/// Directory for the temporary files of a publication.
+///
+/// Hydrated repositories are direct children of the configured Git scratch
+/// root. Reusing that parent keeps temporary files on the mounted scratch
+/// volume without another path argument.
+fn scratch_dir_of(repo_path: &Path) -> Result<&Path, CasError> {
+    repo_path
+        .parent()
+        .ok_or_else(|| CasError::PackCapture("repository path has no scratch parent".into()))
+}
+
+/// Read every ref and the symbolic HEAD from the workspace at `repo_path`.
+pub async fn snapshot_workspace(repo_path: &Path) -> Result<WorkspaceState, CasError> {
     const MAX_REF_SNAPSHOT_BYTES: u64 = 4 * 1024 * 1024;
+    let scratch_dir = scratch_dir_of(repo_path)?;
 
     let refs_stdout_tmp = tempfile::NamedTempFile::new_in(scratch_dir)
         .map_err(|e| CasError::PackCapture(format!("for-each-ref stdout tempfile: {e}")))?;
@@ -313,26 +412,7 @@ async fn snapshot_workspace_state(
         .await
         .map_err(|e| CasError::PackCapture(format!("for-each-ref stdout read: {e}")))?;
 
-    let mut refs = BTreeMap::new();
-    for line in std::str::from_utf8(&refs_stdout)
-        .unwrap_or_default()
-        .lines()
-    {
-        let mut parts = line.splitn(2, ' ');
-        let (Some(name), Some(oid)) = (parts.next(), parts.next()) else {
-            continue;
-        };
-        if oid.len() != 40 || !oid.chars().all(|c| c.is_ascii_hexdigit()) {
-            warn!(ref_name = %name, oid = %oid, "for-each-ref returned malformed oid; skipping");
-            continue;
-        }
-        if refs.len() >= MAX_MANIFEST_REFS && !refs.contains_key(name) {
-            return Err(CasError::ResourceLimit(format!(
-                "workspace contains more than {MAX_MANIFEST_REFS} refs"
-            )));
-        }
-        refs.insert(name.to_string(), oid.to_string());
-    }
+    let refs = parse_ref_snapshot(&refs_stdout)?;
 
     let mut head_cmd = Command::new("git");
     head_cmd
@@ -349,7 +429,7 @@ async fn snapshot_workspace_state(
         String::new()
     };
 
-    Ok((refs, head))
+    Ok(WorkspaceState { refs, head })
 }
 
 fn resolve_published_head(
@@ -925,6 +1005,7 @@ fn compose_after(
         refs,
         packs,
         parent: parent_digest,
+        published_at: None,
     }
 }
 
@@ -942,6 +1023,7 @@ fn compose_compacted_after(
         refs,
         packs: compacted_pack_keys,
         parent: parent_digest,
+        published_at: None,
     }
 }
 
@@ -977,14 +1059,16 @@ fn record_compaction(
     }
 }
 
-/// The function the §Push step 2–7 protocol distills to.
+/// The function the §Push step 4–7 protocol distills to.
 ///
 /// **Caller contract — `Inv_RefDerivedFromParent` is structural.** The
 /// `parent_state` you pass in must be the same one the workspace was
 /// hydrated from. Concretely: `hydrate::hydrate_for_write(store, ctx, owner,
 /// repo)` returns `(HydratedRepo, ParentState)` from a single pointer
 /// observation → `install_hook(repo.path())` → run `receive-pack`
-/// against the workspace → call this with the **same `parent_state`**.
+/// against the workspace → [`snapshot_workspace`] → call this with the
+/// **same `parent_state`** and that snapshot, and only when
+/// [`push_disposition`] returned [`PushDisposition::Publish`].
 /// The CAS predicate is `parent_state.if_match`, so a concurrent writer
 /// that advanced the pointer between hydrate and CAS reliably surfaces
 /// as `CasError::Conflict { winner_manifest, .. }` (412 → HTTP 409). The
@@ -994,6 +1078,7 @@ fn record_compaction(
 /// at step 7 is the *only* writer serialization (`Inv_NoFork`). No
 /// advisory lock — adding one would hide exactly the interleavings the
 /// model proves safe.
+#[allow(clippy::too_many_arguments)] // the store, the repository identity and the two ref states
 pub async fn cas_publish(
     store: &GitStore,
     ctx: &TenantContext,
@@ -1001,6 +1086,7 @@ pub async fn cas_publish(
     owner: &str,
     repo: &str,
     parent_state: &ParentState,
+    workspace: &WorkspaceState,
     limits: PublishLimits,
 ) -> Result<CasSuccess, CasError> {
     cas_publish_inner(
@@ -1010,6 +1096,7 @@ pub async fn cas_publish(
         owner,
         repo,
         parent_state,
+        workspace,
         PublishOptions {
             limits,
             compaction_threshold: PACK_COMPACTION_THRESHOLD,
@@ -1018,6 +1105,7 @@ pub async fn cas_publish(
     .await
 }
 
+#[allow(clippy::too_many_arguments)] // same parameters as `cas_publish`
 async fn cas_publish_inner(
     store: &GitStore,
     ctx: &TenantContext,
@@ -1025,27 +1113,26 @@ async fn cas_publish_inner(
     owner: &str,
     repo: &str,
     parent_state: &ParentState,
+    workspace: &WorkspaceState,
     options: PublishOptions,
 ) -> Result<CasSuccess, CasError> {
     let limits = options.limits;
     let pkey = pointer_key(ctx.community(), owner, repo);
+    let scratch_dir = scratch_dir_of(repo_path)?;
 
-    // Hydrated repositories are direct children of the configured Git scratch
-    // root. Reuse that parent for publication tempfiles so they remain on the
-    // mounted scratch volume without adding another independent path argument.
-    let scratch_dir = repo_path
-        .parent()
-        .ok_or_else(|| CasError::PackCapture("repository path has no scratch parent".into()))?;
-
-    // Snapshot post-receive-pack state from disk. `parent_state.parent.refs`
+    // `workspace` is the post-receive-pack state. `parent_state.parent.refs`
     // are the refs the workspace was hydrated from — `pack-objects --revs`
     // below uses them as the "negative" set to produce the delta pack.
-    let (refs_after, head_observed) = snapshot_workspace_state(repo_path, scratch_dir).await?;
+    let refs_after = workspace.refs.clone();
 
     // Fresh bare repositories can inherit Git's environment-dependent
     // `master` symref even when the first push creates `main`. Publish a real
     // branch whenever one exists so HEAD never advertises a phantom branch.
-    let head = resolve_published_head(&refs_after, head_observed, &parent_state.parent.head);
+    let head = resolve_published_head(
+        &refs_after,
+        workspace.head.clone(),
+        &parent_state.parent.head,
+    );
 
     let packs_before = parent_state.parent.packs.len();
     let mut compaction_failure = None;
@@ -1168,6 +1255,16 @@ async fn cas_publish_inner(
             new_pack_key,
         )
     };
+    // Stamp the publication time on both the compacted and delta-pack paths.
+    // Strictly after the parent's stamp, so the derived kind:30618 events sort
+    // in manifest-chain order whichever instance and clock emit them.
+    let m_after = Manifest {
+        published_at: Some(next_published_at(
+            &parent_state.parent,
+            nostr::Timestamp::now().as_secs(),
+        )),
+        ..m_after
+    };
 
     // **Pre-CAS validation** (Sami #2 / Max / Dawn): refuse to commit an
     // un-clone-able manifest. `Manifest::validate` checks every refname
@@ -1391,6 +1488,67 @@ mod tests {
         assert!(digest_from_manifest_key("not/manifests/abc").is_err());
     }
 
+    #[test]
+    fn push_disposition_publishes_only_changed_refs_from_a_clean_exit() {
+        let parent: BTreeMap<String, String> =
+            [("refs/heads/main".to_string(), "1".repeat(40))].into();
+        let mut advanced = parent.clone();
+        advanced.insert("refs/heads/main".into(), "2".repeat(40));
+        let mut created = parent.clone();
+        created.insert("refs/heads/feature".into(), "1".repeat(40));
+        let deleted = BTreeMap::new();
+
+        for exited_ok in [true, false] {
+            assert_eq!(
+                push_disposition(exited_ok, &parent, &parent),
+                PushDisposition::RelayOnly,
+                "unchanged refs are never published (exited_ok = {exited_ok})"
+            );
+        }
+        for changed in [&advanced, &created, &deleted] {
+            assert_eq!(
+                push_disposition(true, &parent, changed),
+                PushDisposition::Publish
+            );
+            assert_eq!(
+                push_disposition(false, &parent, changed),
+                PushDisposition::Abort
+            );
+        }
+    }
+
+    #[test]
+    fn ref_snapshot_rejects_every_line_it_cannot_read() {
+        let oid = "a".repeat(40);
+        let good = format!("refs/heads/main {oid}\nrefs/tags/v1 {oid}\n");
+        let refs = parse_ref_snapshot(good.as_bytes()).expect("well-formed snapshot");
+        assert_eq!(refs.len(), 2);
+        assert_eq!(refs.get("refs/heads/main"), Some(&oid));
+        assert!(parse_ref_snapshot(b"").expect("empty snapshot").is_empty());
+
+        // A skipped line would publish a manifest without that ref. Each of
+        // these used to be skipped, and non-UTF-8 output used to read as an
+        // empty repository.
+        let mut not_utf8 = good.clone().into_bytes();
+        not_utf8.extend_from_slice(b"refs/heads/\xff ");
+        not_utf8.extend_from_slice(oid.as_bytes());
+        not_utf8.push(b'\n');
+        let malformed: [Vec<u8>; 5] = [
+            not_utf8,
+            format!("{good}refs/heads/no-oid\n").into_bytes(),
+            format!("{good}refs/heads/short abc123\n").into_bytes(),
+            format!("{good}refs/heads/not-hex {}\n", "z".repeat(40)).into_bytes(),
+            format!("{good} {oid}\n").into_bytes(),
+        ];
+        for input in malformed {
+            assert!(
+                matches!(parse_ref_snapshot(&input), Err(CasError::PackCapture(_))),
+                "accepted {:?}",
+                String::from_utf8_lossy(&input)
+            );
+        }
+    }
+
     #[test]
     fn compose_after_first_push() {
         let parent = ParentState::fresh().parent;
@@ -1700,6 +1858,8 @@ mod tests {
             refs: parent_refs,
             packs: vec![first_pack_key, second_pack_key],
             parent: None,
+            // Stamped by an instance whose clock runs far ahead of this one.
+            published_at: Some(4_000_000_000),
         };
         parent.validate().expect("parent manifest");
         let parent_key = store
@@ -1764,6 +1924,9 @@ mod tests {
             limits,
             compaction_threshold: 2,
         };
+        let workspace = snapshot_workspace(hydrated.path())
+            .await
+            .expect("snapshot pushed workspace");
         let success = cas_publish_inner(
             &store,
             &ctx,
@@ -1771,6 +1934,7 @@ mod tests {
             &owner,
             repo,
             &parent_state,
+            &workspace,
             test_options,
         )
         .await
@@ -1782,6 +1946,11 @@ mod tests {
         );
         assert!(success.manifest.refs.contains_key("refs/tags/v1"));
         assert_eq!(success.manifest.parent, Some(parent_digest));
+        assert_eq!(
+            success.manifest.published_at,
+            Some(4_000_000_001),
+            "the child's kind:30618 must sort after its parent's"
+        );
 
         let conflict = cas_publish_inner(
             &store,
@@ -1790,6 +1959,7 @@ mod tests {
             &owner,
             repo,
             &parent_state,
+            &workspace,
             test_options,
         )
         .await
diff --git a/crates/buzz-relay/src/api/git/hydrate.rs b/crates/buzz-relay/src/api/git/hydrate.rs
index 080bbd5c1c..2c7f712b56 100644
--- a/crates/buzz-relay/src/api/git/hydrate.rs
+++ b/crates/buzz-relay/src/api/git/hydrate.rs
@@ -558,6 +558,7 @@ mod tests {
             refs: BTreeMap::new(),
             packs: Vec::new(),
             parent: None,
+            published_at: None,
         };
         let cache = GitPackCache::new(scratch.path(), u64::MAX, 2).expect("cache");
 
@@ -666,6 +667,7 @@ mod tests {
             refs,
             packs: vec![pack_key.clone()],
             parent: None,
+            published_at: None,
         };
         let manifest_bytes = manifest.canonical_bytes().expect("serialize");
         let manifest_key = st
@@ -814,6 +816,7 @@ mod tests {
             refs: BTreeMap::new(),
             packs: vec![],
             parent: None,
+            published_at: None,
         };
         let manifest_bytes = manifest.canonical_bytes().expect("serialize");
         let manifest_key = st
diff --git a/crates/buzz-relay/src/api/git/manifest.rs b/crates/buzz-relay/src/api/git/manifest.rs
index 0dfbdb35a4..1d2687da4a 100644
--- a/crates/buzz-relay/src/api/git/manifest.rs
+++ b/crates/buzz-relay/src/api/git/manifest.rs
@@ -12,8 +12,9 @@
 //!
 //! - `refs: BTreeMap` — sorted ref names at serialization.
 //! - `packs: Vec<String>` — sorted by `canonical_bytes()` before writing.
-//! - Struct field order: `version`, `head`, `refs`, `packs`, `parent`
-//!   (matches declaration; serde emits in this order).
+//! - Struct field order: `version`, `head`, `refs`, `packs`, `parent`,
+//!   `published_at` (matches declaration; serde emits in this order, and
+//!   omits `published_at` when absent).
 //! - `serde_json::to_vec` — no whitespace.
 //!
 //! Round-trip + byte-stability are pinned in unit tests.
@@ -68,6 +69,29 @@ pub struct Manifest {
     /// reads literally as `parent = pointer.digest`. Writers must strip any
     /// `manifests/` prefix before assigning. Enforced by `validate()`.
     pub parent: Option<String>,
+    /// Unix seconds at which a push published this manifest, strictly greater
+    /// than the parent's. The derived kind:30618 carries it as `created_at`,
+    /// so readers that pick the newest event follow the manifest chain rather
+    /// than the order in which relay instances happened to stamp events.
+    /// `None` for the shared announce-time seed and for manifests written
+    /// before the field existed; omitted from canonical JSON in that case so
+    /// those manifests keep their bytes and digests.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub published_at: Option<u64>,
+}
+
+/// The `published_at` for a manifest superseding `parent`: `now`, advanced
+/// past the parent's own `published_at` when the clock has not moved on (two
+/// pushes in one second) or runs behind the instance that wrote the parent.
+///
+/// An unstamped parent (the announce-time seed, or a manifest written before
+/// the field existed) had its kind:30618 stamped at or before `now`, possibly
+/// in this same second, so the successor takes `now + 1` to sort after it.
+pub fn next_published_at(parent: &Manifest, now: u64) -> u64 {
+    match parent.published_at {
+        Some(previous) => now.max(previous.saturating_add(1)),
+        None => now.saturating_add(1),
+    }
 }
 
 /// Errors from manifest (de)serialization or validation.
@@ -296,6 +320,7 @@ mod tests {
             refs,
             packs: vec![pack_key('c'), pack_key('d')],
             parent: Some("ee".repeat(32)),
+            published_at: None,
         }
     }
 
@@ -371,6 +396,7 @@ mod tests {
             refs: BTreeMap::new(),
             packs: Vec::new(),
             parent: None,
+            published_at: None,
         };
         m.validate().expect("empty manifest is the announce-seed");
         // Canonical bytes must be deterministic + stable so all empty manifests
@@ -567,6 +593,7 @@ mod tests {
             refs,
             packs: vec![pack_key('1')],
             parent: None,
+            published_at: None,
         };
         let bytes = m.canonical_bytes().unwrap();
         let s = std::str::from_utf8(&bytes).unwrap();
@@ -578,4 +605,44 @@ mod tests {
             )
         );
     }
+
+    #[test]
+    fn published_at_serializes_last_and_round_trips() {
+        let mut m = sample();
+        m.parent = None;
+        m.refs.clear();
+        m.packs.clear();
+        m.published_at = Some(1_700_000_000);
+        let bytes = m.canonical_bytes().unwrap();
+        assert_eq!(
+            std::str::from_utf8(&bytes).unwrap(),
+            r#"{"version":1,"head":"refs/heads/main","refs":{},"packs":[],"parent":null,"published_at":1700000000}"#
+        );
+        assert_eq!(Manifest::from_bytes(&bytes).unwrap(), m);
+    }
+
+    #[test]
+    fn manifests_without_published_at_still_parse() {
+        let legacy =
+            br#"{"version":1,"head":"refs/heads/main","refs":{},"packs":[],"parent":null}"#;
+        let m = Manifest::from_bytes(legacy).unwrap();
+        assert_eq!(m.published_at, None);
+        assert_eq!(m.canonical_bytes().unwrap(), legacy.to_vec());
+    }
+
+    #[test]
+    fn next_published_at_strictly_follows_the_parent() {
+        let mut parent = sample();
+        parent.published_at = None;
+        assert_eq!(next_published_at(&parent, 100), 101);
+
+        parent.published_at = Some(90);
+        assert_eq!(next_published_at(&parent, 100), 100);
+        // Same second as the parent.
+        parent.published_at = Some(100);
+        assert_eq!(next_published_at(&parent, 100), 101);
+        // The parent's instance clock ran ahead of ours.
+        parent.published_at = Some(105);
+        assert_eq!(next_published_at(&parent, 100), 106);
+    }
 }
diff --git a/crates/buzz-relay/src/api/git/manifest_event.rs b/crates/buzz-relay/src/api/git/manifest_event.rs
index 698f27e9d1..96ab793179 100644
--- a/crates/buzz-relay/src/api/git/manifest_event.rs
+++ b/crates/buzz-relay/src/api/git/manifest_event.rs
@@ -18,7 +18,7 @@
 
 use std::collections::BTreeMap;
 
-use nostr::{Event, EventBuilder, Keys, Kind, PublicKey, Tag, TagKind};
+use nostr::{Event, EventBuilder, Keys, Kind, PublicKey, Tag, TagKind, Timestamp};
 
 /// Subset of `Manifest` needed to emit a kind:30618 event.
 ///
@@ -39,6 +39,10 @@ pub struct RefStateInputs<'a> {
     /// the pusher's pubkey from the receive-pack hook. On repo-creation, this
     /// is the kind:30617 author (repo owner). Hex-encoded (64 chars).
     pub actor_pubkey_hex: &'a str,
+    /// The manifest's `published_at`, used as the event's `created_at` so
+    /// readers that pick the newest kind:30618 see the newest manifest. `None`
+    /// (a manifest written before the field existed) falls back to now.
+    pub published_at: Option<u64>,
 }
 
 /// Errors from building a kind:30618 ref-state event.
@@ -105,8 +109,11 @@ pub fn build_ref_state_event(
     // p-tag: buzz extension (pusher or owner pubkey).
     tags.push(Tag::public_key(actor));
 
-    let event = EventBuilder::new(Kind::Custom(30618), "")
-        .tags(tags)
+    let mut builder = EventBuilder::new(Kind::Custom(30618), "").tags(tags);
+    if let Some(published_at) = inputs.published_at {
+        builder = builder.custom_created_at(Timestamp::from(published_at));
+    }
+    let event = builder
         .sign_with_keys(relay_keys)
         .map_err(|e| BuildError::Sign(e.to_string()))?;
 
@@ -183,6 +190,7 @@ mod tests {
             head: "refs/heads/main",
             refs: &refs,
             actor_pubkey_hex: &owner,
+            published_at: None,
         };
         let ev = build_ref_state_event(&inputs, &relay_keys()).unwrap();
 
@@ -214,6 +222,7 @@ mod tests {
             head: "refs/heads/dev",
             refs: &refs,
             actor_pubkey_hex: &owner_hex(),
+            published_at: None,
         };
         let ev = build_ref_state_event(&inputs, &relay_keys()).unwrap();
         assert_eq!(first_tag(&ev, "HEAD").unwrap()[1], "ref: refs/heads/dev");
@@ -234,6 +243,7 @@ mod tests {
             head: "refs/heads/main",
             refs: &refs,
             actor_pubkey_hex: &owner_hex(),
+            published_at: None,
         };
         let ev = build_ref_state_event(&inputs, &relay_keys()).unwrap();
 
@@ -277,6 +287,7 @@ mod tests {
             head: "refs/heads/main",
             refs: &refs,
             actor_pubkey_hex: &owner_hex(),
+            published_at: None,
         };
         let ev = build_ref_state_event(&inputs, &relay_keys()).unwrap();
 
@@ -300,6 +311,7 @@ mod tests {
             head: "refs/heads/sha1-branch",
             refs: &refs,
             actor_pubkey_hex: &owner_hex(),
+            published_at: None,
         };
         let ev = build_ref_state_event(&inputs, &relay_keys()).unwrap();
         assert!(first_tag(&ev, "refs/heads/sha1-branch").is_some());
@@ -325,6 +337,7 @@ mod tests {
             head: "refs/heads/ok",
             refs: &refs,
             actor_pubkey_hex: &owner_hex(),
+            published_at: None,
         };
         let ev = build_ref_state_event(&inputs, &relay_keys()).unwrap();
         assert!(first_tag(&ev, "refs/heads/short").is_none());
@@ -358,6 +371,7 @@ mod tests {
             head: "refs/heads/legit",
             refs: &refs,
             actor_pubkey_hex: &owner_hex(),
+            published_at: None,
         };
         let ev = build_ref_state_event(&inputs, &relay_keys()).unwrap();
         assert!(first_tag(&ev, "refs/heads/legit").is_some());
@@ -373,6 +387,7 @@ mod tests {
             head: "refs/heads/main",
             refs: &refs,
             actor_pubkey_hex: "not-a-pubkey",
+            published_at: None,
         };
         let err = build_ref_state_event(&inputs, &relay_keys()).unwrap_err();
         assert!(matches!(err, BuildError::InvalidActor(_)));
@@ -386,10 +401,26 @@ mod tests {
             head: "refs/heads/main",
             refs: &refs,
             actor_pubkey_hex: &owner_hex(),
+            published_at: None,
         };
         let ev = build_ref_state_event(&inputs, &relay_keys()).unwrap();
         assert_eq!(first_tag(&ev, "d").unwrap()[1], "myrepo");
         // Pin: caller responsibility — if they pass "myrepo.git", that's what
         // ends up in the d-tag and won't match the kind:30617 announcement.
     }
+
+    #[test]
+    fn created_at_is_the_manifest_published_at() {
+        let refs = refs_with(&[]);
+        let inputs = RefStateInputs {
+            repo_id: "r",
+            head: "refs/heads/main",
+            refs: &refs,
+            actor_pubkey_hex: &owner_hex(),
+            published_at: Some(1_700_000_000),
+        };
+        let ev = build_ref_state_event(&inputs, &relay_keys()).unwrap();
+        assert_eq!(ev.created_at, Timestamp::from(1_700_000_000));
+        ev.verify().expect("signature covers the custom created_at");
+    }
 }
diff --git a/crates/buzz-relay/src/api/git/settings.rs b/crates/buzz-relay/src/api/git/settings.rs
index 69e6f06514..5fc3a8a2a6 100644
--- a/crates/buzz-relay/src/api/git/settings.rs
+++ b/crates/buzz-relay/src/api/git/settings.rs
@@ -25,7 +25,7 @@ use serde_json::{json, Value};
 use super::{
     binding::{resolve_repo_binding, RepoBinding},
     hydrate::load_pointer,
-    manifest::{is_safe_refname, pointer_key, Manifest},
+    manifest::{is_safe_refname, next_published_at, pointer_key, Manifest},
     manifest_event::{build_ref_state_event, RefStateInputs},
     store::{CasOutcome, ETag, GitStore, Precond},
     transport::{authorize_git_read, deny_banned_git_principal, validate_repo_id},
@@ -130,6 +130,10 @@ impl DefaultBranchSnapshot {
         }
         let changed = self.manifest.head != head;
         if changed {
+            self.manifest.published_at = Some(next_published_at(
+                &self.manifest,
+                nostr::Timestamp::now().as_secs(),
+            ));
             self.manifest.head = head;
             self.manifest.parent = Some(self.digest.clone());
             self.manifest.validate().map_err(backend)?;
@@ -401,10 +405,17 @@ async fn set_default_branch(
         )
     })?;
     serving_write.verify().await.map_err(backend)?;
-    let (snapshot, changed) = serving_write
-        .protect(snapshot.set(&state.git_store, request))
+    // As in `finalize_push`, a pointer CAS that landed stands even if the lease
+    // check after it fails; the lease-guarded kind:30618 insert decides
+    // whether publication may continue.
+    let (set, lease_after_cas) = serving_write
+        .protect_landed(snapshot.set(&state.git_store, request))
         .await
-        .map_err(backend)??;
+        .map_err(backend)?;
+    let (snapshot, changed) = set?;
+    if let Err(error) = lease_after_cas {
+        tracing::warn!(%error, "serving lease check failed after the default-branch CAS landed; continuing publication");
+    }
     let publication = async {
         if changed {
             let actor = auth.caller.to_hex();
@@ -414,6 +425,7 @@ async fn set_default_branch(
                     head: &snapshot.manifest.head,
                     refs: &snapshot.manifest.refs,
                     actor_pubkey_hex: &actor,
+                    published_at: snapshot.manifest.published_at,
                 },
                 &state.relay_keypair,
             )
@@ -435,7 +447,9 @@ async fn set_default_branch(
         Ok::<(), Response>(())
     }
     .await;
-    serving_write.finish().await.map_err(backend)?;
+    if let Err(error) = serving_write.finish().await {
+        tracing::warn!(%error, "failed to release community serving lease after default-branch publication");
+    }
     // Publication failure is not mistaken for a rolled-back manifest.
     if publication.is_err() {
         return Err(error(StatusCode::INTERNAL_SERVER_ERROR, "default branch committed but notification failed; read the current default branch before retrying"));
diff --git a/crates/buzz-relay/src/api/git/settings_tests.rs b/crates/buzz-relay/src/api/git/settings_tests.rs
index fd735520c0..0e6bdbb5fc 100644
--- a/crates/buzz-relay/src/api/git/settings_tests.rs
+++ b/crates/buzz-relay/src/api/git/settings_tests.rs
@@ -1336,6 +1336,9 @@ mod external_infra {
                 &self.owner.public_key().to_hex(),
                 &self.repo,
                 &super::super::super::cas_publish::ParentState::fresh(),
+                &super::super::super::cas_publish::snapshot_workspace(&source)
+                    .await
+                    .unwrap(),
                 limits(0),
             )
             .await
@@ -1800,6 +1803,9 @@ mod external_infra {
             &f.owner.public_key().to_hex(),
             &f.repo,
             &parent,
+            &super::super::super::cas_publish::snapshot_workspace(push.path())
+                .await
+                .unwrap(),
             limits(push.hydrated_bytes()),
         )
         .await;
@@ -1827,6 +1833,9 @@ mod external_infra {
             &f.owner.public_key().to_hex(),
             &f.repo,
             &parent,
+            &super::super::super::cas_publish::snapshot_workspace(push.path())
+                .await
+                .unwrap(),
             limits(push.hydrated_bytes()),
         )
         .await
@@ -1877,6 +1886,9 @@ mod external_infra {
             &f.owner.public_key().to_hex(),
             &f.repo,
             &parent,
+            &super::super::super::cas_publish::snapshot_workspace(push.path())
+                .await
+                .unwrap(),
             limits(push.hydrated_bytes()),
         )
         .await
@@ -1903,6 +1915,9 @@ mod external_infra {
             &f.owner.public_key().to_hex(),
             &f.repo,
             &parent,
+            &super::super::super::cas_publish::snapshot_workspace(push.path())
+                .await
+                .unwrap(),
             limits(push.hydrated_bytes()),
         )
         .await
diff --git a/crates/buzz-relay/src/api/git/transport.rs b/crates/buzz-relay/src/api/git/transport.rs
index 35ae3cab4a..24e8961066 100644
--- a/crates/buzz-relay/src/api/git/transport.rs
+++ b/crates/buzz-relay/src/api/git/transport.rs
@@ -33,7 +33,10 @@ use tower_http::limit::RequestBodyLimitLayer;
 use tracing::{error, info, warn};
 
 use super::binding::{resolve_repo_binding, RepoBinding};
-use super::cas_publish::{cas_publish, CasError, ParentState, PublishLimits};
+use super::cas_publish::{
+    cas_publish, push_disposition, snapshot_workspace, CasError, ParentState, PublishLimits,
+    PushDisposition, WorkspaceState,
+};
 use super::hook::install_hook;
 use super::hydrate::{
     hydrate_for_read, hydrate_for_write, load_manifest_for_read, HydrateError, HydratedRepo,
@@ -1368,9 +1371,10 @@ pub async fn upload_pack(
 /// 4. Run `receive-pack --stateless-rpc` against the tempdir. The hook
 ///    enforces fast-forward + branch protection in-process.
 /// 5. `finalize_push(PushContext { pack, parent_state, repo, ... })` is
-///    the only path that builds a push `Response`. It calls
-///    `cas_publish` (§Push steps 2–7) and emits kind:30618 on `Won`,
-///    *only then* builds the 2xx.
+///    the only path that builds a push `Response`. It compares the
+///    workspace refs with the hydrated ones (§Push step 3); if they
+///    changed it calls `cas_publish` (§Push steps 4–7) and emits
+///    kind:30618 on `Won`, and *only then* builds the 2xx.
 pub async fn receive_pack(
     State(state): State<Arc<AppState>>,
     auth: GitAuth,
@@ -1384,19 +1388,18 @@ pub async fn receive_pack(
     let _permit = acquire_git_permit(&state, "receive_pack")?;
 
     // **No per-repo advisory lock — by design.** Writer serialization is
-    // the pointer CAS at `cas_publish` step 7 (`Inv_NoFork` proves this
-    // sufficient). The previous code held a per-repo `tokio::Mutex`, but
-    // that only spanned one process; once we run >1 relay instance
-    // (which is the point of "no local stateful disk"), it spans nothing
-    // and CAS is the only serialization that holds. The named tradeoff:
-    // two concurrent same-repo pushes each hydrate + run receive-pack,
-    // and the loser's CPU/IO is thrown away on `Conflict`. **Accepted
-    // for v1** — same-ref contention is rare, and a cross-instance lock
-    // would be a distributed-lock service we explicitly don't want.
-    // If contention shows up in metrics, the fix is a short local
-    // best-effort lock as a *latency optimization*, never a correctness
-    // dependency. (Eva's call, on record in #proj-git-on-s3 with the
-    // ParentState seam review.)
+    // the pointer CAS at `cas_publish` step 7 (the `Refines` check in
+    // `docs/spec/GitOnObjectStore.tla` shows this is sufficient). The
+    // previous code held a per-repo `tokio::Mutex`, but that only spanned
+    // one process; once we run >1 relay instance (which is the point of
+    // "no local stateful disk"), it spans nothing and CAS is the only
+    // serialization that holds. The named tradeoff: two concurrent
+    // same-repo pushes each hydrate + run receive-pack, and the loser's
+    // CPU/IO is thrown away on `Conflict`. **Accepted for v1** — same-ref
+    // contention is rare, and a cross-instance lock would be a
+    // distributed-lock service we explicitly don't want. If contention
+    // shows up in metrics, the fix is a short local best-effort lock as a
+    // *latency optimization*, never a correctness dependency.
 
     // Hydrate parent state + workspace in one round-trip. ParentState
     // travels with the workspace into finalize_push so the CAS predicates
@@ -1498,18 +1501,15 @@ fn receive_pack_git_config(hooks_dir: String) -> Vec<(&'static str, String)> {
 /// [`finalize_push`] has decided to build a `Response` from these bytes.
 pub(crate) struct PackOutput {
     pub stdout: Vec<u8>,
-    /// Whether the push is safe to publish: the `git receive-pack` subprocess
-    /// exited 0 **and** its report-status reported no rejected (`ng`) ref.
+    /// Whether the git subprocess exited with status 0.
     ///
-    /// A pre-receive hook decline (authorization denied) does NOT surface as a
-    /// non-zero exit — `git receive-pack --stateless-rpc` exits 0 and reports
-    /// the rejection only in-band as report-status. So `ok` must fold in the
-    /// report-status scan (`receive_pack_report_rejected`), not the exit code
-    /// alone. `finalize_push` treats `false` as "push did not happen": skip the
-    /// CAS publish and the derived kind:30618 so a rejected push leaves **no
-    /// published state**. The buffered stdout still carries git's in-band
-    /// report-status so the client prints the rejection.
-    pub ok: bool,
+    /// For `receive-pack` this says nothing about whether the push was
+    /// accepted: git exits 0 when a pre-receive hook declines the push, when
+    /// some ref updates are refused, and when the request carries no commands
+    /// at all. [`finalize_push`] therefore decides from the refs the workspace
+    /// holds afterwards (`push_disposition`), and uses this flag only to
+    /// refuse to publish the result of a run that failed part-way.
+    pub exited_ok: bool,
 }
 
 /// Spawn a `git --stateless-rpc <service>` subprocess against the given
@@ -1637,34 +1637,16 @@ async fn run_git_at(
         warn!(service = %service, ?status, "git subprocess exited with error");
         tracing::debug!(stderr = %stderr, service = %service, "git subprocess stderr");
         // Still return output — git protocol errors are communicated in-band.
-        // A non-zero exit feeds `PackOutput.ok` below, but it is NOT the signal
-        // for a pre-receive hook decline: `git receive-pack --stateless-rpc`
-        // exits 0 on a hook decline, reporting the rejection only in-band as
-        // report-status (see `receive_pack_report_rejected`). The exit code
-        // still guards genuine subprocess failures (spawn/IO/abort).
     }
 
-    // Primary fence for a denied push: scan the report-status for an `ng`
-    // (rejected) ref update. `git receive-pack` exits 0 on a pre-receive hook
-    // decline, so the exit code alone is insufficient — the rejection lives in
-    // the in-band report-status. Fold both signals into `ok` so `finalize_push`
-    // skips CAS publish + kind:30618 on any rejected ref.
     let stdout = tokio::fs::read(stdout_tmp.path()).await.map_err(|e| {
         error!(error = %e, service = %service, "git stdout read failed");
         (StatusCode::INTERNAL_SERVER_ERROR, "git error").into_response()
     })?;
 
-    let report_rejected = service == "receive-pack" && receive_pack_report_rejected(&stdout);
-    if report_rejected {
-        warn!(
-            service = %service,
-            "git receive-pack report-status contains a rejected (ng) ref update"
-        );
-    }
-
     Ok(PackOutput {
         stdout,
-        ok: status.success() && !report_rejected,
+        exited_ok: status.success(),
     })
 }
 
@@ -1682,97 +1664,6 @@ async fn read_log_prefix(path: &Path, max_bytes: u64) -> String {
     String::from_utf8_lossy(&bytes).to_string()
 }
 
-/// Returns true when a `git receive-pack` report-status stream contains an
-/// `ng <ref> <reason>` line — i.e. git rejected at least one ref update.
-///
-/// Empirically, `git receive-pack --stateless-rpc` exits **0** even when a
-/// pre-receive hook rejects a push: the rejection is communicated only in-band
-/// to the client as report-status (`unpack ok` followed by `ng refs/...
-/// pre-receive hook declined`). The relay must therefore treat an `ng` status
-/// as "push did not happen" for the publish fence, not rely on the exit code.
-///
-/// ## Wire format
-///
-/// The report-status is a pkt-line stream. When side-band-64k is negotiated
-/// (which the stock client does), the status pkt-lines are **nested**: each
-/// outer pkt-line's payload begins with a channel byte (`1` = data, `2`/`3` =
-/// progress/error text), and the band-1 payload carries its *own* inner
-/// pkt-line stream:
-///
-/// ```text
-/// <outer-len>\x01<inner-len>unpack ok\n<inner-len>ng refs/heads/main ...\n0000
-/// ```
-///
-/// A naive "strip the band byte then split on \n" misses this: the rejection
-/// line surfaces as `0031ng refs/...` (inner length prefix glued on), which
-/// does not start with `ng `. So we de-frame one level deeper — for a band-1
-/// payload we parse the inner pkt-lines before matching. Without side-band the
-/// status pkt-lines appear directly at the outer level, which we also match.
-fn receive_pack_report_rejected(stdout: &[u8]) -> bool {
-    for payload in PktLineIter::new(stdout) {
-        match payload.first() {
-            // Side-band channel 1 (data): carries a nested pkt-line stream.
-            Some(1) => {
-                if PktLineIter::new(&payload[1..]).any(|line| line.starts_with(b"ng ")) {
-                    return true;
-                }
-            }
-            // Side-band channel 2/3 (progress/error text): never status lines.
-            Some(2 | 3) => {}
-            // No side-band: the status pkt-line payload is the line itself.
-            _ => {
-                if payload.starts_with(b"ng ") {
-                    return true;
-                }
-            }
-        }
-    }
-    false
-}
-
-/// Iterator over the payloads of a pkt-line stream.
-///
-/// Yields the bytes between the 4-hex length prefix and the end of each
-/// pkt-line. Skips flush (`0000`) / delim (`0001`) / response-end (`0002`)
-/// control pkts. Stops on the first malformed length or truncated frame
-/// (defensive: a corrupt stream simply produces no further matches rather
-/// than panicking).
-struct PktLineIter<'a> {
-    buf: &'a [u8],
-    i: usize,
-}
-
-impl<'a> PktLineIter<'a> {
-    fn new(buf: &'a [u8]) -> Self {
-        Self { buf, i: 0 }
-    }
-}
-
-impl<'a> Iterator for PktLineIter<'a> {
-    type Item = &'a [u8];
-
-    fn next(&mut self) -> Option<&'a [u8]> {
-        loop {
-            if self.i + 4 > self.buf.len() {
-                return None;
-            }
-            let len_hex = std::str::from_utf8(&self.buf[self.i..self.i + 4]).ok()?;
-            let len = usize::from_str_radix(len_hex, 16).ok()?;
-            // 0000 (flush), 0001 (delim), 0002 (response-end): no payload.
-            if len < 4 {
-                self.i += 4;
-                continue;
-            }
-            if self.i + len > self.buf.len() {
-                return None;
-            }
-            let payload = &self.buf[self.i + 4..self.i + len];
-            self.i += len;
-            return Some(payload);
-        }
-    }
-}
-
 /// Keeps the git subprocess and its hydrated workspace alive for exactly as
 /// long as the response body is being streamed.
 ///
@@ -2072,6 +1963,10 @@ struct FinalizePushHooks {
     post_cas_gate: Option<Arc<PostCasGate>>,
     #[cfg(test)]
     fail_ref_state_insert: bool,
+    /// Fire the lease-loss signal as the pointer CAS completes, as a failed
+    /// heartbeat renewal would, while the durable lease stays valid.
+    #[cfg(test)]
+    lose_lease_signal_after_cas: bool,
 }
 
 #[cfg(test)]
@@ -2094,6 +1989,19 @@ async fn finalize_push(state: &Arc<AppState>, ctx: PushContext) -> Response {
     finalize_push_inner(state, ctx, &FinalizePushHooks::default()).await
 }
 
+/// Read what a finished `receive-pack` run left in the workspace and decide
+/// what the relay owes the client: git's answer alone, a publication, or a
+/// failure. The returned snapshot is the one a publication must use.
+async fn observe_push(
+    pack: &PackOutput,
+    parent_state: &ParentState,
+    repo_path: &Path,
+) -> Result<(PushDisposition, WorkspaceState), CasError> {
+    let workspace = snapshot_workspace(repo_path).await?;
+    let disposition = push_disposition(pack.exited_ok, &parent_state.parent.refs, &workspace.refs);
+    Ok((disposition, workspace))
+}
+
 async fn finalize_push_inner(
     state: &Arc<AppState>,
     ctx: PushContext,
@@ -2102,34 +2010,72 @@ async fn finalize_push_inner(
     #[cfg(not(test))]
     let _ = hooks;
 
-    // The push fence, part 0 — **a rejected push publishes nothing.**
+    // The push fence, part 0 — **publish exactly what the push changed.**
     //
-    // `ctx.pack.ok` is false when git aborted the ref updates: either the
-    // subprocess exited non-zero (genuine failure) OR — the important case —
-    // a pre-receive hook declined the push. A hook decline does NOT yield a
-    // non-zero exit; `git receive-pack --stateless-rpc` exits 0 and reports
-    // the rejection only in-band as report-status (`ng <ref> <reason>`), which
-    // `run_git_at` folds into `ok` via `receive_pack_report_rejected`. In
-    // either case the workspace refs were NOT advanced, so there is no
-    // committed state to publish: skip the CAS pointer write AND the derived
-    // kind:30618. Otherwise a denied push would emit a relay-signed, fanned-out
-    // 30618 falsely attributing the ref state to the *denied* pusher
-    // (`actor = ctx.pusher`), breaking the invariant "rejected push → no
-    // published state".
+    // The workspace refs are the only evidence of what receive-pack did, so
+    // the decision is taken from them (`push_disposition`), not from git's
+    // exit status or its report to the client:
     //
-    // git's in-band report-status (already buffered in `ctx.pack.stdout`)
-    // still streams back so the client prints `! [remote rejected]` / the
-    // hook's decline message; only the publish side effects are suppressed.
-    if !ctx.pack.ok {
-        warn!(
-            owner = %ctx.owner,
-            repo = %ctx.repo_id,
-            "receive-pack exited non-zero (e.g. pre-receive hook decline); \
-             skipping CAS publish and kind:30618 — no state published"
-        );
-        let response = build_git_response("receive-pack", ctx.pack);
-        drop(ctx.repo_handle);
-        return response;
+    // - Refs unchanged: nothing was accepted. This covers a hook decline, a
+    //   request with no commands, and a push whose every command was refused.
+    //   Publishing here would move the pointer and emit a relay-signed
+    //   kind:30618 naming a pusher the policy never approved.
+    // - Refs changed, git exited 0: at least one command was applied, and git
+    //   reports `ok` for it even if it reports `ng` for others. Those refs must
+    //   be published before the client sees that report.
+    // - Refs changed, git exited non-zero: the run failed part-way and its
+    //   report may be incomplete. Nothing is published and the request fails.
+    let (disposition, workspace) =
+        match observe_push(&ctx.pack, &ctx.parent_state, ctx.repo_handle.path()).await {
+            Ok(observed) => observed,
+            Err(CasError::ResourceLimit(e)) => {
+                warn!(
+                    owner = %ctx.owner,
+                    repo = %ctx.repo_id,
+                    error = %e,
+                    "push rejected: repo exceeds relay resource limits"
+                );
+                return (
+                    StatusCode::PAYLOAD_TOO_LARGE,
+                    "repository exceeds relay resource limits",
+                )
+                    .into_response();
+            }
+            Err(error) => {
+                error!(
+                    owner = %ctx.owner,
+                    repo = %ctx.repo_id,
+                    %error,
+                    "could not read workspace refs after receive-pack; nothing published"
+                );
+                return (StatusCode::INTERNAL_SERVER_ERROR, "git backend error").into_response();
+            }
+        };
+    match disposition {
+        PushDisposition::Publish => {}
+        PushDisposition::RelayOnly => {
+            info!(
+                owner = %ctx.owner,
+                repo = %ctx.repo_id,
+                exited_ok = ctx.pack.exited_ok,
+                "receive-pack changed no ref; nothing published"
+            );
+            let response = build_git_response("receive-pack", ctx.pack);
+            drop(ctx.repo_handle);
+            return response;
+        }
+        PushDisposition::Abort => {
+            error!(
+                owner = %ctx.owner,
+                repo = %ctx.repo_id,
+                "receive-pack exited non-zero after changing refs; nothing published"
+            );
+            return (
+                StatusCode::INTERNAL_SERVER_ERROR,
+                "git receive-pack failed; nothing was published",
+            )
+                .into_response();
+        }
     }
 
     // An already-running receive-pack may cross the durable fence after
@@ -2173,76 +2119,31 @@ async fn finalize_push_inner(
         &ctx.owner,
         &ctx.repo,
         &ctx.parent_state,
+        &workspace,
         PublishLimits {
             parent_hydrated_bytes: ctx.repo_handle.hydrated_bytes(),
             max_pack_bytes: state.config.git_max_pack_bytes,
             max_repo_bytes: state.config.git_max_repo_bytes,
         },
     );
-    let success = match serving_write.protect(publish).await {
-        Ok(result) => match result {
-            Ok(s) => s,
-            Err(CasError::Conflict {
-                winner_manifest_key,
-                ..
-            }) => {
-                warn!(
-                    owner = %ctx.owner,
-                    repo = %ctx.repo,
-                    winner = %winner_manifest_key,
-                    "push lost CAS race; tempdir dropped, returning 409"
-                );
-                return (
-                    StatusCode::CONFLICT,
-                    "push superseded by a concurrent writer; pull and retry",
-                )
-                    .into_response();
-            }
-            Err(CasError::ManifestInvalid(e)) => {
-                // 4xx-class: the workspace produced refs/HEAD/oids the
-                // manifest validator rejects (unsafe refname, malformed oid,
-                // empty head, malformed parent). Pre-CAS — no pointer was
-                // written.
-                warn!(
-                    owner = %ctx.owner,
-                    repo = %ctx.repo,
-                    error = %e,
-                    "push rejected: manifest validation failed"
-                );
-                return (
-                    StatusCode::BAD_REQUEST,
-                    "push produced invalid manifest state",
-                )
-                    .into_response();
-            }
-            Err(CasError::ResourceLimit(e)) => {
-                warn!(
-                    owner = %ctx.owner,
-                    repo = %ctx.repo,
-                    error = %e,
-                    "push rejected: repo exceeds relay resource limits"
-                );
-                return (
-                    StatusCode::PAYLOAD_TOO_LARGE,
-                    "repository exceeds relay resource limits",
-                )
-                    .into_response();
-            }
-            Err(e) => {
-                // 5xx-class: ManifestReadFailed (parent corruption),
-                // Backend, PackCapture. The tempdir drops on scope exit; no
-                // pointer was written (or, on rare ManifestReadFailed during
-                // winner-fetch, the winner is already installed and the
-                // loser's data is unrelated).
-                error!(
-                    owner = %ctx.owner,
-                    repo = %ctx.repo,
-                    error = %e,
-                    "push failed pre-response"
-                );
-                return (StatusCode::INTERNAL_SERVER_ERROR, "git backend error").into_response();
-            }
-        },
+    #[cfg(test)]
+    let lost_after_cas = hooks
+        .lose_lease_signal_after_cas
+        .then(|| serving_write.lost());
+    #[cfg(test)]
+    let publish = async move {
+        let result = publish.await;
+        if let Some(lost) = lost_after_cas {
+            lost.cancel();
+        }
+        result
+    };
+    // `protect_landed`, not `protect`: once `cas_publish` returns, its outcome
+    // stands even if the lease check that follows fails. A landed pointer CAS
+    // cannot be undone, so reporting it as a failure would tell the client
+    // the push did not land when it did, and would skip its kind:30618.
+    let (result, lease_after_cas) = match serving_write.protect_landed(publish).await {
+        Ok(landed) => landed,
         Err(error) => {
             warn!(owner = %ctx.owner, repo = %ctx.repo, %error, "push lost community serving lease during CAS publish");
             return (
@@ -2252,6 +2153,82 @@ async fn finalize_push_inner(
                 .into_response();
         }
     };
+    let success = match result {
+        Ok(s) => s,
+        Err(CasError::Conflict {
+            winner_manifest_key,
+            ..
+        }) => {
+            warn!(
+                owner = %ctx.owner,
+                repo = %ctx.repo,
+                winner = %winner_manifest_key,
+                "push lost CAS race; tempdir dropped, returning 409"
+            );
+            return (
+                StatusCode::CONFLICT,
+                "push superseded by a concurrent writer; pull and retry",
+            )
+                .into_response();
+        }
+        Err(CasError::ManifestInvalid(e)) => {
+            // 4xx-class: the workspace produced refs/HEAD/oids the
+            // manifest validator rejects (unsafe refname, malformed oid,
+            // empty head, malformed parent). Pre-CAS — no pointer was
+            // written.
+            warn!(
+                owner = %ctx.owner,
+                repo = %ctx.repo,
+                error = %e,
+                "push rejected: manifest validation failed"
+            );
+            return (
+                StatusCode::BAD_REQUEST,
+                "push produced invalid manifest state",
+            )
+                .into_response();
+        }
+        Err(CasError::ResourceLimit(e)) => {
+            warn!(
+                owner = %ctx.owner,
+                repo = %ctx.repo,
+                error = %e,
+                "push rejected: repo exceeds relay resource limits"
+            );
+            return (
+                StatusCode::PAYLOAD_TOO_LARGE,
+                "repository exceeds relay resource limits",
+            )
+                .into_response();
+        }
+        Err(e) => {
+            // 5xx-class: ManifestReadFailed (parent corruption),
+            // Backend, PackCapture. The tempdir drops on scope exit; no
+            // pointer was written (or, on rare ManifestReadFailed during
+            // winner-fetch, the winner is already installed and the
+            // loser's data is unrelated).
+            error!(
+                owner = %ctx.owner,
+                repo = %ctx.repo,
+                error = %e,
+                "push failed pre-response"
+            );
+            return (StatusCode::INTERNAL_SERVER_ERROR, "git backend error").into_response();
+        }
+    };
+    // The pointer is committed. A lapsed lease no longer decides the response:
+    // the kind:30618 insert below is admitted against the durable lease, so it
+    // fails if deletion has fenced the community, and succeeds if only the
+    // local heartbeat signal fired.
+    if let Err(error) = lease_after_cas {
+        warn!(
+            owner = %ctx.owner,
+            repo = %ctx.repo,
+            manifest = %success.manifest_key,
+            %error,
+            "serving lease check failed after the pointer CAS landed; continuing publication"
+        );
+    }
 
     #[cfg(test)]
     if let Some(gate) = &hooks.post_cas_gate {
@@ -2260,34 +2237,16 @@ async fn finalize_push_inner(
     }
 
     // Derived after CAS: kind:30618 ref-state event over the *committed*
-    // manifest's refs/head. Spec §Implementation Correspondence:
-    // "kind:30618 is derived after CAS, never the commit." We emit only
-    // when the committed manifest differs from the parent — a true no-op
-    // push pays no 30618 cost.
-    //
-    // **Strict no-op detection.** We emit unless the canonical manifest
-    // is byte-identical to the parent (Dawn's `canonical_bytes` is
-    // deterministic, so equal published state ⇒ equal digest by
-    // construction). The cases this differs from "refs+head equality":
-    // pack-only changes (rare; internal recompaction, or a push that
-    // produces a new pack covering existing tips with different deltas)
-    // would emit a 30618 with identical `(refs, head)`. The relay DB's
-    // `Ok((_, false))` arm below dedups it for free — one extra DB
-    // round-trip per pack-only push, which clients don't normally
-    // generate. Tightening to refs+head equality is a future
-    // micro-optimization only if that dedup cost becomes visible.
-    let parent_digest_str: Option<&str> = ctx.parent_state.parent_digest.as_deref();
-    let after_digest = success.manifest_key.strip_prefix("manifests/");
-    let manifest_changed = match (parent_digest_str, after_digest) {
-        (Some(before), Some(after)) => before != after,
-        _ => true, // first push (parent None) or impossible-shape after key → publish
-    };
-    let publication_result: Result<(), String> = if manifest_changed {
+    // manifest's refs/head. The event is derived from the commit and is never
+    // the commit itself. Every publication reaches this point with changed
+    // refs (`PushDisposition::Publish`), so there is always an event to emit.
+    let publication_result: Result<(), String> = {
         let inputs = RefStateInputs {
             repo_id: &ctx.repo_id,
             head: &success.manifest.head,
             refs: &success.manifest.refs,
             actor_pubkey_hex: &hex::encode(ctx.pusher.to_bytes()),
+            published_at: success.manifest.published_at,
         };
         match build_ref_state_event(&inputs, &state.relay_keypair) {
             Ok(event) => {
@@ -2341,20 +2300,15 @@ async fn finalize_push_inner(
             }
             Err(error) => Err(format!("kind:30618 build failed: {error}")),
         }
-    } else {
-        Ok(())
     };
 
     // The admitted serving write spans the complete publication attempt. Fence
     // acquisition cannot overtake the pointer CAS, durable 30618 insert, or
     // local fan-out attempt; only now may the lease be released.
+    // A failed release does not change the outcome either: the pointer CAS
+    // and the lease-guarded kind:30618 insert have both already happened.
     if let Err(error) = serving_write.finish().await {
         warn!(owner = %ctx.owner, repo = %ctx.repo, %error, "failed to release community serving lease after push publication");
-        return (
-            StatusCode::SERVICE_UNAVAILABLE,
-            "community write lease lost during publication",
-        )
-            .into_response();
     }
     if let Err(error) = publication_result {
         error!(
@@ -2536,16 +2490,378 @@ mod track_c_tests {
             "receive-pack failed: {}",
             String::from_utf8_lossy(&output.stderr)
         );
-        assert!(
-            !receive_pack_report_rejected(&output.stdout),
-            "receive-pack rejected the deletion: {}",
-            String::from_utf8_lossy(&output.stdout)
-        );
-
         assert!(!remote.join("refs/heads/main").exists());
         assert!(remote.join("refs/heads/master").exists());
     }
 
+    /// A pack with no objects, which a client sends when the refs it pushes
+    /// name objects the remote already has.
+    #[cfg(unix)]
+    const EMPTY_PACK: &[u8] = &[
+        b'P', b'A', b'C', b'K', 0, 0, 0, 2, 0, 0, 0, 0, 0x02, 0x9d, 0x08, 0x82, 0x3b, 0xd8, 0xa8,
+        0xea, 0xb5, 0x10, 0xad, 0x6a, 0xc7, 0x5c, 0x82, 0x3c, 0xfd, 0x3e, 0xd3, 0x1e,
+    ];
+
+    /// A `receive-pack` request body: one pkt-line per `(old, new, ref)`
+    /// command, the capability list on the first, a flush, and an empty pack
+    /// when there is a command.
+    #[cfg(unix)]
+    fn push_request(commands: &[(&str, &str, &str)], capabilities: &str) -> Vec<u8> {
+        let mut request = Vec::new();
+        for (index, (old, new, name)) in commands.iter().enumerate() {
+            let line = if index == 0 {
+                format!("{old} {new} {name}\0{capabilities}\n")
+            } else {
+                format!("{old} {new} {name}\n")
+            };
+            request.extend_from_slice(format!("{:04x}", line.len() + 4).as_bytes());
+            request.extend_from_slice(line.as_bytes());
+        }
+        request.extend_from_slice(b"0000");
+        if !commands.is_empty() {
+            request.extend_from_slice(EMPTY_PACK);
+        }
+        request
+    }
+
+    /// A hydrated workspace stand-in: a bare repository whose `main` is the
+    /// second of two commits, with a pre-receive hook that accepts or declines
+    /// every push. Returns the scratch root, the repository path, and the two
+    /// commit ids, oldest first. Unix only: the hook is a shell script made
+    /// executable through its file mode.
+    #[cfg(unix)]
+    fn push_fixture(hook_accepts: bool) -> (TempDir, std::path::PathBuf, String, String) {
+        use std::os::unix::fs::PermissionsExt;
+
+        let root = TempDir::new().expect("tempdir");
+        let remote = root.path().join("remote.git");
+        let source = root.path().join("source");
+        let remote_arg = remote.to_str().expect("utf-8 remote path");
+        let source_arg = source.to_str().expect("utf-8 source path");
+        let setup: [(&Path, &[&str]); 9] = [
+            (root.path(), &["init", "--bare", "--quiet", remote_arg]),
+            (
+                root.path(),
+                &["init", "--quiet", "--initial-branch=main", source_arg],
+            ),
+            (&source, &["config", "user.name", "Buzz Test"]),
+            (&source, &["config", "user.email", "buzz-test@example.com"]),
+            (
+                &source,
+                &["commit", "--quiet", "--allow-empty", "-m", "first"],
+            ),
+            (
+                &source,
+                &["commit", "--quiet", "--allow-empty", "-m", "second"],
+            ),
+            (&source, &["push", "--quiet", remote_arg, "main"]),
+            (&source, &["rev-parse", "HEAD~1"]),
+            (&source, &["rev-parse", "HEAD"]),
+        ];
+        let mut oids = Vec::new();
+        for (cwd, args) in setup {
+            let output = run_test_git(cwd, args, &[]);
+            assert!(
+                output.status.success(),
+                "git {args:?} failed: {}",
+                String::from_utf8_lossy(&output.stderr)
+            );
+            if args[0] == "rev-parse" {
+                oids.push(String::from_utf8(output.stdout).expect("utf-8 oid"));
+            }
+        }
+        let hook = remote.join("hooks").join("pre-receive");
+        std::fs::create_dir_all(remote.join("hooks")).expect("hooks directory");
+        let exit_code = if hook_accepts { 0 } else { 1 };
+        std::fs::write(
+            &hook,
+            format!("#!/bin/sh\ncat >/dev/null\nexit {exit_code}\n"),
+        )
+        .expect("write hook");
+        std::fs::set_permissions(&hook, std::fs::Permissions::from_mode(0o755))
+            .expect("make hook executable");
+        (
+            root,
+            remote,
+            oids[0].trim().to_string(),
+            oids[1].trim().to_string(),
+        )
+    }
+
+    /// The publish decision is taken from what `git receive-pack` did to the
+    /// workspace, for each way a push can end. Every case runs real git through
+    /// the production `run_git_at` and decides with the production
+    /// `observe_push`.
+    ///
+    /// The first two cases are the ones the earlier rule (publish when git
+    /// exits 0 and reports no `ng`) got wrong in the permissive direction: git
+    /// exits 0 and reports nothing, yet no push was accepted. A rule that
+    /// publishes when the report has an `ok` line or no `ng` line gets them
+    /// wrong in the same way. The last two cases are the ones the earlier rule
+    /// got wrong in the other direction: git reports `ok` for a ref it
+    /// updated, and the rule dropped that update because another ref was
+    /// refused, for a stale old value or for a name that conflicts with
+    /// another ref in the same push. The case before them shows that an `ok` line does not by itself
+    /// mean a ref changed.
+    #[cfg(unix)]
+    #[tokio::test]
+    async fn push_is_published_exactly_when_receive_pack_changed_refs() {
+        /// One ref-update command: `(old, new, ref)`.
+        type RefCommand = (String, String, &'static str);
+        struct Case {
+            name: &'static str,
+            hook_accepts: bool,
+            capabilities: &'static str,
+            /// Builds the commands from the two fixture commits.
+            commands: fn(&str, &str) -> Vec<RefCommand>,
+            expect: PushDisposition,
+            /// Status lines git must have reported to the client.
+            reported: &'static [&'static str],
+        }
+        let create_feature = |first: &str, _second: &str| {
+            vec![("0".repeat(40), first.to_string(), "refs/heads/feature")]
+        };
+        let cases = [
+            Case {
+                name: "request with no commands, hook would decline",
+                hook_accepts: false,
+                capabilities: "",
+                commands: |_, _| Vec::new(),
+                expect: PushDisposition::RelayOnly,
+                reported: &[],
+            },
+            Case {
+                name: "declined push from a client that asked for no status report",
+                hook_accepts: false,
+                capabilities: "",
+                commands: create_feature,
+                expect: PushDisposition::RelayOnly,
+                reported: &[],
+            },
+            Case {
+                name: "declined push with a status report",
+                hook_accepts: false,
+                capabilities: "report-status",
+                commands: create_feature,
+                expect: PushDisposition::RelayOnly,
+                reported: &["ng refs/heads/feature"],
+            },
+            Case {
+                name: "accepted push",
+                hook_accepts: true,
+                capabilities: "report-status",
+                commands: create_feature,
+                expect: PushDisposition::Publish,
+                reported: &["ok refs/heads/feature"],
+            },
+            Case {
+                name: "accepted command that asks for the value the ref already has",
+                hook_accepts: true,
+                capabilities: "report-status",
+                // git reports `ok` and changes nothing, so there is nothing
+                // to publish and the report is true of the published state.
+                commands: |_, second| {
+                    vec![(second.to_string(), second.to_string(), "refs/heads/main")]
+                },
+                expect: PushDisposition::RelayOnly,
+                reported: &["ok refs/heads/main"],
+            },
+            Case {
+                name: "accepted push, one ref updated and one refused",
+                hook_accepts: true,
+                capabilities: "report-status",
+                // `main` is at the second commit, so an update that names the
+                // first commit as its old value is refused.
+                commands: |first, second| {
+                    vec![
+                        ("0".repeat(40), first.to_string(), "refs/heads/feature"),
+                        (first.to_string(), second.to_string(), "refs/heads/main"),
+                    ]
+                },
+                expect: PushDisposition::Publish,
+                reported: &["ok refs/heads/feature", "ng refs/heads/main"],
+            },
+            Case {
+                name: "accepted push, two refs whose names conflict",
+                hook_accepts: true,
+                capabilities: "report-status",
+                // A ref name cannot be both a file and a directory, so git
+                // creates one of `feature` and `feature/x` and refuses the
+                // other. Which one it creates depends on the git version, so
+                // the expected lines match either outcome and the check below
+                // ties each ref's presence to its own `ok` line.
+                commands: |first, second| {
+                    vec![
+                        ("0".repeat(40), first.to_string(), "refs/heads/feature"),
+                        ("0".repeat(40), second.to_string(), "refs/heads/feature/x"),
+                    ]
+                },
+                expect: PushDisposition::Publish,
+                reported: &["ok refs/heads/feature", "ng refs/heads/feature"],
+            },
+        ];
+
+        for case in cases {
+            let (root, remote, first, second) = push_fixture(case.hook_accepts);
+            let before = snapshot_workspace(&remote).await.expect("snapshot before");
+            assert_eq!(before.refs.get("refs/heads/main"), Some(&second));
+            let mut parent_state = ParentState::fresh();
+            parent_state.parent.refs = before.refs.clone();
+
+            let commands = (case.commands)(&first, &second);
+            let borrowed: Vec<(&str, &str, &str)> = commands
+                .iter()
+                .map(|(old, new, name)| (old.as_str(), new.as_str(), *name))
+                .collect();
+            let request = push_request(&borrowed, case.capabilities);
+            let git_config = receive_pack_git_config(remote.join("hooks").display().to_string());
+            let pack = match run_git_at(
+                &remote,
+                "receive-pack",
+                Body::from(request),
+                &git_config,
+                root.path(),
+                RECEIVE_PACK_MAX_OUTPUT_BYTES,
+            )
+            .await
+            {
+                Ok(pack) => pack,
+                Err(response) => panic!("{}: run_git_at failed: {}", case.name, response.status()),
+            };
+            // git exits 0 in every case, so the exit status cannot be what
+            // separates an accepted push from a declined or empty one.
+            assert!(pack.exited_ok, "{}: receive-pack exit status", case.name);
+            let stdout = String::from_utf8_lossy(&pack.stdout).to_string();
+            for line in case.reported {
+                assert!(
+                    stdout.contains(line),
+                    "{}: expected {line:?} in {stdout:?}",
+                    case.name
+                );
+            }
+            if case.reported.is_empty() {
+                assert!(
+                    !stdout.contains("ng ") && !stdout.contains("ok "),
+                    "{}: expected no status report, got {stdout:?}",
+                    case.name
+                );
+            }
+
+            let (disposition, after) = observe_push(&pack, &parent_state, &remote)
+                .await
+                .expect("observe push");
+            assert_eq!(disposition, case.expect, "{}", case.name);
+            // The snapshot handed to the publication holds exactly the refs
+            // git reported as created.
+            for created in ["refs/heads/feature", "refs/heads/feature/x"] {
+                assert_eq!(
+                    after.refs.contains_key(created),
+                    stdout.contains(&format!("ok {created}\n")),
+                    "{}: {created} in snapshot",
+                    case.name
+                );
+            }
+            assert_eq!(
+                after.refs.get("refs/heads/main"),
+                Some(&second),
+                "{}",
+                case.name
+            );
+        }
+    }
+
+    /// A push whose ref snapshot crosses the manifest ref cap is a permanent
+    /// repository limit: it must answer 413, as the publish path did before
+    /// the snapshot moved ahead of the publish decision, not a 500 a client
+    /// would retry.
+    #[cfg(unix)]
+    #[tokio::test]
+    async fn snapshot_resource_limit_answers_413() {
+        let state = crate::state::tests::test_state().await;
+        let scratch = TempDir::new().expect("scratch");
+        let listener = tokio::net::TcpListener::bind("127.0.0.1:0")
+            .await
+            .expect("mock object store listener");
+        let addr = listener.local_addr().expect("mock address");
+        let app = Router::new().fallback(|| async { StatusCode::NOT_FOUND });
+        let server = tokio::spawn(async move { axum::serve(listener, app).await });
+        let store = super::super::store::GitStore::new(
+            &format!("http://{addr}"),
+            "fixture",
+            "fixture",
+            "fixture",
+            "us-east-1",
+            buzz_media::config::S3AddressingStyle::Path,
+        )
+        .expect("mock Git store");
+        let tenant = TenantContext::resolved(
+            CommunityId::from_uuid(uuid::Uuid::from_u128(1)),
+            "git.example",
+        );
+        let (hydrated, parent_state) = hydrate_for_write(
+            &store,
+            &tenant,
+            &"a".repeat(64),
+            "snapshot-limit",
+            HydrationOptions {
+                pack_cache: &state.git_pack_cache,
+                scratch_dir: scratch.path(),
+                max_pack_bytes: 1024 * 1024,
+                max_repo_bytes: 2 * 1024 * 1024,
+            },
+        )
+        .await
+        .expect("hydrate empty fixture");
+        server.abort();
+        let _ = server.await;
+
+        let (_fixture_root, source, _, tip) = push_fixture(true);
+        assert_git_success(
+            run_test_git(
+                &source,
+                &["push", "--quiet", hydrated.path().to_str().unwrap(), "main"],
+                &[],
+            ),
+            "seed fixture commit",
+        );
+        let mut packed_refs = String::from("# pack-refs with: peeled fully-peeled sorted\n");
+        for index in 0..=super::super::manifest::MAX_MANIFEST_REFS {
+            packed_refs.push_str(&format!("{tip} refs/heads/ref-{index:05}\n"));
+        }
+        std::fs::write(hydrated.path().join("packed-refs"), packed_refs).expect("fixture refs");
+        assert!(matches!(
+            snapshot_workspace(hydrated.path()).await,
+            Err(CasError::ResourceLimit(_))
+        ));
+        let response = finalize_push(
+            &state,
+            PushContext {
+                pack: PackOutput {
+                    stdout: Vec::new(),
+                    exited_ok: true,
+                },
+                parent_state,
+                owner: "a".repeat(64),
+                repo: "snapshot-limit".into(),
+                repo_id: "snapshot-limit".into(),
+                pusher: Keys::generate().public_key(),
+                tenant,
+                repo_handle: hydrated,
+            },
+        )
+        .await;
+        let status = response.status();
+        let body = axum::body::to_bytes(response.into_body(), 4096)
+            .await
+            .unwrap();
+        assert_eq!(
+            status,
+            StatusCode::PAYLOAD_TOO_LARGE,
+            "snapshot resource limits must not become backend errors; body: {}",
+            String::from_utf8_lossy(&body)
+        );
+    }
+
     async fn run_finalize_git(repo: &Path, args: &[&str]) -> std::process::Output {
         let mut command = Command::new("git");
         command.current_dir(repo).args(args);
@@ -2657,7 +2973,10 @@ mod track_c_tests {
         (request, claim)
     }
 
-    async fn pushed_context(
+    /// A push context whose workspace is exactly as hydrated: what
+    /// `finalize_push` receives when `receive-pack` exited 0 without applying
+    /// a command (a declined push, or a request with no commands).
+    async fn unchanged_context(
         state: &AppState,
         community: CommunityId,
         host: &str,
@@ -2681,6 +3000,32 @@ mod track_c_tests {
         )
         .await
         .expect("hydrate empty test repo");
+        PushContext {
+            pack: PackOutput {
+                stdout: b"git-answer".to_vec(),
+                exited_ok: true,
+            },
+            parent_state,
+            owner,
+            repo: repo.clone(),
+            repo_id: repo,
+            pusher,
+            tenant,
+            repo_handle: hydrated,
+        }
+    }
+
+    /// A push context whose workspace gained a commit on `main`.
+    async fn pushed_context(
+        state: &AppState,
+        community: CommunityId,
+        host: &str,
+        owner: String,
+        repo: String,
+        pusher: nostr::PublicKey,
+        scratch: &Path,
+    ) -> PushContext {
+        let mut ctx = unchanged_context(state, community, host, owner, repo, pusher, scratch).await;
         let source = scratch.join("source");
         tokio::fs::create_dir(&source)
             .await
@@ -2693,22 +3038,15 @@ mod track_c_tests {
             .expect("write source file");
         run_finalize_git(&source, &["add", "file.txt"]).await;
         run_finalize_git(&source, &["commit", "--quiet", "-m", "committed"]).await;
-        let remote = hydrated.path().to_str().expect("hydrated path utf8");
-        run_finalize_git(&source, &["push", "--quiet", remote, "main"]).await;
-
-        PushContext {
-            pack: PackOutput {
-                stdout: b"push-ok".to_vec(),
-                ok: true,
-            },
-            parent_state,
-            owner,
-            repo: repo.clone(),
-            repo_id: repo,
-            pusher,
-            tenant,
-            repo_handle: hydrated,
-        }
+        let remote = ctx
+            .repo_handle
+            .path()
+            .to_str()
+            .expect("hydrated path utf8")
+            .to_string();
+        run_finalize_git(&source, &["push", "--quiet", &remote, "main"]).await;
+        ctx.pack.stdout = b"push-ok".to_vec();
+        ctx
     }
 
     async fn repo_announcement_holds_serving_lease_until_pointer_is_seeded() {
@@ -2834,6 +3172,7 @@ mod track_c_tests {
         let hooks = FinalizePushHooks {
             post_cas_gate: Some(Arc::clone(&gate)),
             fail_ref_state_insert: false,
+            lose_lease_signal_after_cas: false,
         };
         let finalize_state = Arc::clone(&state);
         let finalize =
@@ -2924,6 +3263,7 @@ mod track_c_tests {
         let hooks = FinalizePushHooks {
             post_cas_gate: None,
             fail_ref_state_insert: true,
+            lose_lease_signal_after_cas: false,
         };
 
         let response = finalize_push_inner(&state, ctx, &hooks).await;
@@ -2938,6 +3278,131 @@ mod track_c_tests {
         pool.close().await;
     }
 
+    async fn finalize_push_lease_signal_after_landed_cas_still_publishes() {
+        let (state, pool) = finalize_test_state().await;
+        let host = format!(
+            "git-finalize-lease-signal-{}.example",
+            uuid::Uuid::new_v4().simple()
+        );
+        let community = state
+            .db
+            .ensure_configured_community(&host)
+            .await
+            .expect("create test community")
+            .id;
+        let scratch = TempDir::new().expect("scratch");
+        let owner = format!("owner-{}", uuid::Uuid::new_v4().simple());
+        let repo = format!("repo-{}", uuid::Uuid::new_v4().simple());
+        let ctx = pushed_context(
+            &state,
+            community,
+            &host,
+            owner.clone(),
+            repo.clone(),
+            Keys::generate().public_key(),
+            scratch.path(),
+        )
+        .await;
+        let hooks = FinalizePushHooks {
+            post_cas_gate: None,
+            fail_ref_state_insert: false,
+            lose_lease_signal_after_cas: true,
+        };
+
+        let response = finalize_push_inner(&state, ctx, &hooks).await;
+        assert_eq!(
+            response.status(),
+            StatusCode::OK,
+            "a landed CAS must not be reported as a failed push"
+        );
+        let pointer = crate::api::git::manifest::pointer_key(community, &owner, &repo);
+        assert!(
+            state
+                .git_store
+                .get_pointer(&pointer)
+                .await
+                .expect("read pointer")
+                .is_some(),
+            "the CAS landed"
+        );
+        let mut query = buzz_db::event::EventQuery::for_community(community);
+        query.kinds = Some(vec![30_618]);
+        query.d_tag = Some(repo);
+        let events = state.db.query_events(&query).await.expect("query 30618");
+        assert_eq!(
+            events.len(),
+            1,
+            "the landed CAS still derives its kind:30618"
+        );
+        assert!(state
+            .db
+            .deletion_store()
+            .serving_writes_drained(community)
+            .await
+            .expect("serving lease released"));
+        drop(state);
+        pool.close().await;
+    }
+
+    /// git exits 0 for a push the hook declined and for a request with no
+    /// commands. Neither changes a ref, so the relay must answer with git's
+    /// output and publish nothing: no pointer write, and no kind:30618 naming
+    /// the caller as the pusher of a state they were not allowed to push.
+    async fn finalize_push_publishes_nothing_when_receive_pack_changed_no_ref() {
+        let (state, pool) = finalize_test_state().await;
+        let host = format!(
+            "git-finalize-unchanged-{}.example",
+            uuid::Uuid::new_v4().simple()
+        );
+        let community = state
+            .db
+            .ensure_configured_community(&host)
+            .await
+            .expect("create test community")
+            .id;
+        let scratch = TempDir::new().expect("scratch");
+        let owner = format!("owner-{}", uuid::Uuid::new_v4().simple());
+        let repo = format!("repo-{}", uuid::Uuid::new_v4().simple());
+        let ctx = unchanged_context(
+            &state,
+            community,
+            &host,
+            owner.clone(),
+            repo.clone(),
+            Keys::generate().public_key(),
+            scratch.path(),
+        )
+        .await;
+
+        let response = finalize_push_inner(&state, ctx, &FinalizePushHooks::default()).await;
+        assert_eq!(response.status(), StatusCode::OK);
+        let body = axum::body::to_bytes(response.into_body(), usize::MAX)
+            .await
+            .expect("response body");
+        assert_eq!(&body[..], b"git-answer", "git's own answer is relayed");
+
+        let pointer = crate::api::git::manifest::pointer_key(community, &owner, &repo);
+        assert!(
+            state
+                .git_store
+                .get_pointer(&pointer)
+                .await
+                .expect("read pointer")
+                .is_none(),
+            "a push that changed no ref must not write the pointer"
+        );
+        let mut query = buzz_db::event::EventQuery::for_community(community);
+        query.kinds = Some(vec![30_618]);
+        query.d_tag = Some(repo);
+        let events = state.db.query_events(&query).await.expect("query 30618");
+        assert!(
+            events.is_empty(),
+            "a push that changed no ref must not be attributed to the caller"
+        );
+        drop(state);
+        pool.close().await;
+    }
+
     mod external_infra_minio_tests {
         #[tokio::test]
         #[ignore = "requires Postgres and MinIO"]
@@ -2956,6 +3421,18 @@ mod track_c_tests {
         async fn finalize_push_db_failure_after_cas_is_not_success_and_releases_lease() {
             super::finalize_push_db_failure_after_cas_is_not_success_and_releases_lease().await;
         }
+
+        #[tokio::test]
+        #[ignore = "requires Postgres and MinIO"]
+        async fn finalize_push_lease_signal_after_landed_cas_still_publishes() {
+            super::finalize_push_lease_signal_after_landed_cas_still_publishes().await;
+        }
+
+        #[tokio::test]
+        #[ignore = "requires Postgres and MinIO"]
+        async fn finalize_push_publishes_nothing_when_receive_pack_changed_no_ref() {
+            super::finalize_push_publishes_nothing_when_receive_pack_changed_no_ref().await;
+        }
     }
 
     /// A gzip-encoded request body is transparently inflated before it
@@ -3078,6 +3555,7 @@ mod track_c_tests {
             refs,
             packs: vec!["packs/deadbeef".to_string()],
             parent: None,
+            published_at: None,
         }
     }
 
@@ -3097,12 +3575,6 @@ mod track_c_tests {
         serde_json::to_string(&event).expect("serialize")
     }
 
-    fn pkt(payload: &[u8]) -> Vec<u8> {
-        let mut out = Vec::new();
-        super::pkt_line(&mut out, payload);
-        out
-    }
-
     #[test]
     fn streaming_body_holds_git_permit_until_drop() {
         let semaphore = Arc::new(tokio::sync::Semaphore::new(1));
@@ -3156,95 +3628,6 @@ mod track_c_tests {
         assert_eq!(stream.streamed_bytes, 5);
     }
 
-    /// Wrap inner status pkt-lines in one side-band-64k band-1 (data) outer
-    /// pkt-line — the real shape git emits when side-band is negotiated:
-    /// `<outer-len>\x01<inner-pkt-lines>`.
-    fn sideband_data(inner_pkts: &[&[u8]]) -> Vec<u8> {
-        let mut inner = vec![0x01u8]; // band 1 = data channel
-        for p in inner_pkts {
-            inner.extend(pkt(p));
-        }
-        pkt(&inner)
-    }
-
-    #[test]
-    fn receive_pack_report_rejected_detects_plain_ng_line() {
-        // No side-band: status pkt-lines at the outer level.
-        let mut out = Vec::new();
-        out.extend(pkt(b"unpack ok\n"));
-        out.extend(pkt(b"ng refs/heads/main pre-receive hook declined\n"));
-        out.extend_from_slice(b"0000");
-
-        assert!(receive_pack_report_rejected(&out));
-    }
-
-    #[test]
-    fn receive_pack_report_rejected_detects_sideband_ng_line() {
-        // Real side-band-64k shape: status pkt-lines NESTED inside a band-1
-        // outer pkt-line. A naive "strip band byte, split on \n" parser misses
-        // this — the rejection surfaces as `0031ng refs/...`.
-        let mut out = sideband_data(&[
-            b"unpack ok\n",
-            b"ng refs/heads/main pre-receive hook declined\n",
-        ]);
-        out.extend_from_slice(b"0000");
-
-        assert!(receive_pack_report_rejected(&out));
-    }
-
-    #[test]
-    fn receive_pack_report_rejected_ignores_ok_status() {
-        // Real side-band-64k success shape — nested `ok` pkt-lines, no `ng`.
-        let mut out = sideband_data(&[b"unpack ok\n", b"ok refs/heads/main\n"]);
-        out.extend_from_slice(b"0000");
-
-        assert!(!receive_pack_report_rejected(&out));
-    }
-
-    #[test]
-    fn receive_pack_report_rejected_matches_real_git_deny_shape() {
-        // Mirrors report-status captured from `git receive-pack` (2.50.1) on a
-        // pre-receive hook decline:
-        //   <band2>policy: denied\n                 (progress/error text)
-        //   <band1>000eunpack ok\n0031ng refs/heads/main pre-receive hook declined\n
-        //   0000
-        // The band-1 payload carries its OWN inner pkt stream — the exact case
-        // a flat parser returns `false` on.
-        let mut out = Vec::new();
-        out.extend(pkt(b"\x02policy: denied\n")); // band 2 = progress/error
-        out.extend(sideband_data(&[
-            b"unpack ok\n",
-            b"ng refs/heads/main pre-receive hook declined\n",
-        ]));
-        out.extend_from_slice(b"0000");
-
-        assert!(
-            receive_pack_report_rejected(&out),
-            "must detect the nested band-1 ng line on a real deny"
-        );
-    }
-
-    #[test]
-    fn receive_pack_report_rejected_ignores_progress_channel_noise() {
-        // A band-2 (progress) line must never be mistaken for a status line,
-        // even if it contained bytes resembling a status — only band-1 counts.
-        let mut out = Vec::new();
-        out.extend(pkt(b"\x02ng-looking progress noise\n")); // band 2 noise
-        out.extend(sideband_data(&[b"unpack ok\n", b"ok refs/heads/main\n"]));
-        out.extend_from_slice(b"0000");
-
-        assert!(!receive_pack_report_rejected(&out));
-    }
-
-    #[test]
-    fn receive_pack_report_rejected_handles_truncated_and_malformed() {
-        // Defensive: malformed length / truncated frame yields no match, never
-        // a panic.
-        assert!(!receive_pack_report_rejected(b""));
-        assert!(!receive_pack_report_rejected(b"zzzz"));
-        assert!(!receive_pack_report_rejected(b"0048")); // length, no payload
-    }
-
     #[test]
     fn git_expected_url_uses_tenant_host_not_config_host() {
         let tenant_a = tenant("host-a.example", 1);
diff --git a/crates/buzz-relay/src/handlers/side_effects.rs b/crates/buzz-relay/src/handlers/side_effects.rs
index 53bbbf1057..f7f83f2494 100644
--- a/crates/buzz-relay/src/handlers/side_effects.rs
+++ b/crates/buzz-relay/src/handlers/side_effects.rs
@@ -4195,6 +4195,7 @@ async fn seed_manifest_pointer(
         refs: BTreeMap::new(),
         packs: Vec::new(),
         parent: None,
+        published_at: None,
     };
     empty
         .validate()
@@ -4310,6 +4311,7 @@ async fn emit_initial_ref_state(
         head: DEFAULT_HEAD,
         refs: &empty_refs,
         actor_pubkey_hex: owner_hex,
+        published_at: None,
     };
     let event = build_ref_state_event(&inputs, &state.relay_keypair)
         .map_err(|e| anyhow::anyhow!("build_ref_state_event: {e}"))?;
diff --git a/crates/buzz-test-client/tests/e2e_git.rs b/crates/buzz-test-client/tests/e2e_git.rs
index 3c82e31764..7a0a910ed1 100644
--- a/crates/buzz-test-client/tests/e2e_git.rs
+++ b/crates/buzz-test-client/tests/e2e_git.rs
@@ -531,6 +531,99 @@ async fn git_concurrent_push_one_wins_and_repo_recovers() {
     );
 }
 
+/// A non-atomic multi-ref push can be partially accepted: git applies each ref
+/// update independently and reports `ok` for the refs it applied. The relay
+/// must publish those refs, or the client records an update that never landed.
+#[tokio::test]
+#[ignore = "requires live relay + MinIO + git"]
+async fn git_partial_push_publishes_accepted_refs() {
+    use nostr::ToBech32;
+
+    let owner = Keys::generate();
+    let owner_hex = owner.public_key().to_hex();
+    let owner_nsec = owner.secret_key().to_bech32().unwrap();
+    let repo = format!("e2e-git-partial-{}", std::process::id());
+    let s3 = GitS3Probe::from_env();
+
+    let channel = create_test_channel(&owner).await;
+    let announce = EventBuilder::new(Kind::from(30617), "")
+        .tags(vec![
+            Tag::parse(["d", &repo]).unwrap(),
+            Tag::parse(["name", "e2e partial push repo"]).unwrap(),
+            Tag::parse(["buzz-channel", &channel]).unwrap(),
+        ])
+        .sign_with_keys(&owner)
+        .unwrap();
+    post_event(&announce).await;
+    tokio::time::sleep(std::time::Duration::from_secs(2)).await;
+
+    let tmp = tempdir_named("buzz-e2e-git-partial");
+    let url = format!("{}/git/{}/{}", relay_http_url(), owner_hex, repo);
+
+    git(&["clone", "--quiet", &url, "work"], tmp.path(), &owner_nsec);
+    let work = tmp.path().join("work");
+    std::fs::write(work.join("README.md"), "base\n").unwrap();
+    git(&["add", "."], &work, &owner_nsec);
+    git(&["commit", "--quiet", "-m", "base"], &work, &owner_nsec);
+    git(&["branch", "-M", "main"], &work, &owner_nsec);
+    git(
+        &["push", "--quiet", "origin", "main", "main:feature"],
+        &work,
+        &owner_nsec,
+    );
+    let base_pointer = s3.require_pointer(&owner_hex, &repo).await;
+
+    // `feature/x` conflicts with the existing `feature` branch, so git rejects
+    // it while applying the fast-forward of `main`.
+    std::fs::write(work.join("README.md"), "base\nnext\n").unwrap();
+    git(&["commit", "--quiet", "-am", "next"], &work, &owner_nsec);
+    let next_sha = git(&["rev-parse", "main"], &work, &owner_nsec)
+        .trim()
+        .to_string();
+    let out = git_status(
+        &["push", "origin", "main", "main:refs/heads/feature/x"],
+        &work,
+        &owner_nsec,
+    );
+    let stderr = String::from_utf8_lossy(&out.stderr);
+    assert!(
+        !out.status.success(),
+        "feature/x must be rejected: {stderr}"
+    );
+    assert!(
+        stderr.contains("main -> main"),
+        "client reports main as pushed: {stderr}"
+    );
+
+    let after_pointer = s3.require_pointer(&owner_hex, &repo).await;
+    assert_ne!(
+        after_pointer, base_pointer,
+        "the accepted main update must advance the S3 manifest pointer"
+    );
+    git(
+        &["clone", "--quiet", &url, "after"],
+        tmp.path(),
+        &owner_nsec,
+    );
+    let after = tmp.path().join("after");
+    assert_eq!(
+        git(&["rev-parse", "main"], &after, &owner_nsec).trim(),
+        next_sha,
+        "a fresh clone sees the main update the client was told landed"
+    );
+    let feature_x = git_status(
+        &[
+            "rev-parse",
+            "--verify",
+            "--quiet",
+            "refs/remotes/origin/feature/x",
+        ],
+        &after,
+        &owner_nsec,
+    );
+    assert!(!feature_x.status.success(), "rejected feature/x is absent");
+}
+
 struct TempDir(PathBuf);
 impl TempDir {
     fn path(&self) -> &Path {
diff --git a/docs/git-on-object-storage.md b/docs/git-on-object-storage.md
index 7b5a5aeee7..f8a2309379 100644
--- a/docs/git-on-object-storage.md
+++ b/docs/git-on-object-storage.md
@@ -6,39 +6,55 @@
 
 This document specifies a protocol for hosting git repositories on an object
 store (S3 and S3-compatible backends such as MinIO) with **no persistent
-filesystem**, and gives a formal proof of its safety properties. Repository
+filesystem**, and states what has been verified about it. Repository
 content is stored as create-only, content-addressed pack objects (immutable by
 protocol discipline — see A1, not by assuming an immutable store); the current
 state of every ref is captured by a single mutable *manifest pointer* updated
-by atomic compare-and-swap (CAS). We prove two safety theorems —
-**durability-ordering** (a client never observes success for a ref change that
-is not yet durable) and **manifest reconstruction** (hydrating a published
-manifest reconstructs every object reachable from its refs; the named pack set is
-a superset of that closure) — and one
-**linearizability** theorem (concurrent ref-changing pushes never lose an
-update). All three reduce to three explicitly stated object-store axioms.
+by atomic compare-and-swap (CAS).
+
+The correctness statement is a refinement. Every behavior of the protocol is a
+behavior of an *atomic ref database* (`docs/spec/GitRefDB.tla`), in which a push
+takes effect in one step, is applied only if it is authorized and only against
+the ref values it names, and is reported to the client truthfully. This covers
+**linearizability** (concurrent pushes never lose an update) and the client-side
+half of **durability-ordering** (a client is never told an update succeeded
+unless it was published). Three further properties concern storage: the pointer
+never names an object that is not stored, the packs a published manifest lists
+contain every object reachable from its refs (**manifest reconstruction**), and
+whatever a reader has resolved stays fetchable.
+
+Three kinds of evidence support these statements, and §Mechanized Verification
+says which claim rests on which. The refinement and the storage properties are
+model-checked exhaustively for small instances. The pointer discipline is
+proved in Lean for any number of clients, refs and objects. The correspondence
+between the models and the Rust code rests on tests and review. All of it is
+relative to three object-store axioms and to a stated contract for
+`git receive-pack`. Two further behaviors of the implementation, the
+serving-write lease and the order of the derived kind:30618 events, are checked
+in a separate bounded model.
 
 The protocol is not novel as an *algorithm*: it is git's post-reftable ref
 model — immutable content artifacts plus an atomic pointer swap — with the
 atomic primitive substituted from POSIX `rename()` to an S3 conditional `PUT`.
 The contribution of this document is the **formal characterization**: to our
 knowledge, no prior formal treatment of git refs over conditional-write object
-storage exists (see Prior Art). The proof is *parametric over the atomic
+storage exists (see Prior Art). The argument is *parametric over the atomic
 primitive*: it holds for any backend satisfying the three axioms, and a concrete
 backend is *admitted for deployment* by a single conformance gate (a finite probe
 cannot prove a universal axiom; it can only admit or reject a backend).
 
 ## Scope and Non-Goals
 
-This specification proves **safety** ("nothing bad happens"). It deliberately
-does **not** prove:
+This specification concerns **safety** ("nothing bad happens"). It deliberately
+does **not** establish:
 
 - **Liveness or performance.** That a hydrate completes within a latency budget
   is empirical, not formal; it is characterized by benchmark, not theorem.
 - **Git's internal correctness.** `git index-pack`, `upload-pack`, and
-  `receive-pack` are trusted upstream components. We prove only that our
-  *composition* feeds them well-formed inputs and surfaces their outputs
-  faithfully.
+  `receive-pack` are trusted upstream components. The models represent
+  `receive-pack` by a stated contract (assumption G1, §Mechanized Verification)
+  and check that our *composition* publishes exactly what git did and reports
+  git's outputs faithfully.
 - **The object-store axioms themselves.** S3's durability, read-after-write
   consistency, and conditional-write linearizability are stated as axioms
   (§Axioms); each backend is *admitted* per-deployment by an empirical conformance
@@ -88,7 +104,8 @@ or a sustained-load regime the conformance probe (§Conformance) doesn't
 already exercise. The non-negotiable rule: retry, if added, lives in the
 store layer and retries *only* pre-classification network errors — never
 `Ok(2xx)`, `LostRace(412)`, or `NotFound(404)`. Retrying a classified
-outcome would change the TLA action and break the proof.
+outcome would change the modeled action, and the checked results would no
+longer apply to the code.
 
 ## System Model
 
@@ -254,62 +271,113 @@ alter what `d` resolves to; and (ii) **no pack `d` names is ever deleted**
 published [A1 + A2, §Push step order], so a reader holding an older `d` can always
 GET every pack — a concurrent GC that prunes packs unreachable from the *new*
 pointer never 404s this reader. This read-consistency-during-writer property is the
-reason the no-deletion rule is load-bearing, not cosmetic; it is asserted in the
-prose here because the mechanized model has no Read action (it checks the writer
-side; this is the reader-side complement).
+reason the no-deletion rule is load-bearing, not cosmetic. The model has a
+reader process and checks the property as `ReaderComplete`; a seeded deletion of
+an unlisted pack violates it (§Mechanized Verification).
 
 ### Push
 
 ```
-1. receive-pack: accept the pack, index it, derive new object set O.
-2. for each o in O: PUT pack-object(o)            # content-addressed, idempotent (A1)
-3. (e, d_before) := pointer(R); m_before := manifest(d_before)
-4. validate Δ against m_before.refs               # fast-forward / push rules
-       on rejection -> respond non-ff, STOP (no write, no fence cost)
-5. m_after := m_before with refs updated per Δ; packs := m_before.packs ∪ keys(O)
-6. d_after := PUT manifest-object(m_after)         # content-addressed (A1)
-7. result := PUT M_R (value = d_after)          # CAS (A3)
-       If-Match: e         if a pointer already exists (e from step 3)
-       If-None-Match: *    if the repo has no pointer yet (first push / repo init)
-       on 412 (lost race): re-read pointer, GOTO 3 (retry) or respond non-ff
+1. (e, d_before) := pointer(R); m_before := manifest(d_before)
+   hydrate an ephemeral workspace W from m_before      # one pointer observation
+2. receive-pack on W with the pre-receive hook installed:
+       the hook submits the whole command list Δ to the push policy;
+           if the policy declines, git applies no command
+       git applies a command only if its old_id is the ref's value in W
+3. refs_after := refs(W)                              # what git actually did
+       refs_after = m_before.refs -> relay git's output, STOP (nothing to publish)
+       git exited abnormally      -> respond error, STOP (nothing is published)
+4. O := a pack of the objects reachable from refs_after but not from
+        m_before.refs (delta), or of all objects reachable from refs_after
+        (compaction)
+5. PUT pack-object(O)                                 # content-addressed, create-only (A1)
+6. m_after := (refs_after, head, packs, parent = d_before)
+        packs = m_before.packs ∪ keys(O), or keys(O) alone after compaction
+   d_after := PUT manifest-object(m_after)            # content-addressed (A1)
+7. result := PUT M_R (value = d_after)                # CAS (A3)
+       If-Match: e         if a pointer already exists (e from step 1)
+       If-None-Match: *    if the repo has no pointer yet
+       on 412 (lost race): respond conflict (HTTP 409), STOP
        on success: the ref change is PUBLISHED
-8. construct success response   # ONLY after step 7 succeeds  -- the FENCE
+8. relay git's output to the client   # ONLY after step 7 succeeds  -- the FENCE
 ```
 
-**The fence (step 8 after step 7).** The success response is not constructed
-until the CAS in step 7 returns success. This is the publish-ordering
-guarantee. It is *conditional on refs changing*: a no-op or rejected push
-(step 4) never reaches step 7 and pays zero CAS/fence latency.
+**The fence (step 8 after step 7).** Git's status report for a push that
+changed refs is not sent until the CAS in step 7 returns success. This is the
+publish-ordering guarantee. It applies only when refs changed: a push that git
+declined, or one that changed nothing, stops at step 3 and performs no write.
+
+**Publication is decided from the workspace (step 3).** The relay does not infer
+what git did from git's exit status or from the status report in its output.
+Both are unreliable for this purpose. `git receive-pack` exits 0 when the
+pre-receive hook declines a push and when a request carries no commands, it
+reports a declined push only to a client that asked for a status report, and a
+push with several commands can end with some applied and others refused. The
+relay therefore compares the refs in the workspace after `receive-pack` with
+the refs the workspace was hydrated from. If they are equal, nothing is
+published and the client receives git's own answer. That answer contains `ok`
+only for a command whose new value equals its old value: git accepts such a
+command and changes nothing, and its report is true of the published state the
+workspace was hydrated from. If they differ and git
+exited normally, exactly the refs now in the workspace are published, so the
+`ok` and `ng` lines git reported per ref are true of the published state. If
+they differ and git exited abnormally, the request fails and nothing is
+published. Under the contract G1 for `receive-pack` (§Mechanized Verification),
+a changed workspace implies that the push policy accepted the command list, so
+a publication always acts for an authorized push.
 
 **No advisory lock.** Reftable serializes writers with `tables.list.lock` *and*
 the rename. This protocol has **no advisory lock in v1**: writer serialization
-is provided entirely by the CAS in step 7. §Theorem 3 proves this is
+is provided entirely by the CAS in step 7. Theorem 3 states that this is
 sufficient — the lock reftable uses is an optimization (it avoids wasted work
 under contention), not a correctness requirement, *given A3*.
 
-**Retry is policy, not safety.** The "GOTO 3" loop on a 412 is a *liveness/policy*
-choice — retry count, backoff, or immediate non-ff rejection are all sound. Safety
-(Theorems 1–3) holds for any of them, because a losing push that retries simply
-re-runs steps 3–7 against the advanced pointer; it never writes `M_R` while
-predicated on a stale ETag. We deliberately make no liveness claim here (§Scope).
+**No retry inside a request.** A push that loses the race at step 7 is answered
+with a conflict. Its workspace was computed from a manifest that is no longer
+current, so nothing derived from it may be published; the client pushes again,
+which starts at step 1 against the new pointer. Whether and when a client
+retries is a liveness matter and affects none of the safety properties. We
+deliberately make no liveness claim here (§Scope).
 
 ## Safety Theorems
 
-Let a push `p` be **ref-changing** if it reaches step 7. Let `observe(p) =
-success` mean a client received `p`'s success response (step 8 executed).
+This section states the properties the protocol is required to have. The
+statements are numbered as theorems because the implementation's comments cite
+them by number. The paragraphs marked *Argument* explain why each property
+holds; they are explanations and not the evidence. The evidence is in
+§Mechanized Verification: each statement is checked exhaustively by TLC for
+small instances, and the parts of Theorems 1–3 that concern the pointer are
+proved in Lean without a bound on clients, refs or objects.
+
+Two definitions are used throughout. A push is **published** when its
+conditional write in step 7 succeeds. A client is **told `ok` for a ref** when
+the response it receives contains git's status line `ok <ref>`.
 
 ### Theorem 1 (Durability-Ordering)
 
-> If `observe(p) = success` for a ref-changing push `p`, then at the moment of
-> observation, `pointer(R)` has held a value `d_after` whose manifest reflects
-> `p`'s ref updates, and that manifest and all packs it names are durable.
+> (a) Whenever the pointer names a manifest, that manifest and every pack it
+> lists are stored. (b) If a client is told `ok` for a command that changes a
+> ref, the push was published before the response was sent, and the published
+> manifest holds the value the client asked for.
 
-**Proof.** Step 8 executes only after step 7 returns success (program order;
-enforced by type in the implementation — see §Implementation Correspondence).
-By A3, step 7's success means `M_R` was atomically set to `d_after`. By A1,
-`manifest(d_after)` (written step 6) and every pack in `O` (written step 2,
-before step 6) are durable. The fence orders the client-visible success strictly
-after the durable pointer swap. Therefore observation implies durability. ∎
+**Argument.** For (a), a manifest becomes the pointer's value only in step 7,
+and the same request stored that manifest in step 6 and its new packs in step
+5. The packs it inherits were listed by `m_before`, which was the pointer's
+value when read, so they were already stored; nothing is deleted (A1). For (b),
+the response is built in step 8, which runs only after step 7 succeeded, and
+`refs_after` in the published manifest is the workspace state from which git
+produced its `ok` lines. A request that stops at step 3 relays git's output
+without publishing. In that case every `ok` git reported belongs to a command
+that asked for the value the ref already had, because a command that changes a
+ref and is reported `ok` leaves the workspace different from `m_before`. Such a
+report is true of the state the request read in step 1, and that read is where
+the request takes effect.
+
+*Model:* (a) is the invariant `Fence`; (b) is part of the refinement `Refines`
+(the abstract specification allows a response to report only the outcome fixed
+when the push took effect) and is also stated directly as `NoSilentDrop`.
+The check `relayed-ok` confirms that the model reaches the case of an `ok`
+that is relayed without a publication.
 
 *Pointer integrity:* the pointer object holds a manifest *digest*, not inline
 state. A1+A2 mean a successful pointer write is durable and read-after-write
@@ -319,9 +387,11 @@ wrong-but-plausible history). The protocol never trusts an unresolvable or
 mismatched pointer.
 
 Corollary (crash safety): if the process crashes between any two steps, no
-client has observed success unless step 7 completed; an incomplete push leaves
+client has been told `ok` unless step 7 completed; an incomplete push leaves
 orphan packs and an unchanged pointer — wasted bytes, never a visible-but-lost
-ref change.
+ref change. The converse does not hold and is not claimed: a push can be
+published and the client can still receive an error, for example when the
+response is lost. The client then learns the outcome by reading the refs.
 
 ### Theorem 2 (Manifest Reconstruction)
 
@@ -330,24 +400,33 @@ ref change.
 > missing. (The named pack set is a *superset* of that reachable closure; see
 > the remark on force-push/delete below.)
 
-**Proof.** By the push order, `d` is published (step 7) only after all packs in
-`manifest(d).packs` are durably written (step 2, before step 6). By A2 a reader
-that resolves `d` (step 1) can GET every pack in `manifest(d).packs` (step 3).
-By A1 + content-addressing, each pack's bytes are exactly those written, and any
+**Argument.** By Theorem 1(a) every pack in `manifest(d).packs` is stored, and
+by A2 a reader that resolves `d` can GET each of them. By A1 +
+content-addressing, each pack's bytes are exactly those written, and any
 deviation is detected by digest. Git's `index-pack` over a complete, verified
 pack set reconstructs the object graph (trusted upstream, §Non-Goals; reproducible
 against a pinned minimum `git` ≥ 2.31, the first release with `git index-pack
 --fsck-objects` defaults relied on here). It remains
 to show `manifest(d).packs` *covers* the reachable closure of `m.refs`. By
-induction on the push chain: the empty repo's manifest names ∅ and refs ∅
-(covered vacuously). A normal step sets
-`m_after.packs = m_before.packs ∪ keys(O)` where `O` is every object this push
-introduced; and `m_after.refs` only points at objects in `m_before.refs`'
-closure (unchanged or deleted refs) or in `O` (new or force-moved refs). A
-compaction step instead feeds every `m_after.refs` tip to `git pack-objects
---revs` with no negative revisions, then names only the resulting bounded pack
-set. The normal case preserves coverage by induction; the compaction case
-re-establishes coverage directly from the complete post-push ref closure. ∎
+induction on the sequence of publications: the empty repo's manifest names ∅ and
+refs ∅ (covered vacuously). A normal step sets
+`m_after.packs = m_before.packs ∪ keys(O)` where `O` holds every object
+reachable from `refs_after` that is not reachable from `m_before.refs`, so an
+object reachable from `refs_after` is either in `O` or covered by the induction
+hypothesis. A compaction step instead feeds every `refs_after` tip to
+`git pack-objects --revs` with no negative revisions, then names only the
+resulting bounded pack set. The normal case preserves coverage by induction; the
+compaction case re-establishes coverage directly from the complete post-push ref
+closure. The induction applies to `m_before` because the conditional write
+succeeds only if `m_before` is still the pointer's value (Theorem 3).
+
+The step "`O` holds every object reachable from `refs_after` and not from
+`m_before.refs`" requires those objects to be present in the workspace. That is
+part of the contract G1: `receive-pack` refuses a ref update whose new value is
+not fully connected.
+
+*Model:* the invariant `PublishedClosed`, over an object graph in which one
+object refers to another, so that a pack can lack an ancestor.
 
 **Remark (force-push, delete, and GC).** Coverage is a *superset*, not equality,
 and that is the correct invariant. A delete-ref drops a key from `m.refs`; a
@@ -360,34 +439,64 @@ a replacement manifest that normally has fewer packs. At the hard cap, an
 equal-count replacement is also valid when it incorporates the newly reachable
 objects while remaining within the bound. The old immutable objects are not
 deleted, so readers holding an earlier manifest remain valid. Physical
-object-store deletion remains a separate retention concern outside this proof
+object-store deletion remains a separate retention concern outside this
 boundary.
 
 ### Theorem 3 (Linearizable Refs / No Lost Update)
 
-> If two ref-changing pushes `p₁`, `p₂` execute concurrently, the published
-> history of `M_R` contains both effects in some serial order, or rejects one;
-> neither silently overwrites the other.
+> Every behavior of the protocol is a behavior of the atomic ref database
+> `GitRefDB` under the mapping that reads the database state from the manifest
+> the pointer names. In particular: each change of the published refs applies
+> commands of one push, each applied command names as its old value the value
+> the ref held immediately before the change, and a push whose conditional
+> write fails changes nothing.
 
-**Proof.** Both read the pointer (step 3) and CAS predicated on the ETag they
-read (step 7). Suppose both read ETag `e`. By A3 at most one CAS predicated on
-`e` succeeds; WLOG `p₁` succeeds, `M_R` advances to `e′`. `p₂`'s CAS predicated
-on `e` then fails (412): `p₂` re-reads (now `e′`, `d_after(p₁)`), re-validates Δ
-against `p₁`'s published refs (step 4), and either composes onto `p₁`'s state or
-is rejected non-ff. `p₂` never writes `M_R` while predicated on the stale `e`.
-By A3's linearizability, the successful CAS sequence is a single total order;
-each push's `m_after` is computed from its immediate predecessor's published
-state. Hence no update is lost and the published ref history is serial. The
-absence of an advisory lock changes only *efficiency under contention* (a loser
-may do wasted indexing before its 412), not correctness. ∎
+**Argument.** A request observes the pointer once, in step 1, and every later
+step works from that observation: git validates each command against the refs
+hydrated from `m_before`, and the conditional write in step 7 is predicated on
+the ETag `e` read in step 1. By A3 the write succeeds only if the pointer's
+current ETag is `e`. Under the ETag assumption E1 (§Mechanized Verification)
+that implies the pointer still holds `d_before`, so at the instant of the
+write the published refs are exactly the refs git validated against. The whole
+push therefore takes effect at that instant as one step of the atomic database:
+the applied commands have the right old values, and the refs they did not touch
+keep their published values. A request whose write fails publishes nothing and
+is answered with a conflict. The default-branch setter (§Default-branch
+management) follows the same discipline and is one further kind of atomic step.
 
-The mechanized model makes "no update is lost" concrete in checked forms over
-**real ref values**: the published manifests form a chain with no two sharing a
-parent (`Inv_NoFork` — a shared parent *is* a lost update); an installed push's
-committed ref value equals the value it proposed (`Inv_RefEffectApplied` — your
-write is what lands); each install is derived from the pointer it actually read
-(`Inv_RefDerivedFromParent` — never built on superseded state). Removing the CAS
-guard makes the model fork; that is the precise sense in which A3 is load-bearing.
+The comparison in step 7 is on the ETag, which may be a function of the pointer
+body alone. That is sufficient. If the pointer's body returns to an earlier
+value, the manifest it names is the same manifest, with the same refs, HEAD and
+packs, so a push computed from the earlier observation is also correct against
+the current state. Because a manifest records its predecessor, a body in fact
+never recurs (the Lean theorem `pointer_depth_eq_writes`), and a successful
+write implies that no other write that changed the pointer happened since the
+read (`cas_sees_no_intervening_write`; the Lean model omits the default-branch
+setter, whose same-value write rewrites the same body and so preserves the
+argument of the previous paragraph).
+
+*Model:* the temporal property `Refines`. Removing the CAS guard, predicating
+the write on a later observation than the one the workspace was built from, a
+store whose ETag does not distinguish bodies, and sending the response before
+the write each violate it.
+
+### Theorem 4 (Authorized Publication)
+
+> A request reaches step 4 only if the push policy accepted its command list
+> and `receive-pack` changed at least one ref. A request that is answered from
+> git's output without a publication reported `ok` only for commands that
+> asked for no change.
+
+**Argument.** Step 3 continues to step 4 only if the workspace refs differ from
+`m_before.refs`. By G1 `receive-pack` changes a ref only after the pre-receive
+hook accepted the command list, and the hook accepts only what the push policy
+accepts. The second sentence restates the observation used for Theorem 1(b): a
+command that changes a ref and is reported `ok` changes the workspace.
+
+*Model:* the invariants `PublishIsAuthorizedChange` and `NoSilentDrop`. Both
+fail for the rule this protocol used before (publish when git exits 0 and
+reports no `ng`), which the model keeps as the seeded error
+`Decision = "legacy"`.
 
 ## Conformance (Admitting a Backend for A3)
 
@@ -509,16 +618,38 @@ transfer:
   `CasError::Conflict { winner_manifest, winner_manifest_key }`. The variant is
   distinct from `Backend(StoreError)` so `?`-bubbling cannot turn 412 into 500.
   There is no in-handler retry: the loser's receive-pack output was derived
-  against a now-superseded parent, so reusing it would change the TLA action
-  and break `Inv_RefDerivedFromParent`. The client re-pushes, which re-hydrates
-  against the advanced state — that is the only safe retry, and `git` itself
-  drives it.
-- **kind:30618 derived after CAS.** Emission is conditional on
-  `manifest_changed = (parent_digest != committed_digest)` — `Manifest::
-  canonical_bytes` is deterministic, so equal published state ⇒ equal digest by
-  construction (no-op pushes pay no 30618 cost). The event is built by
-  `manifest_event::build_ref_state_event` from `CasSuccess.manifest` — the
-  values that *physically landed* via CAS, by `Inv_RefEffectApplied`. The event
+  against a now-superseded parent, so nothing computed from it may be
+  published (the seeded error `stale-base` is that mistake). The client
+  re-pushes, which re-hydrates against the advanced state — that is the only
+  safe retry, and `git` itself drives it.
+- **Publication decided from observed refs.** `observe_push` takes the snapshot
+  of the workspace after `receive-pack` (`snapshot_workspace`) and passes it,
+  with the hydrated parent refs and git's exit status, to `push_disposition`,
+  which returns `RelayOnly`, `Publish` or `Abort` exactly as §Push step 3
+  prescribes. `finalize_push` calls `cas_publish` only for `Publish` and hands
+  it the same snapshot, so the refs that are compared are the refs that are
+  published. The snapshot parser fails closed: output it cannot read is an
+  error, never an empty or partial ref set. The table-driven test
+  `push_is_published_exactly_when_receive_pack_changed_refs` runs real `git`
+  through the production `run_git_at` and `observe_push` for a request with no
+  commands, a declined push with and without a status report, an accepted push,
+  a command that asks for the value a ref already has, a push in which one ref
+  is updated and another refused for its old value, and a push that creates
+  two refs whose names conflict, of which git creates one and refuses the
+  other. Which of the two git creates differs between git versions; the test
+  accepts either and requires that each ref is in the snapshot exactly when
+  git reported `ok` for it. The test is Unix-only because its hook fixture
+  sets file modes. Two
+  tests cover `finalize_push` itself and need Postgres and an object store:
+  `finalize_push_publishes_nothing_when_receive_pack_changed_no_ref` checks
+  that an unchanged workspace leaves the pointer unwritten and stores no
+  kind:30618 event, and `e2e_git::git_partial_push_publishes_accepted_refs`
+  drives a partially refused push through a live relay.
+- **kind:30618 derived after CAS.** `cas_publish` is reached only for a push
+  that changed refs, so every successful publication is followed by one
+  kind:30618 event and a push that changed nothing emits none. The event is
+  built by `manifest_event::build_ref_state_event` from `CasSuccess.manifest` —
+  the values that were written by the CAS. The event
   is relay-signed (the relay is authoritative for ref state of repos it hosts);
   the pusher's pubkey rides in a `p` tag (buzz extension; NIP-34 does not
   define one). 30618 emission happens after `cas_publish` returns `Ok` and
@@ -526,6 +657,27 @@ transfer:
   consequence of a committed CAS, never the commit itself. A failed 30618
   insert is non-fatal: the push remains durable in the object store, and the
   next read/push surfaces the committed state from the manifest.
+- **kind:30618 order follows the manifest chain.** kind:30618 events are
+  stored side by side, and readers take the one with the greatest
+  `created_at` (lowest id on a tie). Stamping each event with the emitting
+  instance's clock let an older state win: two pushes in one second tie, and a
+  later push on a slower clock sorts first. Each published manifest therefore
+  carries `published_at`, strictly greater than its parent's (`now + 1` after
+  an unstamped parent, such as the announce-time seed), and the derived event
+  uses it as `created_at`. Since the manifests form a chain under CAS, the
+  newest event is the newest manifest regardless of which instance emits it
+  or when. The field is omitted when absent, so the shared empty seed and
+  manifests written before the field existed keep their digests. The argument
+  for a manifest whose parent carries no stamp rests on an assumption about
+  clocks; see "Order of ref-state events" in §Mechanized Verification.
+- **A landed CAS stands when the serving lease lapses after it.** The pointer
+  CAS runs under the community serving-write lease, and the lease check after
+  the operation can fail because the heartbeat missed a renewal, not only
+  because deletion has fenced the community. The CAS cannot be undone at that
+  point, so `finalize_push` (and the default-branch setter) keeps its outcome
+  instead of answering 503, and lets the lease-guarded 30618 insert decide
+  whether publication may continue. Lease loss *during* the operation still
+  drops it and answers 503; whether the pointer PUT landed is then unknown.
 - **No advisory lock.** Writer serialization is the CAS. The per-repo mutex the
   legacy persistent-disk path used would only have spanned a single process and
   is incompatible with the multi-instance v1 architecture (§Scope). Dropping it
@@ -533,30 +685,33 @@ transfer:
   hydrate + run receive-pack, and the CAS losers' work is discarded (an
   accepted v1 tradeoff named in §Scope).
 
-**Current code status (verified provenance).** The full S3-CAS implementation
-exists in code at PR #726's tip (`crates/buzz-relay/src/api/git/`), with the
-relay lib green, clippy `--tests -D warnings` clean, fmt clean, and the live
-MinIO e2e — clone/push/fetch/force-push roundtrip + N-way concurrent-push
-no-fork — green on the assembled tip. (Line numbers below are pinned at
-landing time; reviewers checking after subsequent refactors should consult
-symbol search, not line counts.)
+**Code correspondence.** The implementation is in
+`crates/buzz-relay/src/api/git/`. The table names the symbol for each element
+of the specification; symbols are given without line numbers because those
+drift.
 
 | Spec element | Code |
 |---|---|
-| `Manifest { version, head, refs, packs, parent }` + `canonical_bytes` | `manifest.rs` |
+| `Manifest { version, head, refs, packs, parent, published_at }` + `canonical_bytes` | `manifest.rs` |
+| `next_published_at` (stamp strictly after the parent's) | `manifest.rs` |
 | `Manifest::validate()` (pre-CAS rejection: refs/HEAD/OIDs/parent-shape) | `manifest.rs` |
 | `GitStore::{put_pack, put_manifest, put_pointer}` (create-only + CAS) | `store.rs` |
 | `run_conformance_probe` (A1/A3 fail-closed startup gate) | `store.rs` + `main.rs` |
-| `hydrate_for_read` / `hydrate_for_write` | `hydrate.rs` |
+| §Push step 1: `hydrate_for_write` → `(HydratedRepo, ParentState)` | `hydrate.rs` |
+| §Read: `hydrate_for_read` | `hydrate.rs` |
 | Bounded digest-keyed pack/index cache and single-flight population | `pack_cache.rs` |
+| §Push step 2: `receive_pack`, `install_hook`, the policy callback | `transport.rs`, `hook.rs`, `policy.rs` |
+| §Push step 3: `snapshot_workspace`, `push_disposition`, `observe_push` | `cas_publish.rs`, `transport.rs` |
+| §Push steps 4–7: `cas_publish(.., &parent_state, &workspace, ..)` | `cas_publish.rs` |
 | Proactive full-closure pack compaction before manifest capacity | `cas_publish.rs` |
-| `ParentState { if_match, parent_digest, parent }` + `from_loaded`/`fresh` | `cas_publish.rs:154` |
-| `cas_publish(.., &parent_state) -> Result<CasSuccess, CasError>` | `cas_publish.rs:410` |
-| `CasError::Conflict { winner_manifest, winner_manifest_key }` (typed 412) | `cas_publish.rs:92` |
+| `ParentState { if_match, parent_digest, parent }` + `from_loaded`/`fresh` | `cas_publish.rs` |
+| `CasError::Conflict { winner_manifest, winner_manifest_key }` (typed 412) | `cas_publish.rs` |
 | `build_ref_state_event(&RefStateInputs, &Keys)` (NIP-34 kind:30618) | `manifest_event.rs` |
-| `PushContext { pack, parent_state, repo_handle, … }` | `transport.rs:643` |
-| `finalize_push(state, ctx) -> Response` — **the seam** | `transport.rs:674` |
-| `build_git_response` (sole `Body::from(stdout)` site) | `transport.rs:627` |
+| `PushContext { pack, parent_state, repo_handle, … }` | `transport.rs` |
+| §Push step 8: `finalize_push(state, ctx) -> Response` — **the seam** | `transport.rs` |
+| `build_git_response` (sole `Body::from(stdout)` site) | `transport.rs` |
+| Default-branch setter: `DefaultBranchSnapshot::set` | `settings.rs` |
+| `protect_landed`: a landed conditional write stands when the lease lapses after it | `buzz-deletion`; called from `transport.rs`, `settings.rs` |
 
 The push path reaches `build_git_response` *only* through `finalize_push`,
 which consumes a `PushContext`; the compiler enforces "no `PushContext` ⇒ no
@@ -571,90 +726,377 @@ announced."
 
 One named follow-up: a behavioral integration test for runtime ordering
 (publish-before-response) — currently enforced by `finalize_push` being a
-single sequential async fn (no detached `tokio::spawn`) — is the
-belt-and-suspenders item to add once a mockable-CAS seam exists. The
-mechanical no-fork claim is empirically gated by the live N-way
-concurrent-push e2e (`e2e_git::git_concurrent_push_one_wins_and_repo_recovers`).
+single sequential async fn (no detached `tokio::spawn`) — is the item to add
+once a mockable-CAS seam exists. The no-lost-update claim is exercised
+end-to-end by the live N-way concurrent-push test
+(`e2e_git::git_concurrent_push_one_wins_and_repo_recovers`), which needs
+Postgres and an object store.
 
 ## Mechanized Verification
 
-The safety theorems are model-checked, not only argued in prose. The companion
-TLA+ module `docs/spec/GitOnObjectStore.tla` models concurrent pushers racing to
-advance the manifest pointer, with the CAS action (`If-Match`) as the sole
-pointer writer — directly encoding axiom A3. Each push models a proposed ref
-value (`newVal`, the objectId it wants `main` to hold) and whether its ref
-snapshot reads succeed (`snapErr`); whether it *changes* refs is then **derived**
-(`DidChange == newVal ≠ value-in-the-manifest-it-read`), not a free boolean. The
-skip predicate is `MustPublish(p) == DidChange(p) \/ snapErr(p)` — "publish unless
-we *observed* no change," never "publish unless `b == a`" with failed reads
-compared equal. A `compacted` marker distinguishes normal delta-pack stages
-from stages whose own pack is the trusted full closure produced from every
-post-push ref tip.
+This section separates what is defined, what is assumed, what has been checked
+by a tool, what is supported by tests of the implementation, and what is only
+proposed. The TLC and Lean results can be reproduced with two commands:
+`docs/spec/check.sh` (TLC, pinned to version 1.7.4 by SHA-256; needs Java) and
+`lake build` in `docs/spec/lean` (Lean 4.33.1, no dependencies). Both run in CI
+when a file under `docs/spec/` changes. The Quint results are reproduced with
+the commands given in "Results checked with Quint"; they are not run in CI.
 
-Crucially the model carries the **real ref value** per manifest (`refs[m]` = the
-objectId `main` holds in manifest `m`) and explicit **history** (`parent[m]`).
-This is what lets the invariants prove ref-*update* linearizability — that *your*
-ref write is what gets committed and survives — not merely pointer-id bookkeeping.
-TLC checks eight invariants (a finiteness constraint, `BoundedManifests`, caps published manifests at `MaxManifests` so the retry loop terminates):
+### Definitions
 
-| Invariant | Theorem | Statement |
-|---|---|---|
-| `Inv_Fence` | T1 | an obligated push's manifest is published before success is observed |
-| `Inv_ChangedPublished` | T1 | a ref-changing push is always published (fallible-snapshot bite) |
-| `Inv_Closed` | T2 | a normal manifest covers its parent's packs; a compacted manifest names its trusted full-closure pack |
-| `Inv_NoFork` | T3 | no two published manifests share a parent (a fork = a lost update) |
-| `Inv_RefEffectApplied` | T3 | an installed push's committed ref value equals the value it proposed |
-| `Inv_RefDerivedFromParent` | T3 | an install is derived from the pointer it read (no build on superseded state) |
-| `Inv_ParentPublished` | T2/T3 | every published manifest's parent is published (grounded history) |
-| `Inv_PointerPublished` | T1 | the pointer always names a published manifest |
+Two TLA+ modules define the claim.
 
-```
-$ tlc GitOnObjectStore.tla -config GitOnObjectStore.cfg
-Model checking completed. No error has been found.
-```
+`GitRefDB.tla` is the specification. It describes a database of refs and a HEAD
+with no object store and no concurrency control. A push is an invocation (the
+client submits commands, and it is recorded whether the push policy authorizes
+them), one atomic step in which a subset of the commands is applied, and a
+response. A command may be applied only if the push is authorized and only if
+its old value is the ref's current value. A command whose new value equals its
+old value can be applied; it confirms the value of the ref and changes nothing. A
+response may report the true per-ref outcome, report nothing, or be an error;
+it may not report an outcome that did not occur. The module also records which
+actor the published state is attributed to, which stands for the pusher named
+in the kind:30618 event.
 
-**Every invariant is proven non-vacuous** by a mutation that trips it (each
-checked in isolation against each mutant). This is the discipline that catches
-"green but vacuous" specs:
+`GitOnObjectStore.tla` is the protocol of §Push together with a default-branch
+setter, a reader, and repository creation. Its state is the pointer, the
+manifest store, the pack store, and the local state of each request. A manifest
+is a record of refs, HEAD, packs and (optionally) predecessor. A pack is a set
+of objects, and objects refer to other objects, so reachability and closure are
+computed, not asserted. `receive-pack` is one step that chooses which commands
+to apply, subject to G1 below, and may exit abnormally after applying some.
 
-| Mutation | Trips |
+The correctness statement `Refines` says that every behavior of
+`GitOnObjectStore` is a behavior of `GitRefDB`, where the abstract database is
+read from the manifest the pointer names. The abstract outcome of a push is
+fixed at its conditional write, or, for a request that publishes nothing, at
+its read of the pointer. TLC checks this as a temporal property: every
+step of the protocol must be a step of the specification or leave the abstract
+state unchanged.
+
+### Assumptions
+
+The checked results hold under the following assumptions. None is verified
+here.
+
+- **A1–A3** (§Axioms): durable create-only writes, read-after-write, and a
+  linearizable conditional write on the pointer.
+- **E1 (ETag).** If the pointer's ETag equals the ETag a request read, the
+  pointer's body equals the body that request read. A store whose ETag changes
+  on every write satisfies E1. So does a store whose ETag is a digest of the
+  body, provided that digest does not collide on two pointer bodies that occur.
+  On S3 the ETag of such an object is an MD5 digest, and the body is the
+  hexadecimal SHA-256 digest of a manifest; E1 then asks that no two manifest
+  digests published for one repository have the same MD5.
+- **H1 (digests).** SHA-256 does not collide on the manifests and packs that
+  occur. The models identify a digest with the value it names.
+- **G1 (`git receive-pack`).** `receive-pack` changes a ref only by applying a
+  command the client submitted; only after the pre-receive hook accepted the
+  whole command list; only if the command's old value is the ref's current
+  value in the workspace; and only if every object reachable from the new value
+  is present. It may refuse any command and may exit abnormally after applying
+  some. The hook accepts exactly what the push policy accepts. This is git's
+  documented behavior, and the test named in §Implementation Correspondence
+  exercises the cases that matter here against the installed git, but git
+  itself is not verified.
+- **Policy.** Whether the push policy's decision is the right one is outside
+  these models. They record its answer as a boolean per push.
+
+### Results checked by TLC
+
+TLC explores every reachable state of a finite instance. The base instance has
+two concurrent pushing clients, two refs, the default-branch setter, repository
+creation, and compaction when a manifest lists two packs. The ETag is a
+function of the body and manifests do not record a predecessor. This is the
+weakest comparison a conforming store can provide (the write succeeds in the
+most situations), and it makes the state space finite without any bound on the
+number of pushes, so the base check covers behaviors of unbounded length. The
+other instances vary one dimension each.
+
+| Check | Instance | Distinct states | Result |
+|---|---|---|---|
+| `refdb` | the specification alone, one client; its stated consequences | 11,262 | pass |
+| `push` | base instance | 2,349,839 | pass |
+| `objects` | one client, two objects (one refers to the other), reader | 531,099 | pass |
+| `three-clients` | three clients, one ref | 91,039 | pass |
+| `stale-commands` | a client may name an old value other than the hydrated one | 43,314 | pass |
+| `parent-links` | manifests record their predecessor; at most 3 pointer writes | 1,329,939 | pass |
+| `version-etag` | ETag changes on every write; at most 3 pointer writes | 505,468 | pass |
+| `no-view` | base instance without the setter and without state identification | 6,773,286 | pass |
+
+Each passing check establishes, for its instance, `Refines` and the invariants
+`Fence`, `ReaderComplete`, `PublishedClosed`, `HeadPublished`, `NoSilentDrop`
+and `PublishIsAuthorizedChange`, and the action property `ParentIsPredecessor`
+(a pointer write that changes the manifest names the manifest it replaced,
+where predecessors are recorded). `ReaderComplete` constrains only `objects`,
+the instance with a reader. The whole suite takes about three minutes on a
+16-core machine and about ten minutes on a GitHub-hosted runner.
+
+The instances identify states that differ only in stored objects that nothing
+reads (a TLC `VIEW`), and treat clients as interchangeable (`SYMMETRY`). The
+argument that the first loses nothing is given in `MCGitOnObjectStore.tla`, and
+`no-view` repeats the check without it.
+
+### Seeded design errors
+
+A property that cannot fail constrains nothing. Each row below changes the
+design in one way, and `check.sh` requires TLC to report a violation of the
+named property; the suite fails if a seeded error goes undetected. The view is
+not used for these runs.
+
+| Seeded error | Violates |
 |---|---|
-| skip predicate `DidChange /\ ~snapErr` (ref change + both snapshots fail → silently skipped) | `Inv_ChangedPublished` |
-| a normal stage uses `packs[m] = {m}` without the full-closure marker | `Inv_Closed` |
-| drop CAS guard (two pushers install off one parent — a fork) | `Inv_NoFork` |
-| install records the *read* ref value, not the push's proposal (effect dropped) | `Inv_RefEffectApplied` |
-| record parent as root instead of the pointer actually read | `Inv_RefDerivedFromParent` (+ `Inv_NoFork`) |
+| publish when git exits 0 and reports no `ng` (the original rule): a declined or empty push is published | `PublishIsAuthorizedChange` |
+| the original rule, mixed outcome: the client is told `ok` for a ref that is not published | `NoSilentDrop` |
+| the original rule, git exits abnormally after applying a command | `NoSilentDrop` |
+| the original rule, as a whole | `Refines` |
+| publish when git exits 0 and reports an `ok` or no `ng` (the status-report rule): a declined or empty push is published | `PublishIsAuthorizedChange` |
+| the status-report rule, git exits abnormally after applying a command | `NoSilentDrop` |
+| the status-report rule, as a whole | `Refines` |
+| no pre-receive hook | `PublishIsAuthorizedChange` |
+| pointer write without the condition | `Refines` |
+| condition taken from a later pointer read than the one the workspace was built from | `Refines`, `ParentIsPredecessor` |
+| ETag that does not distinguish bodies (against a push; against the setter) | `Refines` |
+| response sent before the pointer write | `Refines` |
+| pointer write before the uploads | `Fence` |
+| deletion of a pack that the current manifest does not list | `Fence`, `ReaderComplete` |
+| a delta push that drops the packs it inherits | `PublishedClosed` |
+| `receive-pack` without the connectivity check | `PublishedClosed` |
 
-The unmarked `packs[m]={m}` and CAS-guard mutations are the two core closure and
-serialization vacuity tests. The full-closure marker is only assigned by the
-compaction branch; reusing it for a normal delta stage would make the closure
-claim vacuous, so the model explicitly clears stale markers when manifest ids
-are reused.
-The ref-value mutations (effect-dropped, wrong-parent) are what close the gap from
-"pointer CAS serializes" to "ref *updates* are linearizable" — the user-visible
-theorem the title promises. (A weaker mutation, `MustPublish == DidChange` alone,
-does *not* break safety — it over-publishes, safe-but-wasteful; noted so the
-mutation set is honest about which mutations are true safety regressions.
-`Inv_ChangedPublished` and `Inv_Fence` look redundant but are not: see the .tla
-comment — mutating the `MustPublish` operator weakens `Inv_Fence`'s own predicate,
-so the `DidChange`-predicated `Inv_ChangedPublished` is the one that stays
-load-bearing under exactly that mutation.)
+The first seven rows concern the two rules the relay used before the present
+one. Both decided from git's exit status and the lines of its status report.
+The original rule treated any `ng` line as "nothing happened". The status-report
+rule repaired the mixed outcome by publishing whenever an `ok` line is present.
+Neither sees a status report from a client that did not negotiate one, and
+neither sees any line for a request without commands, so both publish in those
+cases. The model was written against what git can do and not against the status
+report, and for either rule it produces a counterexample of four states: the
+repository is created, a request arrives, `receive-pack` declines it, and the
+request is on the publish path, where the published state would be attributed
+to the caller.
 
-The model is checked at `Pushers = {p1,p2,p3}`, `MaxManifests = 3`, under the
-`BoundedManifests` constraint (`|published| ≤ MaxManifests`) — required because
-the retry loop otherwise lets pushers churn fresh manifest ids and ref values
-without bound, so the model is *finite-state only with the bound*. Three
-concurrent pushers exercise every CAS race relevant to these invariants (a fourth
-adds no qualitatively new interleaving). This is a *bounded* model check, not an
-unbounded proof: it exhaustively verifies the invariants within the bound and is mutation-
-shown non-vacuous, which is the standard claim for a TLC-checked safety spec.
+One further check, `relayed-ok`, asserts something that is not required (that a
+request answered without a publication never carries an `ok`) and must be
+violated by the protocol as specified. It shows that the model reaches the case
+of a command that asks for no change, which Theorem 1(b) and Theorem 4 make an
+exception for.
+
+### Results proved in Lean
+
+`docs/spec/lean/GitPointer.lean` proves the pointer discipline for arbitrary
+types of clients, refs, objects and packs, with no finiteness assumption. The
+model there has four steps (read the pointer and stage a successor, upload,
+conditional write, abort) and arbitrary relations for which ref states may
+follow which, which objects a ref state reaches, and which objects a pack
+holds. Its one hypothesis about the store is E1. For every reachable state it
+proves:
+
+- `fence`: the manifest the pointer names and the packs it lists are stored
+  (Theorem 1a).
+- `closed`: those packs contain every object reachable from the manifest's
+  refs, derived from the three rules for composing a pack list (Theorem 2).
+- `pointer_step_legal`: every step leaves the pointer unchanged or replaces it
+  with a manifest computed as a legal successor of the value it replaces
+  (the pointer part of Theorem 3).
+- `pointer_depth_eq_writes` and `cas_sees_no_intervening_write`: a pointer body
+  never recurs, and a successful conditional write implies that no other write
+  that changed the pointer happened since the read (the Lean model omits the
+  default-branch setter, whose same-value write rewrites the same body and so
+  preserves the argument of the previous paragraph).
+
+`write_is_possible` shows that a successful write is reachable, so the results
+do not hold vacuously. The proofs use no axioms beyond Lean's standard three
+(`propext`, `Classical.choice`, `Quot.sound`).
+
+The Lean model is narrower than the TLA+ model. It does not contain the publish
+decision, the responses to clients, the default-branch setter, the reader, or
+`receive-pack`; "legal successor" is a parameter. The two models are related by
+reading, not by a mechanical link.
+
+### Results checked with Quint
+
+The TLA+ and Lean models contain neither the serving-write lease nor the
+kind:30618 events. `docs/spec/GitPushPath.qnt` is a Quint model of the push
+path that contains both. Two pushers each fetch the ref advertisement and then
+send a receive-pack request, which hydrates from whatever pointer is current
+when it runs. A request names at most two of three refs (which include the
+directory/file pair `feature` and `feature/x`), may name none, and may come
+from a client that did not negotiate a status report. The publish decision,
+the lease and the event timestamps follow `finalize_push`. Each relay instance
+reads a clock that may run one second ahead. The invariants are stated over
+what clients observe:
+
+| Invariant | Statement |
+|---|---|
+| `noFalseSuccess` | a ref the client printed as `ok` reached the published pointer |
+| `noFalseFailure` | a ref the client was told failed did not reach the pointer |
+| `refStateMatchesPointer` | once pushes settle, the kind:30618 event that readers select matches the pointer |
+| `publicationChangesRefs` | every published manifest differs in its refs from the one it replaced |
+
+The module `fixed` is the implementation: the publish decision of §Push step
+3, a landed conditional write kept when the lease lapses after it, and events
+stamped with the manifest's `published_at`. The other modules each restore one
+earlier behavior, so that a counterexample is attributed to one defect.
+
+| Module | Restores | Result |
+|---|---|---|
+| `fixed` | nothing | all four invariants hold |
+| `partialBugOnly` | the original publish rule | violates `noFalseSuccess` and `publicationChangesRefs` |
+| `reportRuleOnly` | the status-report publish rule | violates `publicationChangesRefs`; `noFalseSuccess` and `noFalseFailure` hold |
+| `leaseBugOnly` | a landed write reported as a failure when the lease lapses | violates `noFalseFailure` |
+| `timestampBugOnly` | events stamped with the emitting instance's clock | violates `refStateMatchesPointer` |
+| `current` | all three original behaviors | violates `safety` |
+
+The results were obtained with Quint 0.33.0 in two ways. Random simulation
+explores runs of at most 14 steps:
+
+```
+quint run docs/spec/GitPushPath.qnt --main fixed --invariant safety \
+  --max-steps 14 --max-samples 2000000 --seed 0x1
+```
+
+For `fixed` it reports no violation of `safety` (the conjunction of the four
+invariants) in 2,000,000 runs. For `reportRuleOnly`, the same command with one
+invariant at a time reports no violation of `noFalseSuccess`, `noFalseFailure`
+or `refStateMatchesPointer` in 2,000,000 runs each, and a counterexample for
+`publicationChangesRefs`. Each of the other modules produces a counterexample
+for the invariant named in the table. Simulation samples runs; the absence of a
+violation is evidence, not a proof.
+
+The second way is a bounded symbolic check, which considers every run up to
+the bound:
+
+```
+quint verify docs/spec/GitPushPath.qnt --main fixed --invariant safety \
+  --max-steps 8
+```
+
+With Apalache 0.62.1 this reports no violation for `fixed` (81 seconds), and
+the same command for `reportRuleOnly` with `publicationChangesRefs` returns a
+counterexample. A push that publishes takes four steps (advertisement,
+receive-pack, conditional write, event), so the bound of eight covers every
+interleaving of the two pushes in which the clock does not advance. Runs in
+which it advances between steps of both pushes are longer, and are covered by
+simulation only.
+
+A `reportRuleOnly` counterexample is a request that changes no ref and whose
+visible report has no `ng` line: a request with no commands, or a declined push
+from a client that did not negotiate a status report. The status-report rule
+publishes it. In the Quint model the published refs equal
+their predecessor's, so the client-facing invariants still hold; what the
+publication adds is a pointer write and a kind:30618 event that names the
+caller as the pusher. The TLA+ model, which has the push policy, reports the
+same behavior as a violation of `PublishIsAuthorizedChange` (the seeded error
+`report-unauthorized`).
+
+### Evidence about the implementation
+
+The models are about the design. Three things connect them to the code. The
+publish decision is a pure function, `push_disposition`, whose three outcomes
+are the three branches of the model's `Disposition`, and a unit test covers its
+cases. The test `push_is_published_exactly_when_receive_pack_changed_refs` runs
+the production subprocess path against real git for seven ways a push can
+end, and fails if the decision is changed to depend on the exit status alone.
+The test `finalize_push_publishes_nothing_when_receive_pack_changed_no_ref`
+calls `finalize_push` with an unchanged workspace against Postgres and an
+object store, and fails in the same way under that change. The remaining
+correspondence (one pointer observation per request, uploads before the
+conditional write, the response built only in `finalize_push`) is by the
+structure described in §Implementation Correspondence and by the other
+storage-backed tests.
+
+The storage-backed tests of `finalize_push` and `e2e_git` are marked ignored
+and are not selected by any CI job at the time of writing, so they are evidence
+only when someone runs them. The seven-case test needs no services and runs in
+the Unix unit-test jobs.
+
+### Assumptions and limitations
+
+- The TLC results are exhaustive for the instances listed and say nothing
+  directly about larger ones. Two clients with two objects and two refs is
+  beyond what the suite can check in reasonable time. The Lean results remove
+  the bound for the pointer discipline only.
+- Hydration is one atomic step in the push model. The reader process covers
+  reads that are interleaved with writes.
+- Only safety is covered. Nothing here shows that a push eventually succeeds.
+- Deletion of stored objects is modeled only as a seeded error. A garbage
+  collector would need its own model, with the reader and the upload-then-write
+  window as the cases it must respect.
+- The TLA+ and Lean models do not include the relay's database, the
+  serving-write lease, request authentication, or the kind:30618 event stream.
+  The Quint model includes the lease and the events, with the bounds stated in
+  its section, and is not connected to the other two by any mechanical link.
+
+### Order of ref-state events
+
+Two pushes can win their conditional writes in the order A, B and then store
+their kind:30618 events in the order B, A, because event storage happens after
+the write and nothing orders the two requests. When each event carried the
+time at which its relay instance built it, a consumer that reads ref state from
+the newest event could then see A's refs although the pointer holds B's. Two
+pushes within one second, or a later push handled by an instance with a slower
+clock, had the same effect.
+
+The implementation removes the dependence on storage order and on the emitting
+clock. Every manifest written by a push or by the default-branch setter carries
+`published_at`, computed by `next_published_at` as the later of the current
+time and one second after the parent's stamp, and the derived event uses that
+value as its `created_at`. Stamps therefore increase strictly along the chain
+of manifests, and the chain is totally ordered by the conditional write
+(Theorem 3), so the event with the greatest `created_at` is the event of the
+manifest the pointer names. `refStateMatchesPointer` in the Quint model checks
+this for stamped manifests, and `timestampBugOnly` shows the earlier behavior
+violating it.
+
+**Assumption C1 (clocks, unstamped parent).** Two manifests carry no stamp: the
+empty manifest written when a repository is announced, whose bytes are shared
+by all repositories, and any manifest written before the field existed. The
+event of such a manifest was stamped with the clock of the instance that
+emitted it. Its successor takes the current time plus one second on the
+instance that writes it. The successor's event is selected over the
+parent's only if that value exceeds the parent event's `created_at`. This
+holds when one instance handles both, and otherwise when the writing
+instance's clock is not behind the other's by more than the time that passed
+between the two events. C1 states that it holds. It concerns one write per
+repository (the first after creation, or the first after the field was
+introduced); every later manifest has a stamped parent. C1 is established by
+reading the code. It is not modeled: the Quint model starts from a stamped
+manifest. If C1 fails, readers of the newest event see the parent's refs until
+the next push, and the pointer is unaffected.
+
+### Proposed extensions
+
+- Bind publication to the policy decision itself: have the policy endpoint
+  record, per request, the command list it approved, and have step 3 require
+  that the observed ref changes are a subset of an approved list. This would
+  replace assumption G1's clause about the hook with a check in the relay.
+- Remove assumption C1, for example by having the first push after an
+  unstamped manifest read the `created_at` of the stored event and exceed it,
+  and model the unstamped case in Quint.
+- Run the Quint checks in CI with a pinned Quint and Apalache.
+- Run the storage-backed `finalize_push` tests in CI. Their fixture applies the
+  migrations itself, which the CI database (built from the desired-state
+  schema) does not expect, so the fixture needs the schema-mode switch the
+  other storage-backed suites use.
+- A mechanical link between the Lean model and the TLA+ model, or a proof of
+  the full refinement for unbounded parameters.
+
+### Names used by earlier revisions
+
+Code comments and a database migration cite invariant names from an earlier
+model. They are kept as aliases in `GitOnObjectStore.tla`: `Inv_NoFork` and
+`Inv_RefEffectApplied` stand for `Refines`, `Inv_RefDerivedFromParent` for
+`ParentIsPredecessor`, and `Inv_Closed` for `PublishedClosed`.
 
 ## Summary
 
-| Property | Status | Discharged by |
+| Property | Evidence | Relative to |
 |---|---|---|
-| Durability-ordering (T1) | Proved | Fence + A1, A2 |
-| Manifest reconstruction (T2) | Proved | Content-addressing + A1, A2; git upstream |
-| No lost update (T3) | Proved | A3 (no advisory lock needed) |
+| Durability-ordering (T1) | TLC, finite instances; Lean (`fence`), unbounded | A1, A2 |
+| Manifest reconstruction (T2) | TLC, finite instances; Lean (`closed`), unbounded | A1, A2, G1; git upstream |
+| Linearizable refs (T3) | TLC refinement, finite instances; Lean (`pointer_step_legal`), unbounded, pointer discipline only | A3, E1, H1, G1 |
+| Authorized publication (T4) | TLC, finite instances | G1; policy correctness not covered |
+| Landed write reported as landed; ref-state events ordered as the manifests | Quint, bounded | C1 |
+| Model matches the code | Tests and review | — |
 | A1/A2/A3 hold on backend | Empirical | Conformance probe (gate) |
 | Liveness / latency | Empirical | Benchmark (out of scope) |
diff --git a/docs/spec/.gitignore b/docs/spec/.gitignore
index 56d400a914..c2f49eef1c 100644
--- a/docs/spec/.gitignore
+++ b/docs/spec/.gitignore
@@ -1,5 +1,5 @@
-# TLC model-checker scratch output (fingerprint/state dirs, per-run).
-# Generated by `tlc` runs of MultiTenantRelay.tla; not part of the artifact.
+# TLC model-checker scratch output (fingerprint/state dirs, per-run), and the
+# TLC jar that check.sh downloads. Not part of the artifact.
 states/
 *.st
 *.fp
diff --git a/docs/spec/GitOnObjectStore.cfg b/docs/spec/GitOnObjectStore.cfg
deleted file mode 100644
index a94d49e198..0000000000
--- a/docs/spec/GitOnObjectStore.cfg
+++ /dev/null
@@ -1,10 +0,0 @@
-\* TLC model-check config for GitOnObjectStore.
-\* Run: tlc GitOnObjectStore.tla -config GitOnObjectStore.cfg
-SPECIFICATION Spec
-
-CONSTANTS
-    Pushers = {p1, p2, p3}
-    MaxManifests = 3
-
-INVARIANT Safety
-CONSTRAINT BoundedManifests
diff --git a/docs/spec/GitOnObjectStore.tla b/docs/spec/GitOnObjectStore.tla
index f5f71b357a..87917867f2 100644
--- a/docs/spec/GitOnObjectStore.tla
+++ b/docs/spec/GitOnObjectStore.tla
@@ -1,271 +1,580 @@
 -------------------------- MODULE GitOnObjectStore --------------------------
 (***************************************************************************)
-(* Formal model of git refs over object storage, accompanying             *)
-(* docs/git-on-object-storage.md.  Model-checks the three safety           *)
-(* properties under the conditional-write (CAS) axiom A3 by construction:  *)
-(* the PUT/If-Match action is the only writer of the pointer and is atomic *)
-(* per step (TLC interleaves at action granularity), modeling A3 directly. *)
+(* Git on object storage: the publication protocol of buzz-relay.          *)
 (*                                                                         *)
-(* Pushers race to advance a single manifest pointer holding a ref value.   *)
-(* We assert (see SAFETY PROPERTIES for the full set and per-invariant docs):*)
-(*   T1  fence: observed success => the obligated push is durably published  *)
-(*   T2  closure: a published manifest either covers its parent's packs or   *)
-(*       names a trusted full-closure compaction pack                         *)
-(*   T3  ref linearizability: installs form a fork-free chain, each commits  *)
-(*       exactly the value it proposed, derived from the pointer it read     *)
-(* Each invariant is mutation-tested non-vacuous; see docs/ Mechanized §.    *)
+(* WHAT IS CHECKED                                                         *)
+(*                                                                         *)
+(*   1. Refinement.  Every behavior of this module is a behavior of        *)
+(*      GitRefDB (the atomic reference database) under the mapping at the  *)
+(*      end of the file.  This is linearizability of ref updates, plus:    *)
+(*      a client is told "ok" for a command only if that update was        *)
+(*      published or the command asked for the value the ref already had,  *)
+(*      a publication changes refs only on behalf of an authorized push,   *)
+(*      and a push that changes nothing publishes nothing.                 *)
+(*   2. Store invariants: the fence (the pointer never names a manifest or *)
+(*      pack that is not stored), reader completeness (a reader that has   *)
+(*      resolved the pointer can fetch everything it needs), and closure   *)
+(*      (the packs of a published manifest contain every object reachable  *)
+(*      from its refs).                                                    *)
+(*                                                                         *)
+(* HOW IT IS CHECKED                                                       *)
+(*                                                                         *)
+(*   docs/spec/check.sh runs TLC on this module in several configurations. *)
+(*   The protocol as specified must pass.  Each element of Faults, the two *)
+(*   earlier publish decisions ("legacy" and "report"), and the "constant" *)
+(*   ETag mode is a seeded design error; each must be rejected with the    *)
+(*   expected violation, and the script fails if one is not.               *)
+(*                                                                         *)
+(* MODELING DECISIONS                                                      *)
+(*                                                                         *)
+(*   - A digest is modeled by the value it names.  A manifest is a record  *)
+(*     and "its digest" is that record; a pack is a set of objects and     *)
+(*     "its digest" is that set.  This is the assumption that SHA-256 is   *)
+(*     injective on the values that occur.                                 *)
+(*   - The object store offers create-only writes for immutable keys and   *)
+(*     conditional overwrite for the pointer (axioms A1-A3 of the design   *)
+(*     document).  Nothing is ever deleted, except under the "gc" fault.   *)
+(*   - The pointer comparison.  With EtagMode = "content" and              *)
+(*     ParentLinks = FALSE the conditional write succeeds exactly when the *)
+(*     pointer names a manifest with the same refs, head and packs as the  *)
+(*     one that was read.  This is the weakest comparison any conforming   *)
+(*     store provides: a store whose ETag changes on every write, and a    *)
+(*     manifest that also records its predecessor, both make the write     *)
+(*     succeed in strictly fewer situations and change nothing else.       *)
+(*     Every behavior of those variants is therefore a behavior of this    *)
+(*     one, so the properties are checked here without a bound on the      *)
+(*     number of pushes, and the variants are checked directly with a      *)
+(*     bound (MaxWrites) as a cross-check of that argument.                *)
+(*   - git receive-pack is modeled by its contract (assumption G1): it     *)
+(*     changes a ref only by applying a submitted command whose old value  *)
+(*     matches and whose new object is connected, and only after the       *)
+(*     pre-receive hook accepted the command list.  It may additionally    *)
+(*     refuse any command (atomic pushes, directory/file conflicts, deny   *)
+(*     rules) and it may exit abnormally after applying some commands.     *)
+(*   - Hydration (pointer, manifest and packs) is one atomic read.  The    *)
+(*     reader process covers the non-atomic read path.                     *)
+(*   - Safety only.  No liveness property is stated or checked.            *)
 (***************************************************************************)
-EXTENDS Naturals, FiniteSets, Sequences
+EXTENDS Naturals, FiniteSets
 
-CONSTANTS Pushers,        \* set of concurrent pusher ids
-          MaxManifests    \* bound on distinct manifests (model finiteness)
+CONSTANTS
+    \* Shared with GitRefDB.
+    Clients, Refs, Oids, NoOid, DefaultHead, Absent,
+    NoCall, NoOut, NoCmd, NoResp, Error, NoEntry, Owner, Manager,
+    \* Object graph: ObjParents[o] is the set of objects that o refers to.
+    ObjParents,
+    NoManifest,     \* the "parent" of a manifest that has no predecessor
+    NoRead,         \* the reader has not resolved the pointer
+    CompactAt,      \* a publish compacts when its base lists this many packs
+    MaxWrites,      \* bound on pointer writes, where they are counted
+    \* Which background processes take part (see check.sh for the reason).
+    HasSetter, HasReader,
+    \* Design switches.
+    StaleClients,   \* may a client name an old value other than the hydrated one?
+    GitMayCrash,    \* may receive-pack exit non-zero?
+    ParentLinks,    \* does a manifest record its predecessor?
+    Decision,       \* "ground-truth" (implemented), or an earlier rule:
+                    \* "legacy" or "report"
+    EtagMode,       \* "content", "version", or "constant" (a broken store)
+    Faults          \* seeded design errors; {} for the protocol as specified
+
+ASSUME DefaultHead \in Refs
+ASSUME NoOid \notin Oids
+ASSUME ObjParents \in [Oids -> SUBSET Oids]
+ASSUME StaleClients \in BOOLEAN /\ ParentLinks \in BOOLEAN /\ GitMayCrash \in BOOLEAN
+ASSUME HasSetter \in BOOLEAN /\ HasReader \in BOOLEAN
+ASSUME Decision \in {"ground-truth", "legacy", "report"}
+ASSUME EtagMode \in {"content", "version", "constant"}
+ASSUME Faults \subseteq {"no-cas-guard", "stale-base", "drop-parent-packs",
+                         "cas-before-upload", "gc", "no-hook",
+                         "no-connectivity", "ack-before-cas"}
 
 VARIABLES
-    pointer,    \* current manifest id held by M_R (a natural; 0 = empty repo)
-    published,  \* set of manifest ids ever installed as pointer (durable history)
-    packs,      \* function: manifest id -> set of pack ids it names
-    pc,         \* pusher id -> control state
-    readEtag,   \* pusher id -> pointer value it last read (its CAS precondition)
-    staged,     \* pusher id -> manifest id it intends to install
-    parent,     \* manifest id -> the manifest id it was derived from (history)
-    refs,       \* manifest id -> objectId that this manifest binds the ref "main" to
-    compacted,  \* manifests whose own pack is a full closure of their refs
-    newVal,     \* pusher id -> objectId this push proposes for "main" (its effect)
-    snapErr,    \* pusher id -> did either ref-snapshot read fail? (BOOLEAN)
-    observed    \* set of pusher ids that have observed success (fence passed)
+    \* The object store.
+    pointer,   \* Absent, or [body |-> manifest, etag |-> ...]
+    mstore,    \* manifests stored (create-only)
+    pstore,    \* packs stored (create-only)
+    writes,    \* pointer writes so far (counted only where the count is observable)
+    \* One push request per client at a time.
+    pc,        \* "idle", "arrived", "relay", "publish", "uploaded", "abort", "answer"
+    base,      \* pointer value the workspace was hydrated from
+    call,      \* [cmds, mayPush] as submitted, or NoCall
+    stat,      \* per-ref status computed by git receive-pack
+    staged,    \* manifest this push will publish, or NoManifest
+    lin,       \* outcome fixed at the linearization point, or NoOut
+    resp,      \* what the client was last told
+    \* The default-branch setter.
+    spc,       \* "idle" or "staged"
+    sbase,     \* pointer value the setter read
+    starget,   \* branch it was asked to make the default
+    \* A reader (clone or fetch).
+    rd,        \* NoRead, or the manifest it resolved from the pointer
+    \* History.
+    credit     \* who the published state is attributed to
+vars == <<pointer, mstore, pstore, writes, pc, base, call, stat,
+          staged, lin, resp, spc, sbase, starget, rd, credit>>
 
-vars == <<pointer, published, packs, pc, readEtag, staged,
-          parent, refs, compacted, newVal, snapErr, observed>>
+-----------------------------------------------------------------------------
+\* Values
 
-\* We model a single ref, "main", whose value is an objectId in ObjIds. This is
-\* enough to exhibit ref-update linearizability: a lost update is the published
-\* value of "main" reverting or skipping a committed predecessor's value.
-\* (Dawn's point: prove ref VALUES survive, not just that effect tokens are
-\* monotone.) refs[m] is the value "main" holds in manifest m.
-ObjIds == 0..MaxManifests
+OidOrNone  == Oids \cup {NoOid}
+EmptyRefs  == [r \in Refs |-> NoOid]
+\* A command may name the same value as old and new.  git accepts such a
+\* command, reports "ok" for it, and changes nothing.
+Command    == [old : OidOrNone, new : OidOrNone]
+CommandSet == [Refs -> Command \cup {NoCmd}]
+NoReport   == [r \in Refs |-> "none"]
+Packs      == SUBSET Oids
 
-\* A push CHANGES refs iff the value it proposes differs from the value in the
-\* manifest it READ. This is now DERIVED from real ref state, not a free boolean.
-DidChange(p) == newVal[p] # refs[readEtag[p]]
+\* The command sets a client may submit against hydrated refs P.  A client
+\* computes its commands from an advertisement fetched by an earlier request,
+\* so the old values it names can be out of date.  receive-pack refuses such
+\* a command, which makes it indistinguishable from any other refused
+\* command; StaleClients = FALSE leaves them out to keep the two-client
+\* configuration small, and a one-client configuration checks them.
+ClientCommands(P) ==
+    IF StaleClients THEN CommandSet
+    ELSE {cs \in CommandSet : \A r \in Refs : cs[r] # NoCmd => cs[r].old = P[r]}
 
-ManifestIds == 0..MaxManifests
+Fault(f) == f \in Faults
 
-TypeOK ==
-    /\ pointer \in ManifestIds
-    /\ published \subseteq ManifestIds
-    /\ packs \in [ManifestIds -> SUBSET ManifestIds]
-    /\ pc \in [Pushers -> {"idle","staged","done","lost"}]
-    /\ readEtag \in [Pushers -> ManifestIds]
-    /\ staged \in [Pushers -> ManifestIds]
-    /\ parent \in [ManifestIds -> ManifestIds]
-    /\ refs \in [ManifestIds -> ObjIds]
-    /\ compacted \subseteq ManifestIds
-    /\ newVal \in [Pushers -> ObjIds]
-    /\ snapErr \in [Pushers -> BOOLEAN]
-    /\ observed \subseteq Pushers
+\* Objects reachable from a set of objects.
+RECURSIVE Closure(_)
+Closure(S) ==
+    LET T == S \cup UNION {ObjParents[o] : o \in S}
+    IN IF T = S THEN S ELSE Closure(T)
 
+Tips(refs)      == {refs[r] : r \in Refs} \ {NoOid}
+Reachable(refs) == Closure(Tips(refs))
+ObjectsOf(ps)   == UNION ps
+PackOf(objs)    == IF objs = {} THEN {} ELSE {objs}
+
+EmptyManifest ==
+    [refs |-> EmptyRefs, head |-> DefaultHead, packs |-> {}, parent |-> NoManifest]
+
+\* The ETag the store assigns to a pointer write.  "content" is what S3 and
+\* MinIO do for a simple PUT (the ETag is a function of the body); "version"
+\* is a store that issues a new ETag on every write; "constant" is a store
+\* whose ETag does not distinguish bodies, which violates axiom A3.
+EtagOf(body, n) ==
+    CASE EtagMode = "content"  -> body
+      [] EtagMode = "version"  -> n
+      [] EtagMode = "constant" -> "etag"
+
+\* Pointer writes are counted when the count is observable in the state: as
+\* a version ETag, or as the depth of the predecessor chain.  In those modes
+\* the state space is infinite and MaxWrites bounds the exploration.
+Counted    == EtagMode = "version" \/ ParentLinks
+NextWrites == IF Counted THEN writes + 1 ELSE writes
+Bounded    == writes <= MaxWrites
+
+Successor(b) == IF b = Absent \/ ~ParentLinks THEN NoManifest ELSE b.body
+
+BaseRefs(b)  == IF b = Absent THEN EmptyRefs ELSE b.body.refs
+BaseHead(b)  == IF b = Absent THEN DefaultHead ELSE b.body.head
+BasePacks(b) == IF b = Absent THEN {} ELSE b.body.packs
+
+\* cas_publish.rs, resolve_published_head: keep HEAD on its branch while that
+\* branch is published; otherwise prefer the conventional default, then any
+\* published branch; with no branch at all, leave HEAD where it was.
+PublishedHead(refs, h) ==
+    IF refs[h] # NoOid THEN h
+    ELSE IF refs[DefaultHead] # NoOid THEN DefaultHead
+    ELSE IF \E r \in Refs : refs[r] # NoOid
+         THEN CHOOSE r \in Refs : refs[r] # NoOid
+         ELSE h
+
+\* The conditional pointer write (store.rs, put_pointer).  A request based on
+\* an absent pointer uses If-None-Match: *; any other uses If-Match: <etag>.
+CasWouldWin(b) ==
+    \/ Fault("no-cas-guard")
+    \/ b = Absent /\ pointer = Absent
+    \/ b # Absent /\ pointer # Absent /\ pointer.etag = b.etag
+
+Publication(actor, m) == [actor |-> actor, refs |-> m.refs, head |-> m.head]
+
+-----------------------------------------------------------------------------
+\* git receive-pack and the publish decision
+
+\* Commands receive-pack is willing to apply, given the hydrated refs P and
+\* the objects available (hydrated packs plus the client's pack).
+ValidCmds(cmds, P, objs) ==
+    {r \in Refs :
+        /\ cmds[r] # NoCmd
+        /\ cmds[r].old = P[r]
+        /\ \/ cmds[r].new = NoOid
+           \/ Fault("no-connectivity")
+           \/ Closure({cmds[r].new}) \subseteq objs}
+
+\* The pre-receive hook is run only when there is at least one command, and
+\* then decides for the whole command list.
+HookPermits(cmds, may) ==
+    \/ Fault("no-hook")
+    \/ may
+    \/ \A r \in Refs : cmds[r] = NoCmd
+
+StatusOf(cmds, applied) ==
+    [r \in Refs |-> IF r \in applied THEN "ok"
+                    ELSE IF cmds[r] # NoCmd THEN "ng"
+                    ELSE "none"]
+
+\* The two rules transport.rs used earlier.  Both read the report-status
+\* stream, and a client that did not negotiate report-status produces no such
+\* stream, so neither an "ok" nor an "ng" line is seen for it.
+\*   legacy: publish when the process exited zero and the stream contains no
+\*   "ng" line.
+\*   report: publish when the process exited zero and the stream contains an
+\*   "ok" line or no "ng" line.
+SeenOk(wantsReport, st) == wantsReport /\ \E r \in Refs : st[r] = "ok"
+SeenNg(wantsReport, st) == wantsReport /\ \E r \in Refs : st[r] = "ng"
+
+LegacyOk(exitOk, wantsReport, st) == exitOk /\ ~SeenNg(wantsReport, st)
+
+ReportOk(exitOk, wantsReport, st) ==
+    exitOk /\ (SeenOk(wantsReport, st) \/ ~SeenNg(wantsReport, st))
+
+\* Only the earlier rules read whether report-status was negotiated.
+ReportChoices == IF Decision = "ground-truth" THEN {TRUE} ELSE BOOLEAN
+
+ExitChoices == IF GitMayCrash THEN BOOLEAN ELSE {TRUE}
+
+\* The disposition of a push after receive-pack returns.
+\*   ground-truth: compare the workspace refs with the refs it was hydrated
+\*   from.  Unchanged: nothing to publish.  Changed and exited zero: publish.
+\*   Changed and exited non-zero: abort.
+Disposition(exitOk, wantsReport, st, changed) ==
+    CASE Decision = "legacy" ->
+           IF LegacyOk(exitOk, wantsReport, st) THEN "publish" ELSE "relay"
+      [] Decision = "report" ->
+           IF ReportOk(exitOk, wantsReport, st) THEN "publish" ELSE "relay"
+      [] OTHER ->
+           IF ~changed THEN "relay"
+           ELSE IF exitOk THEN "publish" ELSE "abort"
+
+\* cas_publish.rs: the manifest a push stages.  The delta pack holds the
+\* objects reachable from the new refs and not from the hydrated refs; a
+\* base that already lists CompactAt packs is replaced by one pack holding
+\* everything reachable.
+StagedManifest(b, W, objs) ==
+    LET P      == BaseRefs(b)
+        delta  == (Reachable(W) \ Reachable(P)) \cap objs
+        grown  == (IF Fault("drop-parent-packs") THEN {} ELSE BasePacks(b))
+                    \cup PackOf(delta)
+        packs  == IF Cardinality(BasePacks(b)) >= CompactAt
+                  THEN PackOf(Reachable(W) \cap objs)
+                  ELSE grown
+    IN [refs   |-> W,
+        head   |-> PublishedHead(W, BaseHead(b)),
+        packs  |-> packs,
+        parent |-> Successor(b)]
+
+-----------------------------------------------------------------------------
+\* Push
+
+\* A request arrives with its commands.  The commands are computed by the
+\* client from an earlier advertisement (see ClientCommands).
+Arrive(c) ==
+    /\ pc[c] = "idle"
+    /\ \E cmds \in ClientCommands(BaseRefs(pointer)), may \in BOOLEAN :
+         call' = [call EXCEPT ![c] = [cmds |-> cmds, mayPush |-> may]]
+    /\ pc'   = [pc EXCEPT ![c] = "arrived"]
+    /\ resp' = [resp EXCEPT ![c] = NoResp]
+    /\ UNCHANGED <<pointer, mstore, pstore, writes, base, stat, staged, lin,
+                   spc, sbase, starget, rd, credit>>
+
+\* The relay reads the pointer once, hydrates a workspace from it, and runs
+\* receive-pack.  All of this is local to the request, so it is one step; the
+\* request's fate (relay / publish / abort) is then fixed.
+\*
+\* A request that will publish nothing takes effect here, at its read of the
+\* pointer: every "ok" git reports for it belongs to a command that asked for
+\* the value the ref already had, and that was true of the published state at
+\* this step.  It need not be true any later.
+Begin(c) ==
+    /\ pc[c] = "arrived"
+    /\ pointer # Absent => pointer.body \in mstore /\ pointer.body.packs \subseteq pstore
+    /\ call[c].cmds \in ClientCommands(BaseRefs(pointer))
+    /\ \E wantsReport \in ReportChoices, clientPack \in Packs, exitOk \in ExitChoices :
+         LET cmds  == call[c].cmds
+             P     == BaseRefs(pointer)
+             objs  == ObjectsOf(BasePacks(pointer)) \cup clientPack
+             valid == IF HookPermits(cmds, call[c].mayPush)
+                      THEN ValidCmds(cmds, P, objs) ELSE {}
+         IN \E applied \in SUBSET valid :
+              LET W    == [r \in Refs |-> IF r \in applied THEN cmds[r].new ELSE P[r]]
+                  st   == StatusOf(cmds, applied)
+                  disp == Disposition(exitOk, wantsReport, st, W # P)
+              IN /\ pc'     = [pc EXCEPT ![c] = disp]
+                 /\ stat'   = [stat EXCEPT ![c] = IF disp = "abort" THEN NoReport ELSE st]
+                 /\ base'   = [base EXCEPT ![c] = IF disp = "publish" THEN pointer ELSE Absent]
+                 /\ staged' = [staged EXCEPT ![c] =
+                                 IF disp = "publish"
+                                 THEN StagedManifest(pointer, W, objs)
+                                 ELSE NoManifest]
+                 /\ lin'    = IF disp = "relay" THEN [lin EXCEPT ![c] = st] ELSE lin
+    /\ UNCHANGED <<pointer, mstore, pstore, writes, call, resp,
+                   spc, sbase, starget, rd, credit>>
+
+\* The relay answers from git's output and publishes nothing.
+Skip(c) ==
+    /\ pc[c] = "relay"
+    /\ pc'  = [pc EXCEPT ![c] = "answer"]
+    /\ UNCHANGED <<pointer, mstore, pstore, writes, base, call, stat,
+                   staged, lin, resp, spc, sbase, starget, rd, credit>>
+
+\* Steps 4-6 of the write path: packs first, then the manifest.
+Upload(c) ==
+    /\ pc[c] = "publish"
+    /\ ~Fault("cas-before-upload")
+    /\ pstore' = pstore \cup staged[c].packs
+    /\ mstore' = mstore \cup {staged[c]}
+    /\ pc' = [pc EXCEPT ![c] = "uploaded"]
+    /\ UNCHANGED <<pointer, writes, base, call, stat, staged, lin, resp,
+                   spc, sbase, starget, rd, credit>>
+
+\* Step 7: the conditional pointer write.  Winning it is the linearization
+\* point of the push.  Losing it changes nothing and is covered by Fail.
+CasWin(c) ==
+    /\ pc[c] = IF Fault("cas-before-upload") THEN "publish" ELSE "uploaded"
+    /\ CasWouldWin(base[c])
+    /\ pointer' = [body |-> staged[c], etag |-> EtagOf(staged[c], NextWrites)]
+    /\ writes'  = NextWrites
+    /\ credit'  = Publication(c, staged[c])
+    /\ lin'     = [lin EXCEPT ![c] = stat[c]]
+    /\ pc'      = [pc EXCEPT ![c] = "answer"]
+    /\ UNCHANGED <<mstore, pstore, base, call, stat, staged, resp,
+                   spc, sbase, starget, rd>>
+
+\* Fault "cas-before-upload": the upload happens after the pointer moved.
+LateUpload(c) ==
+    /\ Fault("cas-before-upload")
+    /\ pc[c] = "answer"
+    /\ staged[c] # NoManifest
+    /\ pstore' = pstore \cup staged[c].packs
+    /\ mstore' = mstore \cup {staged[c]}
+    /\ UNCHANGED <<pointer, writes, pc, base, call, stat, staged, lin,
+                   resp, spc, sbase, starget, rd, credit>>
+
+\* Fault "stale-base": the pointer is read a second time for the CAS
+\* precondition, while the staged manifest was derived from the first read.
+Reread(c) ==
+    /\ Fault("stale-base")
+    /\ pc[c] = "uploaded"
+    /\ pointer # Absent
+    /\ base' = [base EXCEPT ![c] = pointer]
+    /\ UNCHANGED <<pointer, mstore, pstore, writes, pc, call, stat,
+                   staged, lin, resp, spc, sbase, starget, rd, credit>>
+
+Reset(c) ==
+    /\ pc'     = [pc EXCEPT ![c] = "idle"]
+    /\ call'   = [call EXCEPT ![c] = NoCall]
+    /\ stat'   = [stat EXCEPT ![c] = NoReport]
+    /\ base'   = [base EXCEPT ![c] = Absent]
+    /\ staged' = [staged EXCEPT ![c] = NoManifest]
+    /\ lin'    = [lin EXCEPT ![c] = NoOut]
+
+\* The response.  It carries git's own status report, or no report if the
+\* client did not negotiate one.  Whether it did is not recorded: only the
+\* earlier rules read it, and both answers are allowed here in every case.
+Respond(c) ==
+    /\ \/ pc[c] = "answer"
+       \/ Fault("ack-before-cas") /\ pc[c] = "uploaded"
+    /\ \E answer \in {stat[c], NoReport} : resp' = [resp EXCEPT ![c] = answer]
+    /\ Reset(c)
+    /\ UNCHANGED <<pointer, mstore, pstore, writes, spc, sbase, starget, rd, credit>>
+
+\* Any failure: a lost CAS race (409), an aborted publish (500), a crash, a
+\* timeout, or a response lost after the pointer moved.  The client learns
+\* nothing about the outcome.
+Fail(c) ==
+    /\ pc[c] # "idle"
+    /\ resp' = [resp EXCEPT ![c] = Error]
+    /\ Reset(c)
+    /\ UNCHANGED <<pointer, mstore, pstore, writes, spc, sbase, starget, rd, credit>>
+
+-----------------------------------------------------------------------------
+\* Repository creation, the default-branch setter, readers, and deletion
+
+\* handlers/side_effects.rs, seed_manifest_pointer: on announcement, create
+\* the pointer for an empty repository with If-None-Match: *.
+Seed ==
+    /\ pointer = Absent
+    /\ mstore'  = mstore \cup {EmptyManifest}
+    /\ pointer' = [body |-> EmptyManifest, etag |-> EtagOf(EmptyManifest, NextWrites)]
+    /\ writes'  = NextWrites
+    /\ credit'  = Publication(Owner, EmptyManifest)
+    /\ UNCHANGED <<pstore, pc, base, call, stat, staged, lin, resp,
+                   spc, sbase, starget, rd>>
+
+\* settings.rs: the manifest the setter writes.  A request naming the branch
+\* that is already the default writes the manifest it read.
+SetManifestOf(b, h) ==
+    IF b.body.head = h THEN b.body
+    ELSE [b.body EXCEPT !.head = h, !.parent = Successor(b)]
+
+\* Read the pointer, validate the requested branch against the manifest that
+\* was read, and store the successor manifest.
+SetBegin ==
+    /\ HasSetter
+    /\ spc = "idle"
+    /\ pointer # Absent
+    /\ \E h \in Refs :
+         /\ pointer.body.refs[h] # NoOid
+         /\ starget' = h
+         /\ mstore' = mstore \cup {SetManifestOf(pointer, h)}
+    /\ sbase' = pointer
+    /\ spc' = "staged"
+    /\ UNCHANGED <<pointer, pstore, writes, pc, base, call, stat, staged,
+                   lin, resp, rd, credit>>
+
+SetReset ==
+    /\ spc' = "idle"
+    /\ sbase' = Absent
+    /\ starget' = DefaultHead
+
+\* The setter always performs the conditional write, also when the branch is
+\* already the default; that case rewrites the same body.
+SetCas ==
+    /\ spc = "staged"
+    /\ CasWouldWin(sbase)
+    /\ LET m == SetManifestOf(sbase, starget)
+       IN /\ pointer' = [body |-> m, etag |-> EtagOf(m, NextWrites)]
+          /\ credit'  = IF m = sbase.body THEN credit ELSE Publication(Manager, m)
+    /\ writes' = NextWrites
+    /\ SetReset
+    /\ UNCHANGED <<mstore, pstore, pc, base, call, stat, staged, lin,
+                   resp, rd>>
+
+SetFail ==
+    /\ spc = "staged"
+    /\ SetReset
+    /\ UNCHANGED <<pointer, mstore, pstore, writes, pc, base, call, stat,
+                   staged, lin, resp, rd, credit>>
+
+\* A reader resolves the pointer.  It fetches the manifest and packs later,
+\* at any time; ReaderComplete says that fetch cannot fail.
+Read ==
+    /\ HasReader
+    /\ pointer # Absent
+    /\ rd' = pointer.body
+    /\ UNCHANGED <<pointer, mstore, pstore, writes, pc, base, call, stat,
+                   staged, lin, resp, spc, sbase, starget, credit>>
+
+\* Fault "gc": delete a pack that the current manifest does not list.
+Collect ==
+    /\ Fault("gc")
+    /\ pointer # Absent
+    /\ \E p \in pstore \ pointer.body.packs : pstore' = pstore \ {p}
+    /\ UNCHANGED <<pointer, mstore, writes, pc, base, call, stat, staged,
+                   lin, resp, spc, sbase, starget, rd, credit>>
+
+-----------------------------------------------------------------------------
 Init ==
-    /\ pointer = 0
-    /\ published = {0}
-    /\ packs = [m \in ManifestIds |-> {}]
-    /\ pc = [p \in Pushers |-> "idle"]
-    /\ readEtag = [p \in Pushers |-> 0]
-    /\ staged = [p \in Pushers |-> 0]
-    /\ parent = [m \in ManifestIds |-> 0]
-    /\ refs = [m \in ManifestIds |-> 0]   \* "main" starts at objectId 0 (empty)
-    /\ compacted = {}
-    /\ newVal = [p \in Pushers |-> 0]
-    /\ snapErr = [p \in Pushers |-> FALSE]
-    /\ observed = {}
-
-\* A fresh manifest id, distinct from every published manifest AND every
-\* concurrently-staged one (Perci): distinct pushes mint distinct content-addressed
-\* manifests, so two concurrent stages never alias the same id. This keeps the
-\* no-lost-update counterexamples about CAS serialization, not id collision.
-StagedIds == { staged[q] : q \in Pushers }
-FreshId == CHOOSE m \in ManifestIds : m \notin published /\ m \notin StagedIds /\ m # 0
-
-CanStage == \E m \in ManifestIds : m \notin published /\ m \notin StagedIds /\ m # 0
-
-\* The publish-skip decision (the fallible-snapshot fence, Quinn #2 / Dawn's case).
-\* A push skips publish ONLY if its snapshots succeeded AND showed no ref change.
-\* If either snapshot errored (snapErr), it must NOT skip -- it falls through to CAS.
-\* This is "Ok(b) = Ok(a)", never "b = a" with errors silently equal.
-MustPublish(p) == DidChange(p) \/ snapErr[p]
-
-\* Steps 3-6: read pointer; nondeterministically this push either changes refs or
-\* is a no-op, and its ref-snapshot reads either succeed or fail. Stage a manifest.
-Begin(p) ==
-    /\ pc[p] = "idle"
-    /\ CanStage
-    \* This push proposes some value v for "main" (v = current value models a
-    \* no-op push; v # current models a real ref change); its snapshot reads may
-    \* fail (e). The staged manifest binds "main" to v and is derived from the
-    \* manifest the push READ -- so a stale reader builds on stale ref state, and
-    \* only the CAS guard stops it from clobbering a newer published value.
-    /\ \E v \in ObjIds, e \in BOOLEAN, compact \in BOOLEAN :
-         /\ newVal'  = [newVal  EXCEPT ![p] = v]
-         /\ snapErr' = [snapErr EXCEPT ![p] = e]
-         /\ LET m == FreshId IN
-              /\ readEtag' = [readEtag EXCEPT ![p] = pointer]
-              /\ staged'   = [staged   EXCEPT ![p] = m]
-              /\ parent'   = [parent   EXCEPT ![m] = pointer]
-              \* A compact stage models `pack-objects` over every post-push
-              \* ref tip. Its own pack is therefore trusted to cover the full
-              \* reachable closure; a normal stage extends the parent pack set.
-              /\ packs'    = [packs EXCEPT
-                                  ![m] = IF compact
-                                        THEN {m}
-                                        ELSE packs[pointer] \union {m}]
-              /\ refs'     = [refs     EXCEPT ![m] = v]
-              /\ compacted' = IF compact
-                              THEN compacted \union {m}
-                              ELSE compacted \ {m}
-    /\ pc' = [pc EXCEPT ![p] = "staged"]
-    /\ UNCHANGED <<pointer, published, observed>>
-
-\* No-op fast path: a push that must NOT publish (no change, snapshots ok) goes
-\* straight to done WITHOUT touching the pointer -- zero CAS/publish latency.
-SkipPublish(p) ==
-    /\ pc[p] = "staged"
-    /\ ~MustPublish(p)
-    /\ pc' = [pc EXCEPT ![p] = "done"]
-    /\ UNCHANGED <<pointer, published, packs, readEtag, staged, parent, refs, compacted, newVal, snapErr, observed>>
-
-\* Step 7: CAS.  Succeeds iff pointer still equals the etag this pusher read (A3).
-CasSucceed(p) ==
-    /\ pc[p] = "staged"
-    /\ MustPublish(p)
-    /\ pointer = readEtag[p]
-    /\ pointer' = staged[p]
-    /\ published' = published \union {staged[p]}
-    /\ pc' = [pc EXCEPT ![p] = "done"]
-    /\ UNCHANGED <<packs, readEtag, staged, parent, refs, compacted, newVal, snapErr, observed>>
-
-CasFail(p) ==
-    /\ pc[p] = "staged"
-    /\ MustPublish(p)
-    /\ pointer # readEtag[p]
-    /\ pc' = [pc EXCEPT ![p] = "lost"]   \* will retry from idle
-    /\ UNCHANGED <<pointer, published, packs, readEtag, staged, parent, refs, compacted, newVal, snapErr, observed>>
-
-\* Step 8: the fence.  Observe success ONLY after the push reached "done"
-\* (either via successful CAS or a legitimate skip).
-Observe(p) ==
-    /\ pc[p] = "done"
-    /\ observed' = observed \union {p}
-    /\ UNCHANGED <<pointer, published, packs, pc, readEtag, staged, parent, refs, compacted, newVal, snapErr>>
-
-\* A loser retries: back to idle, ready to re-read the advanced pointer.
-Retry(p) ==
-    /\ pc[p] = "lost"
-    /\ pc' = [pc EXCEPT ![p] = "idle"]
-    /\ UNCHANGED <<pointer, published, packs, readEtag, staged, parent, refs, compacted, newVal, snapErr, observed>>
+    /\ pointer = Absent
+    /\ mstore = {}
+    /\ pstore = {}
+    /\ writes = 0
+    /\ pc     = [c \in Clients |-> "idle"]
+    /\ base   = [c \in Clients |-> Absent]
+    /\ call   = [c \in Clients |-> NoCall]
+    /\ stat   = [c \in Clients |-> NoReport]
+    /\ staged = [c \in Clients |-> NoManifest]
+    /\ lin    = [c \in Clients |-> NoOut]
+    /\ resp   = [c \in Clients |-> NoResp]
+    /\ spc = "idle"
+    /\ sbase = Absent
+    /\ starget = DefaultHead
+    /\ rd = NoRead
+    /\ credit = NoEntry
 
 Next ==
-    \E p \in Pushers :
-        Begin(p) \/ SkipPublish(p) \/ CasSucceed(p) \/ CasFail(p)
-          \/ Observe(p) \/ Retry(p)
+    \/ Seed \/ SetBegin \/ SetCas \/ SetFail \/ Read \/ Collect
+    \/ \E c \in Clients :
+         \/ Arrive(c) \/ Begin(c) \/ Skip(c) \/ Upload(c) \/ CasWin(c)
+         \/ LateUpload(c) \/ Reread(c) \/ Respond(c) \/ Fail(c)
 
-Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
+Spec == Init /\ [][Next]_vars
 
-------------------------------------------------------------------------------
-\* SAFETY PROPERTIES
+-----------------------------------------------------------------------------
+\* Store invariants
 
-\* T1 (Durability-Ordering): any observed push that was obligated to publish
-\* (it changed refs, or its snapshot reads errored) has its staged manifest in
-\* the durable published history before the client observes success. A
-\* legitimately-skipped no-op push (no change, snapshots ok) is exempt -- it
-\* publishes nothing and is correct to do so.
-Inv_Fence ==
-    \A p \in observed : MustPublish(p) => staged[p] \in published
+Stored(m) == m \in mstore /\ m.packs \subseteq pstore
 
-\* The bite for the fallible-snapshot case (Quinn #2 / Dawn): if a push actually
-\* changed refs and was observed, its change is durably published -- regardless of
-\* snapshot outcome. This is what breaks if SkipPublish ignores snapErr (i.e. if
-\* the skip predicate were "b = a" instead of "Ok(b) = Ok(a) /\ no change").
+\* T1, fence: the pointer never names anything that is not stored.
+Fence == pointer # Absent => Stored(pointer.body)
+
+\* T1 for readers: what a reader resolved stays fetchable.
+ReaderComplete == rd # NoRead => Stored(rd)
+
+\* T2, closure: the packs a manifest lists contain every object reachable
+\* from its refs, so a workspace built from them alone is a complete
+\* repository.
+Closed(m) == Reachable(m.refs) \subseteq ObjectsOf(m.packs)
+PublishedClosed ==
+    /\ pointer # Absent => Closed(pointer.body)
+    /\ rd # NoRead => Closed(rd)
+
+\* The published HEAD names a published branch whenever one exists.
+HeadPublished ==
+    pointer # Absent =>
+        ((\E r \in Refs : pointer.body.refs[r] # NoOid)
+            => pointer.body.refs[pointer.body.head] # NoOid)
+
+StoreInvariants ==
+    /\ Fence
+    /\ ReaderComplete
+    /\ PublishedClosed
+    /\ HeadPublished
+
+\* Two consequences of the refinement, stated on their own so that a
+\* violation produces a short, specific counterexample.
 \*
-\* NOTE (Dawn): this is NOT redundant with Inv_Fence, even though
-\* MustPublish == DidChange \/ snapErr makes Inv_Fence look strictly stronger.
-\* Inv_Fence is predicated on the OPERATOR MustPublish; mutate that operator (the
-\* skip-on-error bug) and Inv_Fence's own predicate moves with it, so the mutated
-\* Inv_Fence stops catching the bug. Inv_ChangedPublished is predicated on
-\* DidChange directly, independent of MustPublish, so it stays load-bearing under
-\* exactly the mutation we care about. Do not delete it as "redundant."
-Inv_ChangedPublished ==
-    \A p \in observed : DidChange(p) => staged[p] \in published
+\* A request that is answered from git's output without publishing reported
+\* "ok" only for commands that asked for no change.
+Changes(c, r) == call[c].cmds[r].new # call[c].cmds[r].old
+NoSilentDrop ==
+    \A c \in Clients :
+        pc[c] = "relay" => \A r \in Refs : stat[c][r] = "ok" => ~Changes(c, r)
 
-Installed(p) == (p \in observed) /\ MustPublish(p) /\ (staged[p] \in published)
+\* A request that reaches the publish path was accepted by the push policy
+\* and git applied at least one command that changes a ref.
+PublishIsAuthorizedChange ==
+    \A c \in Clients :
+        pc[c] \in {"publish", "uploaded"} =>
+            /\ call[c].mayPush
+            /\ \E r \in Refs : stat[c][r] = "ok" /\ Changes(c, r)
 
-\* (A former Inv_NoLost -- "distinct installs never share a manifest id" -- was
-\* removed: with FreshId excluding in-flight staged ids, Inv_NoFork implies it, so
-\* it caught only a model aliasing artifact, not a real failure mode. Verified by
-\* checking that no mutation trips it without also tripping Inv_NoFork.)
+\* Not a requirement.  check.sh requires this to be VIOLATED by the protocol
+\* as specified, which shows that the model reaches the case NoSilentDrop
+\* makes an exception for: git reports "ok" for a command that asked for no
+\* change, and the relay passes that on without publishing.
+NeverRelaysOk ==
+    \A c \in Clients : pc[c] = "relay" => \A r \in Refs : stat[c][r] # "ok"
 
-\* T3b (Ref-update linearizability -- Dawn's user-visible theorem): the model
-\* now carries the REAL ref value (refs[m] = the objectId "main" holds in manifest
-\* m), not just effect tokens. Two properties bind the proof to ref VALUES:
-\*
-\* (i) Every installed push's own proposed value is exactly what its manifest
-\*     commits -- the push's effect is applied, not dropped.
-Inv_RefEffectApplied ==
-    \A p \in Pushers : Installed(p) => (refs[staged[p]] = newVal[p])
+\* With parent links, a pointer write that changes the manifest names the
+\* manifest it replaced.  The published manifests then form a single chain,
+\* which is what makes the predecessor field usable as an audit trail.
+ParentIsPredecessor ==
+    [][(ParentLinks /\ pointer # Absent /\ pointer'.body # pointer.body)
+          => pointer'.body.parent = pointer.body]_vars
 
-\* (ii) An installed push computed its new value from the manifest that was the
-\*     pointer AT INSTALL TIME (its parent is the pointer it read, and the CAS
-\*     guard forced read == current). So no install builds "main" on top of a
-\*     value that a concurrent winner already superseded -- the lost-update of a
-\*     ref value. Operationally: an installed manifest's parent is published and
-\*     its value was derived from that parent, giving a single serial line of ref
-\*     values. (The fork ban, Inv_NoFork, plus this, is ref linearizability.)
-Inv_RefDerivedFromParent ==
-    \A p \in Pushers :
-        Installed(p) => (parent[staged[p]] = readEtag[p] /\ readEtag[p] \in published)
+-----------------------------------------------------------------------------
+\* Refinement: this protocol implements the atomic reference database.
 
-\* T2 (Reconstruction coverage -- non-vacuous): every published non-root
-\* manifest either names its trusted full-closure compaction pack, or covers its
-\* published parent's pack set plus its own delta pack. The model abstracts
-\* Git's reachability walk as the `compacted` marker; production earns that
-\* marker only by feeding every post-push ref tip to `git pack-objects --revs`.
-Inv_Closed ==
-    \A m \in published :
-        (m # 0 /\ parent[m] \in published) =>
-            (m \in packs[m] /\
-                (m \in compacted \/ packs[parent[m]] \subseteq packs[m]))
+AbsDb ==
+    IF pointer = Absent THEN Absent
+    ELSE [refs |-> pointer.body.refs, head |-> pointer.body.head]
 
-\* Parent integrity: every published non-root manifest's parent is also published
-\* (the install chain is grounded in durable history, never in vapor).
-Inv_ParentPublished ==
-    \A m \in published : (m = 0) \/ (parent[m] \in published)
+Abs == INSTANCE GitRefDB WITH db <- AbsDb, out <- lin
 
-\* The pointer is always itself a published manifest (never points at vapor).
-Inv_PointerPublished ==
-    pointer \in published
+Refines == Abs!Spec
 
-\* T3c (Linear history -- the real no-lost-update): the published manifests form
-\* a single chain ending at the current pointer; there is no fork. A lost update
-\* is precisely a fork: two installs sharing a parent, so one's effects are
-\* dropped from the surviving line. Reachability of every published manifest from
-\* the pointer via parent edges rules that out. With MaxManifests bound, we check
-\* the contrapositive directly: no two distinct published non-root manifests share
-\* a parent (a shared parent = a fork = a lost update). The A3 CAS guard is what
-\* makes this hold; removing it lets two pushers install off the same parent.
-Inv_NoFork ==
-    \A m1, m2 \in published :
-        (m1 # m2 /\ m1 # 0 /\ m2 # 0) => (parent[m1] # parent[m2])
-
-\* Finiteness bound: at most MaxManifests distinct manifests may be published.
-\* Without it the Retry loop lets pushers churn newVal/FreshId unboundedly.
-BoundedManifests == Cardinality(published) <= MaxManifests
-
-Safety ==
-    /\ TypeOK
-    /\ Inv_Fence
-    /\ Inv_ChangedPublished
-    /\ Inv_RefEffectApplied
-    /\ Inv_RefDerivedFromParent
-    /\ Inv_NoFork
-    /\ Inv_Closed
-    /\ Inv_ParentPublished
-    /\ Inv_PointerPublished
+-----------------------------------------------------------------------------
+\* Names used by comments in the implementation and in migration 0002, which
+\* were written against an earlier version of this module.  Each now stands
+\* for the property given here.
+Inv_NoFork               == Refines
+Inv_RefEffectApplied     == Refines
+Inv_RefDerivedFromParent == ParentIsPredecessor
+Inv_Closed               == PublishedClosed
 =============================================================================
diff --git a/docs/spec/GitPushPath.qnt b/docs/spec/GitPushPath.qnt
new file mode 100644
index 0000000000..eab61173c5
--- /dev/null
+++ b/docs/spec/GitPushPath.qnt
@@ -0,0 +1,327 @@
+// Model of the parts of Buzz's Git-on-object-storage push path that the TLA+
+// model (docs/spec/GitOnObjectStore.tla) leaves out: the serving-write lease
+// around the pointer CAS and the timestamps of the kind:30618 events. It also
+// states the publish decision over what clients are told, which complements
+// the refinement statement of the TLA+ model.
+//
+// - info/refs and the receive-pack POST are separate requests; each hydrates
+//   from whatever pointer is current when it runs (transport.rs).
+// - receive-pack applies each ref update independently (non-atomic push); a
+//   pre-receive hook decline rejects all refs. The per-ref outcome is written
+//   to the client only if it negotiated `report-status`, and a request may
+//   carry no commands at all.
+// - finalize_push decides whether to publish (`push_disposition`), then CASes
+//   the manifest pointer inside a serving-write lease that can be lost around
+//   the CAS (buzz-deletion).
+// - after the CAS, the relay emits a kind:30618 ref-state event; clients read
+//   the newest one, ties broken by lowest id
+//   (desktop/src/features/projects/hooks.ts, buzz-db ORDER BY created_at DESC,
+//   id ASC).
+//
+// Invariants are stated over what clients observe, not over protocol
+// internals. PUBLISH_RULE selects the implemented publish decision or one of
+// the two rules the relay used earlier, and each FIX_* constant switches one
+// defect to its fix. `fixed` models the code as it is; `current` models the
+// code before any of the fixes.
+//
+// Check with Quint (https://quint-lang.org):
+//   quint run docs/spec/GitPushPath.qnt --main fixed --invariant safety \
+//     --max-steps 14 --max-samples 2000000 --seed 0x1
+//   quint verify docs/spec/GitPushPath.qnt --main fixed --invariant safety \
+//     --max-steps 8
+// The same commands with --main current, partialBugOnly, reportRuleOnly,
+// leaseBugOnly, or timestampBugOnly report a counterexample.
+//
+// The initial manifest carries a stamp. The announce-time seed and manifests
+// written before `published_at` existed carry none; the argument for them
+// rests on an assumption about clocks that is stated in
+// docs/git-on-object-storage.md and is not modeled here.
+module buzzgit {
+  // "refs":   publish when receive-pack changed the workspace refs (the
+  //           implemented rule, `push_disposition`).
+  // "report": publish when the status report has an `ok` line or no `ng`
+  //           line (the rule before it).
+  // "no_ng":  publish when the status report has no `ng` line (the original
+  //           rule).
+  const PUBLISH_RULE: str
+  const FIX_LEASE: bool
+  const FIX_TIMESTAMPS: bool
+
+  // ---- Domain ----------------------------------------------------------
+
+  type Refs = str -> int // ref name -> commit; 0 means absent
+
+  type Push = {
+    phase: str,          // idle | advertised | received | committed | done
+    adv: Refs,           // refs the client saw in info/refs
+    targets: Set[str],   // refs this push updates (each to commit = pusher id)
+    base: int,           // manifest version receive-pack hydrated from
+    ws: Refs,            // workspace refs after receive-pack
+    report: str -> str,  // what receive-pack did with each command: ok | ng
+    status: bool,        // did the client negotiate report-status?
+    told: str -> str,    // what the client printed: ok | ng | fail
+    stamp: int,          // created_at of the 30618 this push emits
+  }
+
+  type Manifest = { refs: Refs, stamp: int }
+  type Event = { createdAt: int, id: int, refs: Refs }
+
+  pure val REF_LIST = ["main", "feature", "feature/x"]
+  pure val REFS = Set("main", "feature", "feature/x")
+  pure val PUSHERS = Set(1, 2)
+  pure val EVENT_IDS = 1.to(5)
+  pure val MAX_TIME = 2
+
+  pure val INITIAL_REFS: Refs = Map("main" -> 9, "feature" -> 9, "feature/x" -> 0)
+
+  pure val IDLE: Push = {
+    phase: "idle",
+    adv: INITIAL_REFS,
+    targets: Set(),
+    base: 0,
+    ws: INITIAL_REFS,
+    report: Map(),
+    status: true,
+    told: Map(),
+    stamp: 0,
+  }
+
+  // git refuses a ref whose name is a directory/file prefix of a live ref.
+  pure def dfConflict(ws: Refs, r: str): bool =
+    (r == "feature/x" and ws.get("feature") != 0) or
+    (r == "feature" and ws.get("feature/x") != 0)
+
+  // Non-atomic receive-pack: process commands in order; each applies only if
+  // the workspace still holds the client's old value and the name is free.
+  pure def receivePack(p: int, adv: Refs, targets: Set[str], ws0: Refs, hookDeny: bool)
+      : { ws: Refs, report: str -> str } = {
+    if (hookDeny)
+      { ws: ws0, report: targets.mapBy(_ => "ng") }
+    else
+      REF_LIST.foldl({ ws: ws0, report: Map() }, (acc, r) =>
+        if (not(targets.contains(r))) acc
+        else if (acc.ws.get(r) == adv.get(r) and not(dfConflict(acc.ws, r)))
+          { ws: acc.ws.set(r, p), report: acc.report.put(r, "ok") }
+        else
+          { ws: acc.ws, report: acc.report.put(r, "ng") })
+  }
+
+  pure def anyOk(report: str -> str): bool = report.keys().exists(r => report.get(r) == "ok")
+  pure def anyNg(report: str -> str): bool = report.keys().exists(r => report.get(r) == "ng")
+
+  // The status report as the relay and the client see it: git writes the
+  // per-ref lines only for a client that negotiated report-status.
+  pure def visible(pr: Push): str -> str = if (pr.status) pr.report else Map()
+
+  // transport.rs. `hydrated` is the ref state the workspace was built from.
+  pure def shouldPublish(pr: Push, hydrated: Refs): bool =
+    if (PUBLISH_RULE == "refs") pr.ws != hydrated
+    else if (PUBLISH_RULE == "report") anyOk(visible(pr)) or not(anyNg(visible(pr)))
+    else not(anyNg(visible(pr)))
+
+  pure def max(a: int, b: int): int = if (a > b) a else b
+
+  // ---- State -------------------------------------------------------------
+
+  var ptr: int                     // current manifest version (the pointer)
+  var manifests: int -> Manifest   // published manifests by version
+  var nextVersion: int
+  var events: Set[Event]           // stored kind:30618 events
+  var now: int                     // wall clock (seconds)
+  var push: int -> Push
+  var landed: Set[(int, str)]      // (pusher, ref) updates that reached the pointer
+
+  // ---- Actions -----------------------------------------------------------
+
+  action init = all {
+    ptr' = 0,
+    manifests' = Map(0 -> { refs: INITIAL_REFS, stamp: 0 }),
+    nextVersion' = 1,
+    events' = Set({ createdAt: 0, id: 0, refs: INITIAL_REFS }),
+    now' = 0,
+    push' = PUSHERS.mapBy(_ => IDLE),
+    landed' = Set(),
+  }
+
+  // GET info/refs: the client learns the current refs and picks updates.
+  action advertise(p: int): bool = all {
+    push.get(p).phase == "idle",
+    // A request may carry no commands.
+    nondet targets = REFS.powerset().filter(s => s.size() <= 2).oneOf()
+    push' = push.set(p, { ...push.get(p),
+      phase: "advertised",
+      adv: manifests.get(ptr).refs,
+      targets: targets,
+    }),
+    ptr' = ptr, manifests' = manifests, nextVersion' = nextVersion,
+    events' = events, now' = now, landed' = landed,
+  }
+
+  // POST git-receive-pack: hydrate from the *current* pointer, run hook and
+  // per-ref updates in the ephemeral workspace.
+  action receive(p: int): bool = all {
+    push.get(p).phase == "advertised",
+    nondet hookDeny = Set(true, false).oneOf()
+    nondet status = Set(true, false).oneOf()
+    val pr = push.get(p)
+    val result = receivePack(p, pr.adv, pr.targets, manifests.get(ptr).refs, hookDeny)
+    push' = push.set(p, { ...pr,
+      phase: "received",
+      base: ptr,
+      ws: result.ws,
+      report: result.report,
+      status: status,
+    }),
+    ptr' = ptr, manifests' = manifests, nextVersion' = nextVersion,
+    events' = events, now' = now, landed' = landed,
+  }
+
+  // finalize_push when it does not publish: either the rule found nothing to
+  // publish, or the CAS lost the race (409, the client sees an HTTP error for
+  // every ref).
+  action finalizeNoPublish(p: int): bool = all {
+    val pr = push.get(p)
+    val publish = shouldPublish(pr, manifests.get(pr.base).refs)
+    all {
+      pr.phase == "received",
+      not(publish) or ptr != pr.base,
+      // Skipped publish: git's report-status goes back verbatim.
+      // Lost CAS: 409, an HTTP error for every ref.
+      push' = push.set(p, { ...pr,
+        phase: "done",
+        told: if (publish) pr.targets.mapBy(_ => "fail") else visible(pr),
+      }),
+    },
+    ptr' = ptr, manifests' = manifests, nextVersion' = nextVersion,
+    events' = events, now' = now, landed' = landed,
+  }
+
+  // finalize_push CAS. The serving-write lease may be lost after the pointer
+  // PUT lands; `protect` then discards the result and returns 503.
+  action commit(p: int): bool = all {
+    val pr = push.get(p)
+    all {
+      pr.phase == "received",
+      shouldPublish(pr, manifests.get(pr.base).refs),
+      ptr == pr.base,
+      nondet leaseLostAfterCas = Set(true, false).oneOf()
+      nondet skew = Set(0, 1).oneOf() // per-instance clock offset
+      val okRefs = pr.report.keys().filter(r => pr.report.get(r) == "ok")
+      val parentStamp = manifests.get(ptr).stamp
+      val stamp = if (FIX_TIMESTAMPS) max(now + skew, parentStamp + 1) else now + skew
+      all {
+        ptr' = nextVersion,
+        manifests' = manifests.put(nextVersion, { refs: pr.ws, stamp: stamp }),
+        nextVersion' = nextVersion + 1,
+        landed' = landed.union(okRefs.map(r => (p, r))),
+        // On lease loss: 503 "community write lease lost"; no 30618 is emitted.
+        push' = push.set(p,
+          if (leaseLostAfterCas and not(FIX_LEASE))
+            { ...pr, phase: "done", told: pr.targets.mapBy(_ => "fail") }
+          else
+            { ...pr, phase: "committed", stamp: stamp }),
+      },
+    },
+    events' = events, now' = now,
+  }
+
+  // Derived kind:30618 insert, then the success response.
+  action emit(p: int): bool = all {
+    val pr = push.get(p)
+    val usedIds = events.map(e => e.id)
+    all {
+      pr.phase == "committed",
+      nondet id = EVENT_IDS.exclude(usedIds).oneOf()
+      events' = events.union(Set({ createdAt: pr.stamp, id: id, refs: pr.ws })),
+      push' = push.set(p, { ...pr, phase: "done", told: visible(pr) }),
+    },
+    ptr' = ptr, manifests' = manifests, nextVersion' = nextVersion,
+    now' = now, landed' = landed,
+  }
+
+  action tick = all {
+    now < MAX_TIME,
+    now' = now + 1,
+    ptr' = ptr, manifests' = manifests, nextVersion' = nextVersion,
+    events' = events, push' = push, landed' = landed,
+  }
+
+  action step = any {
+    nondet p = PUSHERS.oneOf()
+    any { advertise(p), receive(p), finalizeNoPublish(p), commit(p), emit(p) },
+    tick,
+  }
+
+  // ---- Observations --------------------------------------------------------
+
+  // The 30618 a reader picks: newest created_at, then lowest id.
+  def latestEvent: Event =
+    events.fold({ createdAt: -1, id: 0, refs: INITIAL_REFS }, (best, e) =>
+      if (e.createdAt > best.createdAt or (e.createdAt == best.createdAt and e.id < best.id)) e
+      else best)
+
+  def quiescent: bool = PUSHERS.forall(p => push.get(p).phase == "done")
+
+  // ---- Invariants ----------------------------------------------------------
+
+  // A ref the client printed as pushed reached the published pointer.
+  val noFalseSuccess: bool = PUSHERS.forall(p =>
+    val t = push.get(p).told
+    t.keys().forall(r => t.get(r) == "ok" implies landed.contains((p, r))))
+
+  // A ref the client was told failed did not reach the published pointer.
+  val noFalseFailure: bool = PUSHERS.forall(p =>
+    val t = push.get(p).told
+    t.keys().forall(r => t.get(r) == "fail" implies not(landed.contains((p, r)))))
+
+  // Once pushes settle, the ref state readers see matches the pointer.
+  val refStateMatchesPointer: bool =
+    quiescent implies latestEvent.refs == manifests.get(ptr).refs
+
+  // Every publication changes the refs. A manifest whose refs equal its
+  // predecessor's records no push, yet its kind:30618 names the caller as the
+  // pusher. Versions are allocated in pointer order, so the predecessor of
+  // version v is v - 1.
+  val publicationChangesRefs: bool = 1.to(nextVersion - 1).forall(v =>
+    manifests.get(v).refs != manifests.get(v - 1).refs)
+
+  val safety: bool = and {
+    noFalseSuccess,
+    noFalseFailure,
+    refStateMatchesPointer,
+    publicationChangesRefs,
+  }
+}
+
+// The code before the fixes.
+module current {
+  import buzzgit(PUBLISH_RULE = "no_ng", FIX_LEASE = false, FIX_TIMESTAMPS = false).*
+}
+
+// The code as it is.
+module fixed {
+  import buzzgit(PUBLISH_RULE = "refs", FIX_LEASE = true, FIX_TIMESTAMPS = true).*
+}
+
+// One defect at a time, to attribute each counterexample.
+
+// The original rule: violates noFalseSuccess (a partially accepted push is
+// not published) and publicationChangesRefs.
+module partialBugOnly {
+  import buzzgit(PUBLISH_RULE = "no_ng", FIX_LEASE = true, FIX_TIMESTAMPS = true).*
+}
+
+// The rule that reads the status report: satisfies noFalseSuccess, violates
+// publicationChangesRefs (a request with no commands, or a declined push from
+// a client without report-status, is published).
+module reportRuleOnly {
+  import buzzgit(PUBLISH_RULE = "report", FIX_LEASE = true, FIX_TIMESTAMPS = true).*
+}
+
+module leaseBugOnly {
+  import buzzgit(PUBLISH_RULE = "refs", FIX_LEASE = false, FIX_TIMESTAMPS = true).*
+}
+
+module timestampBugOnly {
+  import buzzgit(PUBLISH_RULE = "refs", FIX_LEASE = true, FIX_TIMESTAMPS = false).*
+}
diff --git a/docs/spec/GitRefDB.cfg b/docs/spec/GitRefDB.cfg
new file mode 100644
index 0000000000..e1b5fc130e
--- /dev/null
+++ b/docs/spec/GitRefDB.cfg
@@ -0,0 +1,23 @@
+\* Sanity check of the abstract specification itself: its stated
+\* consequences hold, with one client (each property is per client).
+SPECIFICATION Spec
+CONSTANTS
+    Clients = {c1}
+    Refs = {main, dev}
+    DefaultHead = main
+    Oids = {o1, o2}
+    NoOid = NoOid
+    Absent = Absent
+    NoCall = NoCall
+    NoOut = NoOut
+    NoCmd = NoCmd
+    NoResp = NoResp
+    Error = Error
+    NoEntry = NoEntry
+    Owner = Owner
+    Manager = Manager
+INVARIANT AppliedWasAuthorized
+INVARIANT CreditMatchesState
+INVARIANT HeadNotDangling
+PROPERTY ToldOnlyTheOutcome
+PROPERTY NoLostUpdate
diff --git a/docs/spec/GitRefDB.tla b/docs/spec/GitRefDB.tla
new file mode 100644
index 0000000000..e2a308ac0a
--- /dev/null
+++ b/docs/spec/GitRefDB.tla
@@ -0,0 +1,184 @@
+------------------------------ MODULE GitRefDB ------------------------------
+(***************************************************************************)
+(* The atomic reference database: what a Git host is supposed to be.       *)
+(*                                                                         *)
+(* This module is the SPECIFICATION that docs/spec/GitOnObjectStore.tla is *)
+(* checked against.  It contains no object store, no packs, no ETags and   *)
+(* no concurrency control.  Every operation takes effect in one step.      *)
+(* The protocol is correct if every one of its behaviors is also a         *)
+(* behavior of this module under the refinement mapping given there; that  *)
+(* statement is linearizability of ref updates, together with the          *)
+(* guarantee that a client is never told an update succeeded when it was   *)
+(* not applied.                                                            *)
+(*                                                                         *)
+(* A push is modeled as an invocation (the client submits ref-update       *)
+(* commands), one atomic linearization step (the commands are evaluated    *)
+(* against the current state and some of them are applied), and a response *)
+(* (the client learns the per-ref outcome, or learns nothing).             *)
+(*                                                                         *)
+(* What this module permits, deliberately:                                 *)
+(*   - Any command may be rejected.  The module states safety only: an     *)
+(*     applied command had the right old value and was authorized.  It     *)
+(*     does not state that a valid command must be accepted.               *)
+(*   - A response may be an error even after the operation took effect.    *)
+(*     A lost reply cannot be distinguished from a failed request, so the  *)
+(*     guarantee runs one way: reported success implies applied.           *)
+(***************************************************************************)
+EXTENDS Naturals
+
+CONSTANTS
+    Clients,      \* identities that push
+    Refs,         \* ref names
+    Oids,         \* object ids a ref may hold
+    NoOid,        \* "this ref does not exist"
+    DefaultHead,  \* symbolic HEAD of a newly created repository
+    Absent,       \* the repository does not exist
+    NoCall, NoOut, NoCmd, NoResp, Error, NoEntry,
+    Owner,        \* actor recorded for repository creation
+    Manager       \* actor recorded for a default-branch change
+
+VARIABLES
+    db,    \* Absent, or [refs, head]: the published ref state
+    call,  \* call[c]: the push client c has outstanding, or NoCall
+    out,   \* out[c]: per-ref outcome fixed when c's push linearized, or NoOut
+    resp,  \* resp[c]: what client c was last told
+    credit \* who the published state is attributed to: [actor, refs, head]
+
+vars == <<db, call, out, resp, credit>>
+
+OidOrNone == Oids \cup {NoOid}
+EmptyRefs == [r \in Refs |-> NoOid]
+Command   == [old : OidOrNone, new : OidOrNone]
+CommandSet == [Refs -> Command \cup {NoCmd}]
+NoReport  == [r \in Refs |-> "none"]
+
+CurRefs == IF db = Absent THEN EmptyRefs ELSE db.refs
+CurHead == IF db = Absent THEN DefaultHead ELSE db.head
+
+\* The published HEAD stays on its branch while that branch exists, and
+\* otherwise moves to some existing branch (which one is left open).  It
+\* dangles only when the repository has no refs at all.
+HeadChoices(refs, h) ==
+    IF refs[h] # NoOid THEN {h}
+    ELSE IF \E r \in Refs : refs[r] # NoOid
+         THEN {r \in Refs : refs[r] # NoOid}
+         ELSE {h}
+
+Entry(actor, refs, head) == [actor |-> actor, refs |-> refs, head |-> head]
+
+Init ==
+    /\ db = Absent
+    /\ call = [c \in Clients |-> NoCall]
+    /\ out  = [c \in Clients |-> NoOut]
+    /\ resp = [c \in Clients |-> NoResp]
+    /\ credit = NoEntry
+
+\* The repository is announced.  Only this action creates an empty repository.
+Create ==
+    /\ db = Absent
+    /\ db' = [refs |-> EmptyRefs, head |-> DefaultHead]
+    /\ credit' = Entry(Owner, EmptyRefs, DefaultHead)
+    /\ UNCHANGED <<call, out, resp>>
+
+\* Client c submits a set of ref-update commands.  mayPush records whether
+\* the push policy authorizes this client's command set.
+Invoke(c) ==
+    /\ call[c] = NoCall
+    /\ \E cs \in CommandSet, may \in BOOLEAN :
+         call' = [call EXCEPT ![c] = [cmds |-> cs, mayPush |-> may]]
+    /\ resp' = [resp EXCEPT ![c] = NoResp]
+    /\ UNCHANGED <<db, out, credit>>
+
+\* The push takes effect.  A is the set of refs whose command is applied.
+\*   - Nothing is applied without authorization.
+\*   - A command is applied only against the old value it names.  A command
+\*     whose new value equals its old value may be applied; it then confirms
+\*     the value of the ref and changes nothing.
+\*   - Every other submitted command is reported rejected and has no effect.
+\*   - A push that changes no ref changes nothing, and the published state
+\*     stays attributed to whoever it was attributed to before.
+Linearize(c) ==
+    /\ call[c] # NoCall
+    /\ out[c] = NoOut
+    /\ LET cs   == call[c].cmds
+           Sent == {r \in Refs : cs[r] # NoCmd}
+       IN \E A \in SUBSET Sent :
+            /\ A # {} => call[c].mayPush
+            /\ \A r \in A : cs[r].old = CurRefs[r]
+            /\ LET newRefs == [r \in Refs |-> IF r \in A THEN cs[r].new ELSE CurRefs[r]]
+               IN \E newHead \in HeadChoices(newRefs, CurHead) :
+                  /\ out' = [out EXCEPT ![c] =
+                               [r \in Refs |-> IF r \in A THEN "ok"
+                                               ELSE IF r \in Sent THEN "ng"
+                                               ELSE "none"]]
+                  /\ IF newRefs = CurRefs
+                     THEN db' = db /\ credit' = credit
+                     ELSE /\ db' = [refs |-> newRefs, head |-> newHead]
+                          /\ credit' = Entry(c, newRefs, newHead)
+    /\ UNCHANGED <<call, resp>>
+
+\* The client is answered.  It may be told the exact outcome, told nothing
+\* (a client that did not ask for a status report), or given an error.  It is
+\* told an outcome only if the push linearized, and then only the true one.
+Respond(c) ==
+    /\ call[c] # NoCall
+    /\ \E answer \in {Error} \cup (IF out[c] = NoOut THEN {} ELSE {out[c], NoReport}) :
+         resp' = [resp EXCEPT ![c] = answer]
+    /\ call' = [call EXCEPT ![c] = NoCall]
+    /\ out'  = [out  EXCEPT ![c] = NoOut]
+    /\ UNCHANGED <<db, credit>>
+
+\* The default branch is changed to an existing branch.
+SetHead ==
+    /\ db # Absent
+    /\ \E h \in Refs :
+         /\ db.refs[h] # NoOid
+         /\ h # db.head
+         /\ db' = [db EXCEPT !.head = h]
+         /\ credit' = Entry(Manager, db.refs, h)
+    /\ UNCHANGED <<call, out, resp>>
+
+Next ==
+    \/ Create
+    \/ SetHead
+    \/ \E c \in Clients : Invoke(c) \/ Linearize(c) \/ Respond(c)
+
+Spec == Init /\ [][Next]_vars
+
+-----------------------------------------------------------------------------
+\* Consequences of the specification, checked on this module by GitRefDB.cfg.
+\* They are properties of the specification, so they hold of every system
+\* that refines it.
+
+\* A push that has applied a command was authorized.
+AppliedWasAuthorized ==
+    \A c \in Clients :
+        (out[c] # NoOut /\ \E r \in Refs : out[c][r] = "ok") => call[c].mayPush
+
+\* The published state is attributed to the operation that produced it.
+CreditMatchesState ==
+    db # Absent => (credit # NoEntry /\ credit.refs = db.refs /\ credit.head = db.head)
+
+\* A client is told an outcome only for a push that took effect, and then
+\* only the true outcome.
+ToldOnlyTheOutcome ==
+    [][\A c \in Clients :
+          (resp'[c] # resp[c] /\ resp'[c] \notin {Error, NoResp})
+              => (out[c] # NoOut /\ resp'[c] \in {out[c], NoReport})]_vars
+
+\* The published HEAD names an existing branch whenever any branch exists.
+HeadNotDangling ==
+    db # Absent =>
+        ((\E r \in Refs : db.refs[r] # NoOid) => db.refs[db.head] # NoOid)
+
+\* A ref changes only in a step that applies a command naming its current
+\* value as the old value.  This is the "no lost update" property.
+NoLostUpdate ==
+    [][\A r \in Refs :
+          CurRefs'[r] # CurRefs[r] =>
+              \E c \in Clients :
+                  /\ call[c] # NoCall
+                  /\ call[c].cmds[r] # NoCmd
+                  /\ call[c].cmds[r].old = CurRefs[r]
+                  /\ call[c].cmds[r].new = CurRefs'[r]]_vars
+=============================================================================
diff --git a/docs/spec/MCGitOnObjectStore.cfg b/docs/spec/MCGitOnObjectStore.cfg
new file mode 100644
index 0000000000..77ea2bea70
--- /dev/null
+++ b/docs/spec/MCGitOnObjectStore.cfg
@@ -0,0 +1,43 @@
+\* The main configuration: two concurrent pushers and the default-branch
+\* setter over two refs.  docs/spec/check.sh derives every other
+\* configuration from this file by substitution; run that script rather than
+\* this file alone.
+SPECIFICATION Spec
+CONSTANTS
+    Clients = {c1, c2}
+    Refs = {main, dev}
+    DefaultHead = main
+    o1 = o1
+    o2 = o2
+    Oids = {o1}
+    NoOid = NoOid
+    Absent = Absent
+    NoCall = NoCall
+    NoOut = NoOut
+    NoCmd = NoCmd
+    NoResp = NoResp
+    Error = Error
+    NoEntry = NoEntry
+    Owner = Owner
+    Manager = Manager
+    NoManifest = NoManifest
+    NoRead = NoRead
+    ObjParents <- MCObjParents
+    CompactAt = 2
+    MaxWrites = 3
+    HasSetter = TRUE
+    HasReader = FALSE
+    StaleClients = FALSE
+    GitMayCrash = TRUE
+    ParentLinks = FALSE
+    Decision = "ground-truth"
+    EtagMode = "content"
+    Faults = {}
+SYMMETRY ClientSymmetry
+VIEW LiveView
+CONSTRAINT Bounded
+INVARIANT StoreInvariants
+INVARIANT NoSilentDrop
+INVARIANT PublishIsAuthorizedChange
+PROPERTY Refines
+PROPERTY ParentIsPredecessor
diff --git a/docs/spec/MCGitOnObjectStore.tla b/docs/spec/MCGitOnObjectStore.tla
new file mode 100644
index 0000000000..df3bdbbb40
--- /dev/null
+++ b/docs/spec/MCGitOnObjectStore.tla
@@ -0,0 +1,49 @@
+------------------------ MODULE MCGitOnObjectStore ------------------------
+(***************************************************************************)
+(* Model-checking instance of GitOnObjectStore.                            *)
+(*                                                                         *)
+(* The object graph has two objects and o2 refers to o1, so a delta pack,  *)
+(* a pack that is missing an ancestor, and compaction all occur.           *)
+(***************************************************************************)
+EXTENDS GitOnObjectStore, TLC
+
+CONSTANTS o1, o2
+
+MCObjParents == [o \in Oids |-> IF o = o2 THEN {o1} \cap Oids ELSE {}]
+ClientSymmetry == Permutations(Clients)
+
+(***************************************************************************)
+(* State identification.  The stores only grow, and most of what they hold *)
+(* is never read again: a manifest staged by a push that lost its race, or *)
+(* one that has since been superseded.  TLC is told to identify two states *)
+(* that differ only in store content that is not read.                     *)
+(*                                                                         *)
+(* Why this loses nothing for the protocol as specified.  The stores are   *)
+(* read in three places: the hydration guard of Begin, and the invariants  *)
+(* Fence and ReaderComplete.  Each reads only the manifests in Read below  *)
+(* (the one the pointer names and the one the reader resolved) and the     *)
+(* packs those manifests list.  Another manifest joins that set only when  *)
+(* a pointer write installs it, and the writing process has stored it and  *)
+(* its packs before that step (Upload, SetBegin, Seed).  So two states     *)
+(* with equal views have the same enabled steps and the same invariant     *)
+(* values, and their successors again have equal views.                    *)
+(*                                                                         *)
+(* Under a seeded fault that argument fails.  With the fault "gc", a pack  *)
+(* staged by a push in progress can be deleted; the view hides the         *)
+(* deletion, and TLC then misses the later pointer write that names the    *)
+(* missing pack.  A view can only hide a violation, never invent one,      *)
+(* because every state TLC explores is reachable.  check.sh therefore runs *)
+(* every seeded-fault configuration without the view, and its check        *)
+(* "no-view" repeats the two-client check of the protocol as specified     *)
+(* without the view.                                                       *)
+(***************************************************************************)
+ReadManifests ==
+    (IF pointer = Absent THEN {} ELSE {pointer.body})
+        \cup (IF rd = NoRead THEN {} ELSE {rd})
+
+LiveView ==
+    <<pointer, mstore \cap ReadManifests,
+      pstore \cap UNION {m.packs : m \in ReadManifests},
+      writes, pc, base, call, stat, staged, lin, resp,
+      spc, sbase, starget, rd, credit>>
+=============================================================================
diff --git a/docs/spec/check.sh b/docs/spec/check.sh
new file mode 100755
index 0000000000..2e3f5a4eec
--- /dev/null
+++ b/docs/spec/check.sh
@@ -0,0 +1,196 @@
+#!/usr/bin/env bash
+# Model-checks the Git-on-object-storage protocol (docs/git-on-object-storage.md).
+#
+#   docs/spec/check.sh            run the whole suite
+#   docs/spec/check.sh NAME...    run only the named checks; a name that is
+#                                 not a check is an error (exit status 2)
+#
+# The suite has two halves.  The protocol as specified must satisfy every
+# property.  Each seeded design error must violate the property named for it;
+# a seeded error that goes undetected fails the suite, because it would mean
+# the properties do not constrain that part of the design.
+# A last check asserts that a behavior of interest never occurs and must be
+# violated too, which shows the model reaches that behavior.
+#
+# Environment:
+#   TLA2TOOLS_JAR   path to tla2tools.jar (default: downloaded next to this file)
+#   TLC_OUT         directory for TLC output and counterexamples (default: temp)
+#   TLC_WORKERS     TLC worker threads (default: auto)
+set -euo pipefail
+
+here=$(cd "$(dirname "$0")" && pwd)
+
+# Reject names that are not checks before doing any work.  Otherwise a
+# misspelled name selects nothing and the run reports success without having
+# checked anything.  The names are read from the `check` lines of this file.
+known=$({ echo refdb; sed -nE 's/^check +([a-z0-9-]+) .*/\1/p' "$here/$(basename "$0")"; })
+for name in "$@"; do
+  if ! printf '%s\n' "$known" | grep -qxF -- "$name"; then
+    echo "error: unknown check '$name'" >&2
+    echo "known checks: $(printf '%s' "$known" | tr '\n' ' ')" >&2
+    exit 2
+  fi
+done
+cd "$here"
+
+TLC_VERSION=1.7.4
+TLC_SHA256=936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88
+jar=${TLA2TOOLS_JAR:-$here/tla2tools.jar}
+out=${TLC_OUT:-$(mktemp -d "${TMPDIR:-/tmp}/buzz-tlc.XXXXXX")}
+workers=${TLC_WORKERS:-auto}
+mkdir -p "$out"
+
+sha256() {
+  if command -v sha256sum >/dev/null 2>&1; then sha256sum "$1" | cut -d' ' -f1
+  else shasum -a 256 "$1" | cut -d' ' -f1; fi
+}
+
+if [ ! -f "$jar" ]; then
+  echo "fetching TLC $TLC_VERSION"
+  curl -fsSL -o "$jar.part" \
+    "https://github.com/tlaplus/tlaplus/releases/download/v$TLC_VERSION/tla2tools.jar"
+  mv "$jar.part" "$jar"
+fi
+if [ "$(sha256 "$jar")" != "$TLC_SHA256" ]; then
+  echo "error: $jar is not TLC $TLC_VERSION (sha256 mismatch)" >&2
+  exit 2
+fi
+
+failures=0
+selected=("$@")
+
+wanted() {
+  [ ${#selected[@]} -eq 0 ] && return 0
+  local n
+  for n in "${selected[@]}"; do [ "$n" = "$1" ] && return 0; done
+  return 1
+}
+
+# tlc NAME MODULE CONFIG -> writes $out/NAME.txt, prints "<verdict> <states>"
+#   verdict: "pass", "violated:<property>", or "error"
+tlc() {
+  local name=$1 module=$2 config=$3 log="$out/$1.txt" verdict states
+  java -XX:+UseParallelGC -cp "$jar" tlc2.TLC -workers "$workers" -deadlock \
+    -metadir "$out/$name.meta" -config "$config" "$module" >"$log" 2>&1 || true
+  rm -rf "$out/$name.meta"
+  if grep -q "Model checking completed. No error has been found." "$log"; then
+    verdict=pass
+  elif grep -q "Error: Invariant .* is violated" "$log"; then
+    verdict="violated:$(sed -n 's/^Error: Invariant \(.*\) is violated.*/\1/p' "$log" | head -1)"
+  elif grep -q "Error: Action property .* of module GitRefDB is violated" "$log"; then
+    # The refinement: a step that is not a step of the abstract specification.
+    verdict="violated:Refines"
+  elif grep -q "Error: Action property .* is violated" "$log"; then
+    verdict="violated:$(sed -n 's/^Error: Action property \(.*\) is violated.*/\1/p' "$log" | head -1)"
+  else
+    verdict=error
+  fi
+  states=$(sed -n 's/^\([0-9,]*\) states generated, \([0-9,]*\) distinct states found.*/\2/p' "$log" | tail -1)
+  echo "$verdict ${states:-?}"
+}
+
+# check NAME EXPECT [sed-expression...]
+#   EXPECT is "pass" or the property the configuration must violate.
+#   The sed expressions rewrite MCGitOnObjectStore.cfg into this configuration.
+check() {
+  local name=$1 expect=$2 cfg="$out/$1.cfg" e result verdict states start
+  local args=(-e '/^\\\*/d') # drop the comment header of the base configuration
+  shift 2
+  wanted "$name" || return 0
+  for e in "$@"; do args+=(-e "$e"); done
+  if [ "$expect" != pass ]; then
+    # Check only the property this seeded error is expected to violate, so
+    # the verdict names it whatever else the error also breaks.  The state
+    # view is dropped: its justification (MCGitOnObjectStore.tla) holds for
+    # the protocol as specified, and under a seeded error it can hide the
+    # violation (it hides a deleted pack that no manifest in use lists yet).
+    args+=(-e '/^INVARIANT /d' -e '/^PROPERTY /d' -e '/^VIEW /d')
+  fi
+  sed "${args[@]}" MCGitOnObjectStore.cfg >"$cfg"
+  case "$expect" in
+    pass) ;;
+    Refines | ParentIsPredecessor) echo "PROPERTY $expect" >>"$cfg" ;;
+    *) echo "INVARIANT $expect" >>"$cfg" ;;
+  esac
+  start=$(date +%s)
+  result=$(tlc "$name" MCGitOnObjectStore.tla "$cfg")
+  verdict=${result% *}; states=${result#* }
+  report "$name" "$expect" "$verdict" "$states" $(( $(date +%s) - start ))
+}
+
+report() {
+  local name=$1 expect=$2 verdict=$3 states=$4 secs=$5 want status
+  if [ "$expect" = pass ]; then want=pass; else want="violated:$expect"; fi
+  if [ "$verdict" = "$want" ]; then status=ok; else status=FAIL; failures=$((failures + 1)); fi
+  printf '%-4s %-22s expected %-34s got %-34s %12s states %4ss\n' \
+    "$status" "$name" "$want" "$verdict" "$states" "$secs"
+}
+
+# Substitutions.
+ONE_CLIENT='s/Clients = {c1, c2}/Clients = {c1}/'
+THREE_CLIENTS='s/Clients = {c1, c2}/Clients = {c1, c2, c3}/'
+ONE_REF='s/Refs = {main, dev}/Refs = {main}/'
+TWO_OBJECTS='s/Oids = {o1}/Oids = {o1, o2}/'
+NO_SETTER='s/HasSetter = TRUE/HasSetter = FALSE/'
+READER='s/HasReader = FALSE/HasReader = TRUE/'
+STALE='s/StaleClients = FALSE/StaleClients = TRUE/'
+PARENT='s/ParentLinks = FALSE/ParentLinks = TRUE/'
+VERSION='s/EtagMode = "content"/EtagMode = "version"/'
+CONSTANT_ETAG='s/EtagMode = "content"/EtagMode = "constant"/'
+LEGACY='s/Decision = "ground-truth"/Decision = "legacy"/'
+REPORT='s/Decision = "ground-truth"/Decision = "report"/'
+NO_VIEW='/^VIEW /d'
+NO_CRASH='s/GitMayCrash = TRUE/GitMayCrash = FALSE/'
+fault() { echo "s/Faults = {}/Faults = {\"$1\"}/"; }
+
+echo "TLC output: $out"
+echo
+echo "The abstract specification"
+if wanted refdb; then
+  start=$(date +%s)
+  result=$(tlc refdb GitRefDB.tla GitRefDB.cfg)
+  report refdb pass "${result% *}" "${result#* }" $(( $(date +%s) - start ))
+fi
+
+echo
+echo "The protocol as specified (must satisfy every property)"
+check push            pass
+check objects         pass "$ONE_CLIENT" "$TWO_OBJECTS" "$NO_SETTER" "$READER"
+check three-clients   pass "$THREE_CLIENTS" "$ONE_REF" "$NO_SETTER"
+check stale-commands  pass "$ONE_CLIENT" "$STALE" "$TWO_OBJECTS" "$NO_SETTER"
+check parent-links    pass "$PARENT" "$NO_SETTER"
+check version-etag    pass "$VERSION" "$NO_SETTER"
+check no-view         pass "$NO_VIEW" "$NO_SETTER"
+
+echo
+echo "Seeded design errors (each must violate the property named)"
+check legacy-unauthorized  PublishIsAuthorizedChange "$LEGACY" "$NO_SETTER" "$NO_CRASH"
+check legacy-silent-drop   NoSilentDrop              "$LEGACY" "$NO_SETTER" "$NO_CRASH"
+check legacy-crash-drop    NoSilentDrop              "$LEGACY" "$NO_SETTER"
+check legacy-refinement    Refines                   "$LEGACY" "$NO_SETTER"
+check report-unauthorized  PublishIsAuthorizedChange "$REPORT" "$NO_SETTER" "$NO_CRASH"
+check report-crash-drop    NoSilentDrop              "$REPORT" "$NO_SETTER"
+check report-refinement    Refines                   "$REPORT" "$NO_SETTER"
+check no-hook              PublishIsAuthorizedChange "$(fault no-hook)" "$NO_SETTER"
+check no-cas-guard         Refines                   "$(fault no-cas-guard)" "$NO_SETTER"
+check stale-base           Refines                   "$(fault stale-base)" "$NO_SETTER"
+check stale-base-chain     ParentIsPredecessor       "$(fault stale-base)" "$NO_SETTER" "$PARENT"
+check constant-etag        Refines                   "$CONSTANT_ETAG" "$NO_SETTER"
+check constant-etag-setter Refines                   "$CONSTANT_ETAG" "$ONE_CLIENT"
+check ack-before-cas       Refines                   "$(fault ack-before-cas)" "$NO_SETTER"
+check cas-before-upload    Fence                     "$(fault cas-before-upload)" "$NO_SETTER"
+check gc-pending-upload    Fence                     "$(fault gc)" "$ONE_CLIENT" "$TWO_OBJECTS" "$NO_SETTER"
+check gc-reader            ReaderComplete            "$(fault gc)" "$ONE_CLIENT" "$TWO_OBJECTS" "$NO_SETTER" "$READER"
+check drop-parent-packs    PublishedClosed           "$(fault drop-parent-packs)" "$ONE_CLIENT" "$TWO_OBJECTS" "$NO_SETTER"
+check no-connectivity      PublishedClosed           "$(fault no-connectivity)" "$ONE_CLIENT" "$TWO_OBJECTS" "$NO_SETTER"
+
+echo
+echo "Coverage (a behavior of the protocol as specified that must be reachable)"
+check relayed-ok           NeverRelaysOk             "$NO_SETTER"
+
+echo
+if [ "$failures" -ne 0 ]; then
+  echo "$failures check(s) did not give the expected result; see $out"
+  exit 1
+fi
+echo "all checks gave the expected result"
diff --git a/docs/spec/lean/.gitignore b/docs/spec/lean/.gitignore
new file mode 100644
index 0000000000..bfb30ec8c7
--- /dev/null
+++ b/docs/spec/lean/.gitignore
@@ -0,0 +1 @@
+/.lake
diff --git a/docs/spec/lean/GitPointer.lean b/docs/spec/lean/GitPointer.lean
new file mode 100644
index 0000000000..daa9c04b04
--- /dev/null
+++ b/docs/spec/lean/GitPointer.lean
@@ -0,0 +1,374 @@
+/-!
+# Conditional pointer writes for Git on an object store
+
+This file proves four safety properties of the storage protocol that
+`../GitOnObjectStore.tla` checks with TLC for small finite instances. The
+proofs here hold for any number of clients, refs, objects and packs. Only core
+Lean is used.
+
+## What is modeled
+
+A repository is stored as immutable manifests and packs plus one mutable
+pointer that names the current manifest. A writer reads the pointer (`begin`),
+stages a successor manifest computed from the value it read, uploads that
+manifest and its packs (`upload`), and then performs a conditional write of
+the pointer (`cas`), which succeeds only if the ETag of the pointer equals the
+ETag of the value the writer read. A writer may stop at any time (`abort`): a
+lost race, a crash, or a timeout. Writers interleave arbitrarily.
+
+`Model.Staged` is the set of manifests a writer may stage from a pointer value
+`p`: the manifest records `p` as its parent, its ref state is a legal successor
+of the ref state of `p`, and its pack list follows one of three rules (no new
+pack, one delta pack added to the packs of `p`, or one pack that replaces them
+all).
+
+Two fields are ghost state, used only to state the results: `State.writes`
+counts successful pointer writes, and `Writer.readAt` records the value of that
+counter when the writer read the pointer.
+
+## Assumptions
+
+* `Model.etag_inj`: the ETag of a pointer body determines the body. This
+  stands for two facts about the implementation: the object store assigns
+  different ETags to different bodies, and SHA-256 has no collision among the
+  values that occur.
+* A digest is modeled by the value it names. `Manifest.parent` therefore holds
+  the predecessor manifest itself, and the predecessor chain is finite because
+  `Manifest` is an inductive type.
+* Nothing is removed from the manifest store or the pack store. Garbage
+  collection is outside this model.
+* `Model.Legal`, `Model.reach` and `Model.objs` are arbitrary relations.
+  Nothing is assumed about which ref updates are legal or which objects a ref
+  state reaches.
+
+## Results (for every reachable state)
+
+* `fence`: the manifest the pointer names is stored, and so is every pack that
+  manifest lists.
+* `closed`: the packs listed by the pointed-to manifest contain every object
+  reachable from its ref state. This is derived from the three pack rules.
+* `pointer_step_legal`: a step either leaves the pointer unchanged or replaces
+  it by a manifest whose parent is the replaced value and whose ref state is a
+  legal successor of the replaced ref state. No update is lost.
+* `cas_sees_no_intervening_write`: when a conditional write is enabled, no
+  pointer write has happened since the writer read the pointer, although the
+  ETag depends only on the body.
+* `pointer_depth_eq_writes`: the length of the predecessor chain of the pointer
+  equals the number of pointer writes, so a published manifest is never
+  published again.
+
+`write_is_possible` exhibits an instance in which a conditional write
+succeeds, so the results are not vacuous.
+
+## What is not covered
+
+The proofs concern the pointer discipline only. The decision whether a push is
+published, the reports sent to clients, the default-branch setter, readers and
+garbage collection are covered by the TLA+ model for finite instances and are
+not formalized here. `Model.Legal` stands for everything `git receive-pack` and
+the push policy permit; this file does not say what that is.
+-/
+
+namespace GitPointer
+
+/-- A manifest: a published ref state, the set of packs that hold its objects,
+and the manifest it replaced (`none` for the first manifest of a repository). -/
+structure Manifest (R Pk : Type) where
+  refs : R
+  packs : Pk → Prop
+  parent : Option (Manifest R Pk)
+
+variable {R Obj Pk Client E : Type}
+
+/-- The length of the predecessor chain of a manifest, counting the manifest. -/
+def Manifest.depth : Manifest R Pk → Nat
+  | ⟨_, _, none⟩ => 1
+  | ⟨_, _, some p⟩ => p.depth + 1
+
+/-- The depth of a pointer value; an absent pointer has depth 0. -/
+def depthOpt : Option (Manifest R Pk) → Nat
+  | none => 0
+  | some m => m.depth
+
+theorem Manifest.depth_eq (m : Manifest R Pk) : m.depth = depthOpt m.parent + 1 := by
+  cases m with
+  | mk r p par => cases par <;> simp [Manifest.depth, depthOpt]
+
+/-- The parameters of the protocol. `objs pk o`: pack `pk` contains object `o`.
+`reach r o`: object `o` is reachable from ref state `r`. `Legal b r`: ref state
+`r` may follow base `b`, where `none` is a repository that does not exist.
+`etag` is the ETag of a pointer body, assumed to determine the body. -/
+structure Model (R Obj Pk E : Type) where
+  objs : Pk → Obj → Prop
+  reach : R → Obj → Prop
+  Legal : Option R → R → Prop
+  etag : Manifest R Pk → E
+  etag_inj : ∀ a b, etag a = etag b → a = b
+
+/-- The local state of a writer: the pointer value it read, the manifest it
+staged, whether it has uploaded that manifest, and (ghost) the write count at
+the time of its read. -/
+structure Writer (R Pk : Type) where
+  base : Option (Manifest R Pk)
+  staged : Manifest R Pk
+  uploaded : Bool
+  readAt : Nat
+
+/-- The global state: the pointer, the manifest store, the pack store, the
+writers in progress, and (ghost) the number of successful pointer writes. -/
+structure State (R Pk Client : Type) where
+  pointer : Option (Manifest R Pk)
+  mstore : Manifest R Pk → Prop
+  pstore : Pk → Prop
+  writers : Client → Option (Writer R Pk)
+  writes : Nat
+
+/-- The initial state: no pointer, empty stores, no writers. -/
+def State.init : State R Pk Client :=
+  ⟨none, fun _ => False, fun _ => False, fun _ => none, 0⟩
+
+/-- `pk` is listed by the manifest `p` names. False when `p` is absent. -/
+def basePacks (p : Option (Manifest R Pk)) (pk : Pk) : Prop :=
+  ∃ b, p = some b ∧ b.packs pk
+
+/-- `g` is `f` with the entry of client `c` replaced by `v`. Stated as a
+relation so that equality of clients need not be decidable. -/
+def Upd (f : Client → Option (Writer R Pk)) (c : Client) (v : Option (Writer R Pk))
+    (g : Client → Option (Writer R Pk)) : Prop :=
+  g c = v ∧ ∀ c', c' ≠ c → g c' = f c'
+
+/-- A writer present after an update is the new entry or was present before. -/
+theorem Upd.cases {f g : Client → Option (Writer R Pk)} {c : Client} {v : Option (Writer R Pk)}
+    (h : Upd f c v g) {c' : Client} {w : Writer R Pk} (hw : g c' = some w) :
+    v = some w ∨ f c' = some w := by
+  rcases Classical.em (c' = c) with rfl | hne
+  · exact Or.inl (h.1.symm.trans hw)
+  · exact Or.inr ((h.2 c' hne).symm.trans hw)
+
+variable (M : Model R Obj Pk E)
+
+/-- `o` is reachable from the ref state of the manifest `p` names. -/
+def Model.baseReach (p : Option (Manifest R Pk)) (o : Obj) : Prop :=
+  ∃ b, p = some b ∧ M.reach b.refs o
+
+/-- The manifests a writer may stage after reading pointer value `p`. -/
+def Model.Staged (p : Option (Manifest R Pk)) (m : Manifest R Pk) : Prop :=
+  m.parent = p ∧ M.Legal (p.map Manifest.refs) m.refs ∧
+  (-- no new pack
+   ((∀ o, M.reach m.refs o → M.baseReach p o) ∧ ∀ pk, m.packs pk ↔ basePacks p pk) ∨
+   -- delta pack
+   (∃ d, (∀ o, M.reach m.refs o → M.baseReach p o ∨ M.objs d o) ∧
+      ∀ pk, m.packs pk ↔ (basePacks p pk ∨ pk = d)) ∨
+   -- compaction
+   (∃ f, (∀ o, M.reach m.refs o → M.objs f o) ∧ ∀ pk, m.packs pk ↔ pk = f))
+
+/-- The packs a manifest lists contain every object reachable from its refs. -/
+def Model.Closed (m : Manifest R Pk) : Prop :=
+  ∀ o, M.reach m.refs o → ∃ pk, m.packs pk ∧ M.objs pk o
+
+/-- The steps of the protocol. Each constructor lists its enabling conditions;
+the post-state is the pre-state with the named fields replaced. -/
+inductive Model.Step : State R Pk Client → State R Pk Client → Prop
+  /-- Client `c` reads the pointer and stages a manifest `m`. -/
+  | begin (s : State R Pk Client) (c : Client) (m : Manifest R Pk) (ws) :
+      s.writers c = none → M.Staged s.pointer m →
+      Upd s.writers c (some ⟨s.pointer, m, false, s.writes⟩) ws →
+      Model.Step s { s with writers := ws }
+  /-- Client `c` stores its staged manifest and the packs it lists. -/
+  | upload (s : State R Pk Client) (c : Client) (w : Writer R Pk) (ws) :
+      s.writers c = some w →
+      Upd s.writers c (some { w with uploaded := true }) ws →
+      Model.Step s { s with
+        mstore := fun x => s.mstore x ∨ x = w.staged
+        pstore := fun pk => s.pstore pk ∨ w.staged.packs pk
+        writers := ws }
+  /-- The conditional write. The comparison is on `Option E`, so an absent
+  pointer matches only an absent base (`If-None-Match: *`). -/
+  | cas (s : State R Pk Client) (c : Client) (w : Writer R Pk) (ws) :
+      s.writers c = some w → w.uploaded = true →
+      s.pointer.map M.etag = w.base.map M.etag →
+      Upd s.writers c none ws →
+      Model.Step s { s with pointer := some w.staged, writes := s.writes + 1, writers := ws }
+  /-- Client `c` stops: a lost race, a crash, or a timeout. -/
+  | abort (s : State R Pk Client) (c : Client) (w : Writer R Pk) (ws) :
+      s.writers c = some w → Upd s.writers c none ws →
+      Model.Step s { s with writers := ws }
+
+/-- The states reachable from the initial state by finitely many steps. -/
+inductive Model.Reachable : State R Pk Client → Prop
+  | init : Model.Reachable State.init
+  | step {s s' : State R Pk Client} : Model.Reachable s → M.Step s s' → Model.Reachable s'
+
+/-! ## Auxiliary lemmas and the inductive invariant -/
+
+/-- A manifest staged from a closed base is closed. This is where the three
+pack rules are used. -/
+theorem Model.Staged.closed {p : Option (Manifest R Pk)} {m : Manifest R Pk}
+    (h : M.Staged p m) (hp : ∀ b, p = some b → M.Closed b) : M.Closed m := by
+  intro o ho
+  have base : M.baseReach p o → ∃ pk, basePacks p pk ∧ M.objs pk o := by
+    rintro ⟨b, rfl, hb⟩
+    obtain ⟨pk, hpk, hobj⟩ := hp b rfl o hb
+    exact ⟨pk, ⟨b, rfl, hpk⟩, hobj⟩
+  rcases h.2.2 with ⟨hr, hpk⟩ | ⟨d, hr, hpk⟩ | ⟨f, hr, hpk⟩
+  · obtain ⟨pk, h1, h2⟩ := base (hr o ho)
+    exact ⟨pk, (hpk pk).2 h1, h2⟩
+  · rcases hr o ho with hb | hd
+    · obtain ⟨pk, h1, h2⟩ := base hb
+      exact ⟨pk, (hpk pk).2 (Or.inl h1), h2⟩
+    · exact ⟨d, (hpk d).2 (Or.inr rfl), hd⟩
+  · exact ⟨f, (hpk f).2 rfl, hr o ho⟩
+
+/-- Equal ETags (as `Option E`) imply equal pointer values, by `etag_inj`. -/
+theorem Model.eq_of_etag_eq {p q : Option (Manifest R Pk)}
+    (h : p.map M.etag = q.map M.etag) : p = q := by
+  cases p <;> cases q <;> simp at h
+  · rfl
+  · exact congrArg some (M.etag_inj _ _ h)
+
+/-- The invariant of one writer: its staged manifest was computed from its
+base, its base is closed, the depth of its base is the write count it read,
+and once it has uploaded, its staged manifest and packs are stored. -/
+structure Model.WriterInv (s : State R Pk Client) (w : Writer R Pk) : Prop where
+  staged : M.Staged w.base w.staged
+  baseClosed : ∀ b, w.base = some b → M.Closed b
+  readAt : depthOpt w.base = w.readAt
+  stored : w.uploaded = true → s.mstore w.staged ∧ ∀ pk, w.staged.packs pk → s.pstore pk
+
+/-- The inductive invariant of the protocol. -/
+structure Model.Inv (s : State R Pk Client) : Prop where
+  fence : ∀ m, s.pointer = some m → s.mstore m ∧ ∀ pk, m.packs pk → s.pstore pk
+  closed : ∀ m, s.pointer = some m → M.Closed m
+  depth : depthOpt s.pointer = s.writes
+  writers : ∀ c w, s.writers c = some w → M.WriterInv s w
+
+/-- The writer invariant survives any step that only adds to the stores. -/
+theorem Model.WriterInv.mono {s s' : State R Pk Client} {w : Writer R Pk}
+    (h : M.WriterInv s w) (hm : ∀ x, s.mstore x → s'.mstore x)
+    (hp : ∀ pk, s.pstore pk → s'.pstore pk) : M.WriterInv s' w :=
+  ⟨h.staged, h.baseClosed, h.readAt, fun hu =>
+    ⟨hm _ (h.stored hu).1, fun pk hpk => hp pk ((h.stored hu).2 pk hpk)⟩⟩
+
+theorem Model.Inv.init : M.Inv (State.init : State R Pk Client) :=
+  ⟨fun _ h => (nomatch h), fun _ h => (nomatch h), rfl, fun _ _ h => (nomatch h)⟩
+
+theorem Model.Inv.step {s s' : State R Pk Client} (inv : M.Inv s) (st : M.Step s s') :
+    M.Inv s' := by
+  cases st with
+  | begin c m ws hc hm hu =>
+    refine ⟨inv.fence, inv.closed, inv.depth, fun c' w' hw' => ?_⟩
+    rcases hu.cases hw' with hnew | hold
+    · cases hnew
+      exact ⟨hm, inv.closed, inv.depth, fun h => nomatch h⟩
+    · exact (inv.writers c' w' hold).mono M (fun _ h => h) (fun _ h => h)
+  | upload c w ws hc hu =>
+    refine ⟨fun m hm => ?_, inv.closed, inv.depth, fun c' w' hw' => ?_⟩
+    · exact ⟨Or.inl (inv.fence m hm).1, fun pk h => Or.inl ((inv.fence m hm).2 pk h)⟩
+    · rcases hu.cases hw' with hnew | hold
+      · cases hnew
+        have hw := inv.writers c w hc
+        exact ⟨hw.staged, hw.baseClosed, hw.readAt, fun _ => ⟨Or.inr rfl, fun _ h => Or.inr h⟩⟩
+      · exact (inv.writers c' w' hold).mono M (fun _ h => Or.inl h) (fun _ h => Or.inl h)
+  | cas c w ws hc hup he hu =>
+    have hw := inv.writers c w hc
+    have hbase : s.pointer = w.base := M.eq_of_etag_eq he
+    refine ⟨fun m hm => ?_, fun m hm => ?_, ?_, fun c' w' hw' => ?_⟩
+    · cases hm
+      exact hw.stored hup
+    · cases hm
+      exact hw.staged.closed M hw.baseClosed
+    · show w.staged.depth = s.writes + 1
+      rw [w.staged.depth_eq, hw.staged.1, ← hbase, inv.depth]
+    · rcases hu.cases hw' with hnew | hold
+      · cases hnew
+      · exact (inv.writers c' w' hold).mono M (fun _ h => h) (fun _ h => h)
+  | abort c w ws hc hu =>
+    refine ⟨inv.fence, inv.closed, inv.depth, fun c' w' hw' => ?_⟩
+    rcases hu.cases hw' with hnew | hold
+    · cases hnew
+    · exact (inv.writers c' w' hold).mono M (fun _ h => h) (fun _ h => h)
+
+/-- Every reachable state satisfies the invariant. -/
+theorem Model.Reachable.inv {s : State R Pk Client} (hs : M.Reachable s) : M.Inv s := by
+  induction hs with
+  | init => exact Model.Inv.init M
+  | step _ st ih => exact ih.step M st
+
+/-! ## Main results -/
+
+/-- The pointer names only what is stored: the manifest it names is in the
+manifest store, and every pack that manifest lists is in the pack store. -/
+theorem fence {s : State R Pk Client} (hs : M.Reachable s) {m : Manifest R Pk}
+    (hm : s.pointer = some m) : s.mstore m ∧ ∀ pk, m.packs pk → s.pstore pk :=
+  hs.inv.fence m hm
+
+/-- The packs listed by the pointed-to manifest contain every object reachable
+from its ref state. -/
+theorem closed {s : State R Pk Client} (hs : M.Reachable s) {m : Manifest R Pk}
+    (hm : s.pointer = some m) : ∀ o, M.reach m.refs o → ∃ pk, m.packs pk ∧ M.objs pk o :=
+  hs.inv.closed m hm
+
+/-- Every step from a reachable state leaves the pointer unchanged or replaces
+it by a manifest whose parent is the replaced value and whose ref state is a
+legal successor of the replaced ref state. Each change of the published ref
+state is thus one step of an atomic ref database, computed against the state
+it replaces. -/
+theorem pointer_step_legal {s s' : State R Pk Client} (hs : M.Reachable s) (st : M.Step s s') :
+    s'.pointer = s.pointer ∨
+    ∃ m, s'.pointer = some m ∧ m.parent = s.pointer ∧
+      M.Legal (s.pointer.map Manifest.refs) m.refs := by
+  cases st with
+  | begin => exact Or.inl rfl
+  | upload => exact Or.inl rfl
+  | abort => exact Or.inl rfl
+  | cas c w ws hc hup he hu =>
+    have hw := hs.inv.writers c w hc
+    have hbase : s.pointer = w.base := M.eq_of_etag_eq he
+    exact Or.inr ⟨w.staged, rfl, hbase ▸ hw.staged.1, hbase ▸ hw.staged.2.1⟩
+
+/-- The length of the predecessor chain of the pointer equals the number of
+pointer writes. Each write therefore publishes a manifest of a depth that no
+earlier published manifest had. -/
+theorem pointer_depth_eq_writes {s : State R Pk Client} (hs : M.Reachable s) :
+    depthOpt s.pointer = s.writes :=
+  hs.inv.depth
+
+/-- If the conditional write of writer `w` is enabled in a reachable state (the
+three hypotheses are the enabling conditions of `Model.Step.cas`), then no
+pointer write has happened since `w` read the pointer. -/
+theorem cas_sees_no_intervening_write {s : State R Pk Client} (hs : M.Reachable s)
+    {c : Client} {w : Writer R Pk} (hc : s.writers c = some w) (_hup : w.uploaded = true)
+    (he : s.pointer.map M.etag = w.base.map M.etag) : w.readAt = s.writes := by
+  have hw := hs.inv.writers c w hc
+  rw [← hw.readAt, ← M.eq_of_etag_eq he, hs.inv.depth]
+
+/-! ## Non-vacuity -/
+
+/-- The enabling conditions can be met: there is an instance of the model in
+which a writer reads the absent pointer, uploads, and wins the conditional
+write. The results above therefore do not hold merely because no pointer write
+is ever possible. -/
+theorem write_is_possible :
+    ∃ (M : Model Unit Unit Unit (Manifest Unit Unit)) (s : State Unit Unit Unit),
+      M.Reachable s ∧ s.writes = 1 ∧ s.pointer ≠ none := by
+  let M : Model Unit Unit Unit (Manifest Unit Unit) :=
+    ⟨fun _ _ => True, fun _ _ => True, fun _ _ => True, id, fun _ _ h => h⟩
+  let m : Manifest Unit Unit := ⟨(), fun _ => True, none⟩
+  have upd : ∀ (f : Unit → Option (Writer Unit Unit)) v, Upd f () v (fun _ => v) :=
+    fun _ _ => ⟨rfl, fun _ h => absurd rfl h⟩
+  have staged : M.Staged none m :=
+    ⟨rfl, trivial, Or.inr (Or.inr ⟨(), fun _ _ => trivial, fun _ => ⟨fun _ => rfl, fun _ => trivial⟩⟩)⟩
+  have s1 := Model.Reachable.step Model.Reachable.init
+    (Model.Step.begin (M := M) State.init () m _ rfl staged (upd _ _))
+  have s2 := Model.Reachable.step s1 (Model.Step.upload _ () _ _ rfl (upd _ _))
+  have s3 := Model.Reachable.step s2 (Model.Step.cas _ () _ _ rfl rfl rfl (upd _ _))
+  exact ⟨M, _, s3, rfl, fun h => nomatch h⟩
+
+end GitPointer
+
+#print axioms GitPointer.fence
+#print axioms GitPointer.closed
+#print axioms GitPointer.pointer_step_legal
+#print axioms GitPointer.cas_sees_no_intervening_write
+#print axioms GitPointer.pointer_depth_eq_writes
+#print axioms GitPointer.write_is_possible
diff --git a/docs/spec/lean/lake-manifest.json b/docs/spec/lean/lake-manifest.json
new file mode 100644
index 0000000000..e829f6ea5e
--- /dev/null
+++ b/docs/spec/lean/lake-manifest.json
@@ -0,0 +1,6 @@
+{"version": "1.2.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "gitpointer",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/docs/spec/lean/lakefile.toml b/docs/spec/lean/lakefile.toml
new file mode 100644
index 0000000000..3757b68e95
--- /dev/null
+++ b/docs/spec/lean/lakefile.toml
@@ -0,0 +1,5 @@
+name = "gitpointer"
+defaultTargets = ["GitPointer"]
+
+[[lean_lib]]
+name = "GitPointer"
diff --git a/docs/spec/lean/lean-toolchain b/docs/spec/lean/lean-toolchain
new file mode 100644
index 0000000000..a8afa7d1b0
--- /dev/null
+++ b/docs/spec/lean/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.33.1
diff --git a/scripts/run-tests.sh b/scripts/run-tests.sh
index 917c0e4c3f..659ff9cf3e 100755
--- a/scripts/run-tests.sh
+++ b/scripts/run-tests.sh
@@ -457,6 +457,12 @@ run_unit_tests() {
   run_test_step "buzz-relay Git object-store and conformance-probe tests" \
     cargo test -p buzz-relay --lib api::git::store:: -- --nocapture
 
+  run_test_step "buzz-relay Git push publish-decision tests" \
+    cargo test -p buzz-relay --lib api::git::cas_publish::tests:: -- --nocapture
+
+  run_test_step "buzz-relay Git push track C tests" \
+    cargo test -p buzz-relay --lib api::git::transport::track_c_tests:: -- --nocapture
+
   run_test_step "buzz-relay NIP-FI upgrade tests" \
     cargo test -p buzz-relay --lib nip_fi_upgrade:: -- --nocapture