TLA+ Spec of a simplified part of MongoDB replication system | Heykuki News