Summary

TLA+ spec + jstest for SERVER-125663: orphans on former config-server-shard never cleaned because markAsReadyRangeDeletionTaskLocally throws NoMatchingDocument after config.rangeDeletions is dropped, exception swallowed silently, clearPending() never called.

Files

• src/mongo/tla_plus/Sharding/ConfigServerTransitionOrphan/ConfigServerTransitionOrphan.tla (260 lines) — 4 variables (rangeState, onDiskPending, rangeDeletionsColl, transitionState), 9 actions over donor steps (CommitMigration → RegisterInMemoryTask → MarkAsReady_Success/_NoMatchingDocument → RunDeletionChain) × transition steps (Start → BeginDrop → Drop → Commit). Constant AllowDropBeforeMarkReady gates DropRangeDeletions while any range is in Registered. Invariants: NoRangePermanentlyStuck + EveryPendingRangeEventuallyCleared.
• MCConfigServerTransitionOrphan.tla (43) + green cfg (21) + bug cfg (17)
• OWNERS.yml → 10gen/server-sharding
• README.md (54 lines / 331 words)
• jstests/sharding/transition_to_dedicated_in_flight_migration_orphan.js (163) — hangInReadyRangeDeletionLocallyInterruptible failpoint + parallel-shell moveChunk + transitionToDedicatedConfigServer; asserts pending-task count returns to 0 and orphan-doc count reaches 0.

TLC verdicts

• Green (Ranges= {r1,r2}

  , flag=FALSE): 93 distinct states, no error, all temporal properties satisfied.

• Bug (Ranges= {r1}

  , flag=TRUE): 7-state counterexample to NoRangePermanentlyStuck ending in MarkAsReady_NoMatchingDocument(r1) → stuckPending after DropRangeDeletions runs while the in-memory task is in Registered — exactly the hazard.