TLA+ protocol expansion for Where

.agents/development-tools.json

@@ -0,0 +1,7 @@
+{
+  "TLA+ Tools": {
+    "repo": "tlaplus/tlaplus",
+    "ref": "5a47802b5c391f59ecdd44117981f4ff8c0656ba",
+    "version": "1.7.4"
+  }
+}

.agents/skills/tla-verify-protocol/SKILL.md

@@ -92,10 +92,15 @@ convention. In this repository, prefer a feature-level
 - the `.tla` module;
 - configurations for the relevant current, negative-control, and candidate
   designs;
-- a local executable checker;
+- a `manifest.json` declaring each TLC case and its pass/fail expectation;
 - a short README with the question, correspondence table, bounds, assumptions,
   exclusions, properties, results, and run command.
 
+Run checks from the repository root with `./tla-check [<Concern> ...]` (see
+[`Where/Specifications/TrackingReconciliation`](../../../Where/Specifications/TrackingReconciliation/README.md)).
+The root script owns TLC/JDK download and pinning; do not add per-spec `check`
+scripts or wire TLA+ into CI unless explicitly requested.
+
 Do not force these exact filenames when the protocol needs a different model
 shape.
 

AGENTS.md

@@ -99,17 +99,18 @@ over a build setting Xcode didn't export.
 
 An app ships an **attribution report** — every third-party work it is built
 with, license notices inline. **Re-run `./attribution` and commit the result
-whenever you add or bump a package or an agent skill**; `./attribution
---check` fails CI if you forget (offline, sub-second — an app's own tests
-can't do this job, since a test bundle can't read `Package.swift`).
+whenever you add or bump a package, an agent skill, or a development tool**;
+`./attribution --check` fails CI if you forget (offline, sub-second — an app's
+own tests can't do this job, since a test bundle can't read `Package.swift`).
 
 - [`Shared/CreditKit`](Shared/CreditKit/AGENTS.md) owns the types and the
   reporting tool and holds **no credits of its own**; each app declares its
   sources in an `attribution-sources.json` and ships the report in its own
   resources (for Where, `Where/Where/Resources/attribution.json`).
 - The report derives from `.product(name:package:)` links (pinned by
-  `Package.resolved`) and `.agents/external-skills.json`, notices read at the
-  pinned revision — so tooling-only packages correctly aren't credited.
+  `Package.resolved`), `.agents/external-skills.json`, and
+  `.agents/development-tools.json`, notices read at the pinned revision — so
+  tooling-only packages correctly aren't credited.
 - **Kind is derived, not declared**: anything reachable from `shippedFrom`'s
   target closure is a library, any other linked package a development tool —
   linking is not shipping, and a UI must keep the two apart.
@@ -150,7 +151,9 @@ by `./sync-agents`.
 `.agents/skills/.gitignore` excludes those fetched copies, so anything else
 under `.agents/skills/` is **repo-owned** and committed. External skills are
 also an **attribution** input — after adding or updating one, re-run
-`./attribution` (see [Attribution](#attribution)).
+`./attribution` (see [Attribution](#attribution)). The same applies to
+`.agents/development-tools.json` when pinned verification or other non-SPM
+tooling changes.
 
 **`.agents/skills/` is the real home; edit the source, never the
 `.claude/skills/` mirror**, and run `./sync-agents` after adding or editing a

MODULE_AUDIT.md

@@ -53,7 +53,7 @@ Pointers only — each one's evidence and suggested fix live in the linked file.
 | 3 | **high** | WhereCore | `DailySummaryReconciler.reconcile()` is absent from the post-day-change fan-out — the notification body stays stale until a foreground re-`configure` | [`Where/TODOs.md`](Where/TODOs.md) P0 |
 | 4 | **high** | WhereUI | Tracking toggle race — `trackingEnabled`'s setter spawns unserialized `Task`s | [`Where/TODOs.md`](Where/TODOs.md) P1 |
 | 5 | **high** | LifecycleKit | Cancel during the *last* step's `minVisible` hold isn't observed, so a superseded drive can set `phase = .ready` | [`Shared/LifecycleKit/TODOs.md`](Shared/LifecycleKit/TODOs.md) P0 |
-| 6 | **medium** | WhereCore | `setPrimaryRegions(_:)` commits atomically but skips `reconcileAfterDayChange()` | [`Where/TODOs.md`](Where/TODOs.md) P1 |
+| 6 | **medium** | WhereCore | `setPrimaryRegions(_:)` commits atomically but skips `reconcileAfterDayDataChange()` | [`Where/TODOs.md`](Where/TODOs.md) P1 |
 | 7 | **medium** | WhereCore | `setTrackedRegion(false)` hard-deletes the row; the shipped picker now reaches it, so past-year re-attribution risk is live | [`Where/TODOs.md`](Where/TODOs.md) P1 |
 | 8 | **medium** | PeriscopeCore | Orphan sweep treats an undecodable `SpanBegan` as an orphan-close candidate, silently overriding `survivesRelaunch` | [`Shared/Periscope/TODOs.md`](Shared/Periscope/TODOs.md) P1 |
 | 9 | **medium** | WhereUI | Load-state UI duplicated across four views; `PresenceTimelineList` renders the *empty* state while the year is still loading | [`Where/TODOs.md`](Where/TODOs.md) P1 |
@@ -69,7 +69,7 @@ Pointers only — each one's evidence and suggested fix live in the linked file.
 
 ### Reconciliation: same two holes, one now user-reachable
 
-`reconcileAfterDayChange()` still fans out to issue state and widgets only. **Daily summary** remains outside it, and **`setPrimaryRegions(_:)`** still commits without calling it. Related and newly urgent: untracking a region hard-deletes its row, and the shipped onboarding picker plus the Settings region editor both route into that path, so the past-year re-attribution risk the `SwiftDataStore` TODO describes is now something a user can trigger.
+`reconcileAfterDayDataChange()` still fans out to issue state and widgets only. **Daily summary** remains outside it, and **`setPrimaryRegions(_:)`** still commits without calling it. Related and newly urgent: untracking a region hard-deletes its row, and the shipped onboarding picker plus the Settings region editor both route into that path, so the past-year re-attribution risk the `SwiftDataStore` TODO describes is now something a user can trigger.
 
 ### Presentation-layer calendar drift outlived the fix
 

Shared/CreditKit/AGENTS.md

@@ -41,7 +41,9 @@ the root [`AGENTS.md`](../../AGENTS.md).
 - **`kind` is derived from reachability, not declared.** `shippedFrom` names
   the app's root package targets; anything inside that closure is a `library`,
   any other linked package a `developmentTool` — linking is not shipping.
-  `shippedFrom` is the only hand-set part.
+  `shippedFrom` is the only hand-set part for SPM packages. **`agentSkills` and
+  `developmentTools` declare `kind` in config** — both are development tools in
+  Where today.
 
 ## Testing
 

Shared/CreditKit/README.md

@@ -66,17 +66,20 @@ ruby Shared/CreditKit/Tools/generate-attribution.rb <config.json>   # just one
     { "type": "swiftPackageManager", "manifest": "Package.swift",
       "resolved": "Package.resolved", "shippedFrom": ["WhereUI"] },
     { "type": "agentSkills", "kind": "developmentTool",
-      "manifest": ".agents/external-skills.json" }
+      "manifest": ".agents/external-skills.json" },
+    { "type": "developmentTools", "kind": "developmentTool",
+      "manifest": ".agents/development-tools.json" }
   ]
 }
 ```
 
-Paths are relative to the repository root. Two source types are understood:
+Paths are relative to the repository root. Three source types are understood:
 
 | Type | Reads | Credits |
 |------|-------|---------|
 | `swiftPackageManager` | packages a target links via `.product(name:package:)`, pinned by the resolved file | one per linked package |
 | `agentSkills` | a `./sync-agents` manifest of `name -> { repo, ref }` | one per vendored skill |
+| `developmentTools` | a manifest of `name -> { repo, ref, version? }` for pinned GitHub-hosted tooling the repo uses but does not link as an SPM package | one per entry |
 
 Deriving the list rather than maintaining it is the point: a package linked by
 *any* module shows up the next time the report runs, so no module has to
@@ -92,6 +95,12 @@ a test-support target is credited (the repo depends on it) but must not be
 described as being in the binary. `shippedFrom` is the only part set by hand, so
 adding a dependency can't quietly land under the wrong kind.
 
+`developmentTools` entries may carry an optional `version` for display; when
+omitted, the pinned ref's short prefix is used (as for agent skills). Keep each
+entry's `ref` aligned with the revision the repository actually uses — for
+example, bump `.agents/development-tools.json` when `./tla-check`'s pinned TLC
+version changes.
+
 The tool needs network and an authenticated `gh`. It is idempotent: re-running
 with nothing changed rewrites the same bytes.
 
@@ -116,9 +125,10 @@ handle at runtime.
   credit names in a test — a test bundle can't read the manifests, so it can
   only compare the report to a literal, which a stale report matches too.
 - **Development tools are not in the binary.** They are credited because the
-  repository makes copies of them, which permissive licenses ask us to
-  attribute. Any UI must keep the two kinds visually distinct so a reader isn't
-  told something untrue about the app they are running.
+  repository depends on them — vendored agent skills, pinned verification
+  tooling, and the like — which permissive licenses ask us to attribute. Any UI
+  must keep the two kinds visually distinct so a reader isn't told something
+  untrue about the app they are running.
 - **A missing report is not automatically an error.** Only the app target ships
   one, so `load` throwing `.reportMissing` is routine in a developer tool or
   test host. CreditKit reports it and leaves the judgement to the caller.
@@ -129,5 +139,6 @@ handle at runtime.
   is on its own; the type can't check what it can't see.
 - **Names, versions, and license titles are never localized.** They are proper
   nouns and legal terms; a UI supplies the translated framing around them.
-- **GitHub-hosted sources only.** Both source types resolve notices through the
-  GitHub API; a dependency hosted elsewhere would need a new source type.
+- **GitHub-hosted sources only.** All manifest-based source types resolve
+  notices through the GitHub API; a dependency hosted elsewhere would need a
+  new source type.

Shared/CreditKit/Tools/generate-attribution.rb

@@ -17,7 +17,9 @@
 #       { "type": "swiftPackageManager", "manifest": "Package.swift",
 #         "resolved": "Package.resolved", "shippedFrom": ["WhereUI"] },
 #       { "type": "agentSkills", "kind": "developmentTool",
-#         "manifest": ".agents/external-skills.json" }
+#         "manifest": ".agents/external-skills.json" },
+#       { "type": "developmentTools", "kind": "developmentTool",
+#         "manifest": ".agents/development-tools.json" }
 #     ]
 #   }
 #
@@ -37,6 +39,10 @@
 #   - `agentSkills` — a `./sync-agents` external-skills manifest of
 #     `name -> { repo, ref }`. These are not in the binary, but the repository
 #     makes copies of them, which is what their licenses ask us to attribute.
+#   - `developmentTools` — a manifest of pinned GitHub-hosted tooling the
+#     repository depends on but does not link as an SPM package (e.g. TLA+/TLC
+#     via `./tla-check`). Entries may carry an optional `version` for display;
+#     otherwise the pinned ref's short prefix is used.
 #
 # Each credit carries its notice **inline**, read at the pinned revision, so one
 # decode yields everything needed to discharge the attribution and there is no
@@ -199,20 +205,28 @@ def swift_package_manager_credits(source)
   end
 end
 
-def agent_skills_credits(source)
+def manifest_credits(source, source_type)
   kind = source.fetch("kind")
-  read_json(source.fetch("manifest"), "agentSkills").map do |name, entry|
+  read_json(source.fetch("manifest"), source_type).map do |name, entry|
     ref = entry.fetch("ref")
     credit(
       name: name,
       kind: kind,
-      version: ref[0, 12],
+      version: entry["version"] || ref[0, 12],
       slug: entry.fetch("repo"),
       ref: ref,
     )
   end
 end
 
+def agent_skills_credits(source)
+  manifest_credits(source, "agentSkills")
+end
+
+def development_tools_credits(source)
+  manifest_credits(source, "developmentTools")
+end
+
 SOURCE_TYPES = {
   "swiftPackageManager" => {
     required: %w[manifest resolved shippedFrom],
@@ -222,6 +236,10 @@ def agent_skills_credits(source)
     required: %w[manifest kind],
     generate: method(:agent_skills_credits),
   },
+  "developmentTools" => {
+    required: %w[manifest kind],
+    generate: method(:development_tools_credits),
+  },
 }.freeze
 
 # Checked for every source before any of them runs, so a config mistake costs a
@@ -287,7 +305,8 @@ def write_report(credits, output_path)
 #
 # Runs entirely offline, which is the whole reason it can gate CI: every field
 # it compares is derived from `Package.swift`, `Package.resolved`, and the skills
-# manifest. It can't re-read a notice, but it doesn't need to — a notice is
+# and development-tools manifests. It can't re-read a notice, but it doesn't need
+# to — a notice is
 # fetched at the pinned revision, so a matching revision means matching text by
 # construction, and the notice being *present* is checked here directly.
 def check_report(credits, output_path)

Where/AGENTS.md

@@ -284,6 +284,10 @@ surfaces survive at near-Release speed. Options: `./Where/install --help`.
 
 Root [testing conventions](../AGENTS.md#testing) apply. What's specific here:
 
+- **Formal protocol specs** live under [`Specifications/`](Specifications/); run
+  them locally with [`./tla-check`](../tla-check) (opt-in, not CI). Each folder
+  holds a `.tla` model, TLC configs, a `manifest.json`, and a README tying the
+  model to production code and cited Swift tests.
 - Test bundles run in `StuffTestHost` via the `unitTests` helper in
   `Project.swift` and link `TestHostSupport` (`show(_:perform:)`, `waitFor`).
 - Use `ScriptedLocationSource` and `SwiftDataStore.inMemory()` — never

Where/Specifications/IngestorQuiesce/Broken.cfg

@@ -0,0 +1,10 @@
+SPECIFICATION Spec
+
+CONSTANTS
+    Implementation = "broken"
+
+INVARIANTS
+    TypeOK
+    NoPersistAfterQuiesceDone
+
+CHECK_DEADLOCK FALSE

Where/Specifications/IngestorQuiesce/Current.cfg

@@ -0,0 +1,12 @@
+SPECIFICATION Spec
+
+CONSTANTS
+    Implementation = "current"
+
+INVARIANTS
+    TypeOK
+    NoAcceptAfterQuiesceBegin
+    NoPersistAfterQuiesceDone
+    MonitoringOffAtQuiesceDone
+
+CHECK_DEADLOCK FALSE

Where/Specifications/IngestorQuiesce/IngestorQuiesce.tla

@@ -0,0 +1,113 @@
+---- MODULE IngestorQuiesce ----
+EXTENDS Integers
+
+CONSTANTS Implementation
+
+ASSUME Implementation \in {"current", "broken"}
+
+Phases == {"idle", "begin", "awaiting", "done"}
+
+VARIABLES
+    acceptsSamples,
+    isMonitoring,
+    inFlightPersist,
+    quiescePhase,
+    storeCount,
+    sampleDelivered,
+    postQuiescePersist
+
+vars == <<acceptsSamples, isMonitoring, inFlightPersist, quiescePhase,
+          storeCount, sampleDelivered, postQuiescePersist>>
+
+Init ==
+    /\ acceptsSamples = TRUE
+    /\ isMonitoring = TRUE
+    /\ inFlightPersist = FALSE
+    /\ quiescePhase = "idle"
+    /\ storeCount = 0
+    /\ sampleDelivered = FALSE
+    /\ postQuiescePersist = FALSE
+
+StreamSample ==
+    /\ quiescePhase = "idle"
+    /\ ~inFlightPersist
+    /\ storeCount < 3
+    /\ sampleDelivered' = TRUE
+    /\ IF acceptsSamples
+          THEN inFlightPersist' = TRUE
+          ELSE inFlightPersist' = FALSE
+    /\ UNCHANGED <<acceptsSamples, isMonitoring, quiescePhase, storeCount, postQuiescePersist>>
+
+CompletePersist ==
+    /\ inFlightPersist
+    /\ inFlightPersist' = FALSE
+    /\ postQuiescePersist' = (quiescePhase = "done")
+    /\ IF quiescePhase = "done" /\ Implementation = "current"
+          THEN UNCHANGED storeCount
+          ELSE storeCount' = storeCount + 1
+    /\ UNCHANGED <<acceptsSamples, isMonitoring, quiescePhase, sampleDelivered>>
+
+BeginQuiesce ==
+    /\ quiescePhase = "idle"
+    /\ quiescePhase' = "begin"
+    /\ acceptsSamples' = IF Implementation = "broken" THEN acceptsSamples ELSE FALSE
+    /\ isMonitoring' = FALSE
+    /\ UNCHANGED <<inFlightPersist, storeCount, sampleDelivered, postQuiescePersist>>
+
+AwaitInFlight ==
+    /\ quiescePhase = "begin"
+    /\ quiescePhase' = "awaiting"
+    /\ UNCHANGED <<acceptsSamples, isMonitoring, inFlightPersist, storeCount, sampleDelivered, postQuiescePersist>>
+
+CompleteQuiesce ==
+    /\ quiescePhase = "awaiting"
+    /\ ~inFlightPersist
+    /\ quiescePhase' = "done"
+    /\ UNCHANGED <<acceptsSamples, isMonitoring, inFlightPersist, storeCount, sampleDelivered, postQuiescePersist>>
+
+LateSampleAfterQuiesce ==
+    /\ quiescePhase = "done"
+    /\ ~inFlightPersist
+    /\ sampleDelivered' = TRUE
+    /\ IF acceptsSamples
+          THEN inFlightPersist' = TRUE
+          ELSE inFlightPersist' = FALSE
+    /\ UNCHANGED <<acceptsSamples, isMonitoring, quiescePhase, storeCount, postQuiescePersist>>
+
+Next ==
+    \/ StreamSample
+    \/ CompletePersist
+    \/ BeginQuiesce
+    \/ AwaitInFlight
+    \/ CompleteQuiesce
+    \/ LateSampleAfterQuiesce
+
+Fairness ==
+    /\ WF_vars(StreamSample)
+    /\ WF_vars(CompletePersist)
+    /\ WF_vars(BeginQuiesce)
+    /\ WF_vars(AwaitInFlight)
+    /\ WF_vars(CompleteQuiesce)
+    /\ WF_vars(LateSampleAfterQuiesce)
+
+Spec == Init /\ [][Next]_vars /\ Fairness
+
+TypeOK ==
+    /\ acceptsSamples \in BOOLEAN
+    /\ isMonitoring \in BOOLEAN
+    /\ inFlightPersist \in BOOLEAN
+    /\ quiescePhase \in Phases
+    /\ storeCount \in 0..3
+    /\ sampleDelivered \in BOOLEAN
+    /\ postQuiescePersist \in BOOLEAN
+
+NoAcceptAfterQuiesceBegin ==
+    quiescePhase \in {"begin", "awaiting", "done"} => ~acceptsSamples
+
+NoPersistAfterQuiesceDone ==
+    ~postQuiescePersist
+
+MonitoringOffAtQuiesceDone ==
+    quiescePhase = "done" => ~isMonitoring
+
+====