Modeling Paxos and Flexible Paxos in Pluscal and TLA+ | Heykuki News