Summary

TLA+ extension for SERVER-112445 (block-on-red labelled): temporary inconsistency between the log-service LSN and the local stable timestamp during FCV init in disaggregated storage.

Files

• src/mongo/tla_plus/Replication/FCVInitDisaggLSN/FCVInitDisaggLSN.tla (322 lines) — single-server FCV-init state machine Idle → LoadFCVDoc → OpenLogService → WaitConvergence → Returned. Two LSN streams (localStableTS, logServiceLSN), pinned fcvDocCommitLSN, public returnTrace set. Eight actions including ReturnConverged (fix path), ReturnEarly (bug action, gated by AllowReturnBeforeConvergence), and SteadyStateWrite (post-init lockstep advance preserving coherence).
• MCFCVInitDisaggLSN.tla — state constraint + server symmetry.
• MCFCVInitDisaggLSN.cfg — green (AllowReturnBeforeConvergence = FALSE). TLC: no error, 2081 states / 780 distinct / depth 13.
• MCFCVInitDisaggLSN.bug.cfg — bug (=TRUE). TLC: BootstrapCoherence violated, counterexample length 5.
• OWNERS.yml → 10gen/server-replication-reviewers
• README.md (299 words)

Headline invariant

BootstrapCoherence == \A s \in Server. fcvPhase[s] = "Returned" => logServiceLSN[s] = localStableTS[s] /\ both >= fcvDocCommitLSN[s]

Companion: ReturnTraceCoherence (every public return-trace row coherent), plus four step-temporal monotonicity properties (LSNsMonotone, PhaseMonotone, FCVDocCommitFrozen, ConvergedReturnsMonotone).

Modeling note

Initial draft allowed background drivers AdvanceLogServiceLSN and AdvanceLocalStableTS to fire in Returned independently — TLC immediately caught it as a BootstrapCoherence violation. Fixed by restricting those drivers to WaitConvergence and adding SteadyStateWrite (atomic lockstep advance) for the post-init regime. Liveness properties are gated off in the default cfg because SYMMETRY is unsound under liveness (TLC warns); instructions in the cfg show how to enable them by removing SYMMETRY.