TLA+ protocol expansion for Where - #184
Conversation
Extract a root script that discovers specs via manifest.json, pins TLC and Temurin through mise, and runs pass/fail cases. TrackingReconciliation drops its local check script in favor of the shared runner. Co-authored-by: Cursor <cursoragent@cursor.com>
Models the handoff-not-factory contract for App Intent service installation: parked callers await install, clear resumes on the next install, and a later install replaces the cached stack. Cited by IntentServicesTests. Co-authored-by: Cursor <cursoragent@cursor.com>
Serialize ingestor start/stop on a single worker lane, re-read intent after each await, and let stop preempt an in-flight start without deadlocking. LocationIngestor.start() bails out if stop() ran during LocationSource.start(). newerStopWinsOverInFlightStart passes without withKnownIssue. Co-authored-by: Cursor <cursoragent@cursor.com>
Models reset/erase teardown ordering: quiesce completes before the store wipe and a late GPS sample cannot repopulate an erased store. Co-authored-by: Cursor <cursoragent@cursor.com>
Models at-most-one active durable log sink per process and scope activation handoff, covering the Flyover sibling-scope exception tracked in TODOs. Co-authored-by: Cursor <cursoragent@cursor.com>
DayJournal.ingest, bulk ingest, and addManualSample now call reconcileAfterDayChange() so reminders and widgets stay in sync. TLC model verifies the canonical post-write ordering; tests updated for the extra reconcile on ingest paths. Co-authored-by: Cursor <cursoragent@cursor.com>
Confirmatory model for at-most-one outermost perform, same-task nesting, and FIFO waiter ordering. SwiftDataStoreTests cites the AtMostOneOutermost property. Co-authored-by: Cursor <cursoragent@cursor.com>
Add clearWhileParkedResumesOnTheNextInstall, cited by the IntentServicesHandoff TLA+ spec's parked-install contract. Co-authored-by: Cursor <cursoragent@cursor.com>
Mark tracking worker and ingest fan-out fixes done, cross-link PostWriteReconcile from remaining fan-out gaps, file P2 LaunchLifecycle and scope-exclusion models, and add ./tla-check pointer under Testing. Co-authored-by: Cursor <cursoragent@cursor.com>
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
| guard !isMonitoring else { return } | ||
| isMonitoring = true | ||
| await locationSource.start() | ||
| guard isMonitoring else { return } |
There was a problem hiding this comment.
Posted by an AI agent on kve's behalf.
Fix: abort start if stop ran during the await (supporting fix for TrackingReconciliation)
What was wrong: start() set isMonitoring = true before await locationSource.start(). A coalesced stop could interleave on the ingestor actor (stop() sets isMonitoring = false), but when the parked start() resumed it continued setting up the ingest task as though monitoring were still wanted.
How the model exposed it: TLC's counterexample has disable stop the ingestor (ingestorActive = false) while enable is still in its "starting" phase. Production needed the same guarantee: a stop during the LocationSource.start() await must leave the ingestor genuinely off, not half-started.
What this guard does: If stop() ran during the await, bail before backlog drain / ingest-task setup. Pairs with the worker's immediate ingestor.stop() on coalesced disable.
| } | ||
|
|
||
| let currentEffective = wantsTracking && authorizationStatus.allowsBackgroundTracking | ||
| guard currentEffective == targetEffective, !trackingReconcilePending else { |
There was a problem hiding this comment.
Posted by an AI agent on kve's behalf.
Fix: re-read intent before publishing (TLA: TrackingReconciliation, FixedCompleteStart / FixedCompleteStop)
What was wrong: The old path published effective tracking state from the target captured before the await, not from intent after the side effect completed.
How TLC found it: In the coalesced model, FixedCompleteStart sets worker' = IF desired /\ Authorized = target THEN "idle" ELSE "ready" — i.e. after start completes, if intent changed during the "starting" phase, the worker loops rather than publishing stale published = TRUE. The broken model's BrokenCompleteStart always sets published' = TRUE regardless of current desired, which is exactly the bug TLC falsifies.
What this code does: After each ingestor.start() / stop() await, recompute currentEffective and continue the loop if it no longer matches the target captured for that iteration (or if another reconcile was coalesced via trackingReconcilePending). Only then assign isTracking.
| public func ingest(_ sample: LocationSample) async throws { | ||
| try await store.perform { try await store.add(sample: sample) } | ||
| await widgets.publishAfterIngest(of: sample) | ||
| await reconcileAfterDayChange() |
There was a problem hiding this comment.
Posted by an AI agent on kve's behalf.
Fix: route ingest paths through full post-write fan-out (TLA: PostWriteReconcile)
What was wrong: ingest(_:), bulk ingest, and addManualSample called widgets.publish() directly, skipping reconcileIssueState() — so a GPS presence change updated the widget snapshot but left the reminder badge and issue alerts stale until the next foreground reconcile.
How TLC found it: The model splits commit, reconcile phases, and changes() ping. Property NoChangesBeforeReconcileDone requires changesPinged => reconcilePhase = done on the canonical path. Broken.cfg allows PingChanges before reconcile completes (BrokenNoEarlyPing), modeling write paths that notify readers before side effects are honest. Code review against the model's correspondence table showed ingest was a production instance of a partial fan-out — widget-only, not the unified reconcileAfterDayChange() sequence the canonical manual-day path uses.
What this change does: All three ingest entry points now await the same fan-out as manual-day writes (invalidate → reminders → issue alerts → widgets). Remaining gaps (DailySummaryReconciler, setPrimaryRegions) are cross-linked in Where/TODOs.md as out-of-model until routed.
|
|
||
| /// Apply ingestor start/stop and publish ``isTracking`` on a single lane so | ||
| /// a newer stop cannot lose to an older start that resumes after its await. | ||
| private func runTrackingReconcile() async { |
There was a problem hiding this comment.
Posted by an AI agent on kve's behalf.
Fix: coalesced tracking worker (TLA: TrackingReconciliation)
What was wrong: Each toggle assignment spawned an independent Task. reconcileTracking() captured intent, awaited ingestor.start(), then unconditionally published isTracking = true when the await returned — even if a newer stop had already persisted wantsTracking = false and stopped the ingestor during that await.
How TLC found it: Broken.cfg runs the command sequence enable → disable with weak fairness. TLC violates CorrectAtQuiescence with final state desired = persisted = ingestorActive = false but published = true. The counterexample matches the real actor boundary: enable enters LocationIngestor.start(), disable runs during the LocationSource.start() await, then the stale enable completion publishes true.
What this code does: One serialized worker lane; on coalesced stop, call ingestor.stop() immediately instead of awaiting the in-flight start (avoids deadlock when start is parked on LocationSource.start()). Coalesced.cfg satisfies the same property for the modeled design.
LaunchLifecycle models undetermined promotion, memo-preserving re-drive, and foreground-only capture-today. ScopeExclusivity models at-most-one active scope and live real container (complementing LogRouting sink ownership). Both confirmatory on Current.cfg; ./tla-check now runs eight specs. Co-authored-by: Cursor <cursoragent@cursor.com>
Co-authored-by: Cursor <cursoragent@cursor.com>
Overall, this is an unusually disciplined adoption for an app codebase — closer to how teams use TLA+ for design verification than as a research artifact. The pilot → expansion arc worked: one spec found a real bug, the skill codifies the workflow, and Below is an assessment against both what you've built and what the broader TLA+ community recommends. What's working well1. Narrow scope, one question per spec Each folder asks a single correctness question ( 2. The skill is excellent process documentation The
That's better than most public "TLA+ in CI" tutorials, which stop at "run TLC and go green." 3. Negative controls are first-class Every spec has a 4. Traceability back to Swift The loop is closed properly:
5.
This is cleaner than most ad-hoc 6. Opt-in, not CI (for now) is a reasonable call Mergify explicitly notes spec drift as a maintenance burden and that CI without drift discipline gives false confidence. Your AGENTS.md says "opt-in, not CI" — that's honest. Formal methods communities generally agree TLA+ complements testing; it doesn't replace it (wal.sh TLA+ guide, Lamport's own framing). 7. Confirmatory specs still have value Even "green on Current.cfg" specs document a claim with explicit bounds. That's useful for onboarding and for the controller rewrite TODOs — you've pre-modeled slices before the big refactor. 8. Protocol pattern library
Possible improvementsHigh value, low disruption
Medium value, more effort
Lower priority / situational
On the skill specificallyStrengths:
Gaps worth filling:
Bottom lineYou've built something most teams never get past the pilot on: a repeatable, honest, bounded formal verification loop integrated into agent workflow without pretending it proves correctness of the whole app. The integration is strong on:
The main risks going forward are the ones the literature warns about too:
If you want one next step with the best ROI: a path-filtered Linux CI job running |
Route single-sample ingest and addManualSample through reconcileIssueState() plus publishAfterIngest(of:) so reminders/issue alerts reconcile without unconditional widget rebuilds. Bulk ingest keeps reconcileAfterDayChange(). Fixes WhereServicesTests.redundantGPSSamplesSkipRepublishingButNewRegionsStillPublish on CI. Co-authored-by: Cursor <cursoragent@cursor.com>
Specula vs our TLA+ setup — overlap assessmentThinking out loud on how much of our custom skill/tooling could be replaced by Specula. Short answer: Specula could replace part of the agent workflow and TLC ergonomics, but not most of what we built. The overlap is real; the philosophies differ enough that a full swap would trade something we want (small, committed, Swift-native design artifacts) for something Specula is optimized for (autonomous, whole-system bug hunting with external outputs). What we built vs what Specula is
Our setup is closer to maintained design experiments tied to production. Specula is closer to autonomous bug factory for concurrent/distributed systems. Overlap: what Specula could replace1. Agent methodology (~30–40%) Our skill and Specula's
Specula's guides are richer on orchestration (BFS vs simulation, fault injection, trace validation). Ours are richer on Swift-specific modeling (actors, awaits, desired vs persisted vs published, coalescing workers) and repo policy (don't wire into CI unless asked, narrow slices only). 2. TLC execution (~70–80% mechanically, ~0% politically) Both pin Java + But
Specula doesn't give us that repo-native contract. We'd still want 3. Counterexample → test (~50%) Specula Phase 4 ( What Specula adds that we don't have (and probably shouldn't replace our stuff with)
That's ~60% of Specula's surface area — optimized for CometBFT-scale targets, not "does What Specula would not replace (keep these)
Practical synthesisReasonable adoption tiers:
Bottom line
The TrackingReconciliation → PostWriteReconcile arc is the argument for keeping our approach: hand-curated slices found real bugs, negative controls caught regressions ( Highest-ROI probe without committing: install Specula's MCP servers, run |
Add a developmentTools generator source type for pinned non-SPM tooling, wire TLA+ Tools v1.7.4 through .agents/development-tools.json, and regenerate Where's attribution report. Co-authored-by: Cursor <cursoragent@cursor.com>
| } | ||
| } | ||
| await widgets.publish() | ||
| await reconcileAfterDayChange() |
There was a problem hiding this comment.
I wonder if reconcileAfterDayChange is the best name for this, vs something else like reconcileAndPublishWidgets?
| public func stopTracking() async { | ||
| wantsTracking = false | ||
| await services.ingestor.stop() | ||
| isTracking = false |
There was a problem hiding this comment.
Looks like we dropped isTracking = false; confirming this was intentional, right? I think trackingWorkerLoop handles this now?
Clarifies the method runs after persisted day-level store data changes, not a calendar-day rollover. Co-authored-by: Cursor <cursoragent@cursor.com>
Isolating declarative behavior from async structureThe TLA specs read well because they separate: Production code still often looks like: That's necessary at the edges, but the decision logic ( The pattern across the areas we touchedThree recurring shapes:
The specs already name the declarative layer. The opportunity is to make that layer explicit in Swift, not buried inside loops. Direction 1: Pure protocol types (closest to TLA)Extract a small state machine value type per protocol — no // Illustrative — not proposing exact API yet
struct TrackingReconcileState: Equatable {
var desired: Bool
var authorizationAllowsBackground: Bool
var ingestorActive: Bool
var published: Bool
var worker: WorkerPhase // idle | ready | starting | stopping
var target: Bool
var pending: Bool
}
enum TrackingReconcile {
static func effectiveTracking(desired: Bool, auth: Bool) -> Bool {
desired && auth
}
/// After a side effect completes: may we publish?
static func shouldPublish(
target: Bool,
currentEffective: Bool,
pending: Bool,
) -> Bool {
currentEffective == target && !pending
}
/// Coalesced stop while worker is in-flight
static func shouldPreemptInFlightStop(targetEffective: Bool) -> Bool {
!targetEffective
}
}
Benefits:
Cost: another type/file per protocol; need discipline to keep effects at the boundary. Direction 2: Reusable coalescing worker (tracking generalized)Tracking is the serialized/coalescing worker pattern from the skill — worth extracting once: protocol CoalescedWorkerEffect {
associatedtype Target: Equatable
func apply(_ target: Target) async
func readCurrentEffective() -> Target // after await
}
// Generic loop: capture target, apply, re-read, continue if stale
Benefits:
Risk: over-abstraction if only tracking needs it today. A lighter version: Direction 3: Reconcile as a declarative plan (DayJournal)PostWriteReconcile is really a fixed pipeline with a policy fork: Today that's two methods duplicating the shared prefix. A more declarative shape: enum PostWriteOutcome {
case sampleIngest(LocationSample)
case dayDataChanged
case issueOnly // dismiss/restore
}
struct PostWriteReconcilePlan: Equatable {
let outcome: PostWriteOutcome
var steps: [ReconcileStep] { … } // pure derivation
}
enum ReconcileStep {
case invalidateIssues
case reconcileReminders
case reconcileIssueAlerts
case publishWidgets
case publishWidgetsAfterIngest(LocationSample)
}
Benefits:
Direction 4: Split "atomic regions" explicitly (Ingestor)
The TLA bug was at boundary 2→3. Making regions explicit helps: enum StartDecision {
case abort // stop won during await
case completeSetup
}
static func afterLocationSourceStart(isMonitoring: Bool) -> StartDecision {
isMonitoring ? .completeSetup : .abort
}The actor method stays async, but the only branch that matters for the protocol is a one-liner pure function — same as TLC's guard. Direction 5: Keep specs and code structurally parallelWe already have correspondence tables in READMEs. Push that one step further:
The goal isn't duplication of TLC — it's one declarative layer both TLC and Swift talk about. What I'd prioritize (ROI vs complexity)High ROI first:
Medium — when a second consumer appears: Later / situational: Guardrails (fit with our conventions)
Natural next steps if we want to pursue this: sketch |
1 participant
Expands the TLA+ verification pilot from one spec to eight, adds a unified
./tla-checkrunner, and lands the two production fixes the models falsified.Tooling
./tla-checkdiscoversWhere/Specifications/*/manifest.json, pins TLC + Temurin, and runs pass/fail casesTrackingReconciliationmigrated off its localcheckscriptTLA+ specs (all green via
./tla-check)changes()SwiftDataStoreTestsProduction fixes
WhereSession(found byTrackingReconciliationbroken config)DayJournal.ingest/ bulk ingest /addManualSamplenow callreconcileAfterDayChange()(found byPostWriteReconcilenegative control + code review)Docs
Where/TODOs.md— tracking + ingest items closed; PostWriteReconcile cross-links; P2 TLA items landedWhere/AGENTS.md—./tla-checkpointer under TestingChecks
./swiftformat --lint./tla-check(8 specs)WhereSessionTrackingTests,DayJournalTests,IntentServicesTests,SwiftDataStoreTests