Companion artifact for SLS-5021.

5-node LCG model with 3 invariants. Bug cfg: write LSN 1 to

{n1,n2,n3} → snapshot n1 → lose {n1,n2,n3}

→ recover without attestation → survivors

{n4,n5}

empty + snapshot 0, but committed=

{1}

→ invariant fails. Snapshots from lost nodes preserved (S3 outlives node).

Files in worktree mongo-w5-3:

• src/mongo/tla_plus/Disagg/LCGMajorityLossRecovery/
• src/mongo/db/SLS-5021-DESIGN.md

Status: Draft.