We should produce a TLA+ spec of new pipelined oplog application advancement protocol, and model-check the core invariant:

lastApplied = T implies every op with optime <= T is applied with commit timestamp <= T

The model should cover:

• dispatcher partitioning of a batch into per-worker slices + one in-flight queue entry with a shared counters in each batch
• workers applying slices independently and decrementing the counter
• the advancer thread popping strictly in FIFO order, stopping at the first nonzero counter, as the sole publisher of lastApplied
• the drain + inline path: drain-to-empty, apply on the dispatcher, publish via a synthetic completed batch
• the wakeup protocol (worker-completes and dispatcher-enqueues notifications, plus the periodic backstop), checking we can't lose a publication

We are intentionally omitting transaction handling and multikey flush ordering.

The completed model should be merged into the src/mongo/tla_plus/Replication path. This model should not reference disagg in any capacity, so this should be OK.