Murat Demirbas

PlusCal-examples. Pluscal/TLA+ modeling of distributed systems/protocols

HLC. TLA

MDBTLA. High level model for MongoDB consistency

RaftLeaderLeases. TLA+ model for Raft Leader Leases, and linearizable reads from leader

TLA-seminar. TLA+ introductory seminar examples

dataflow. TLA+ model for Dataflow protocols

hlc-visualizer. A Javascript visualization for Hybrid Logical Clocks, where you can create local/send events, and take consistent snapshots

BeatPaxos. A Paxos visualization, and a game where you try to delay or even break consensus, by killing a node and delaying messages.