There's a typo in the TLA+ spec for applying oplog entries independently from making them durable:

Restart(i) ==
    /\ state' = [state EXCEPT ![i] = "Follwer"]
    ...

If restarting a node changes its state to "Follwer", that disables actions which check if its state is "Follower", which means model-checking isn't verifying what we want.

Also, model-checking could be much faster if you add Symmetry == Permutations(Server) to MCRaftMongoReplTimestamp.tla and add SYMMETRY Symmetry to MCRaftMongoReplTimestamp.cfg