はじめに 分散合意アルゴリズム Raft とは 分散合意アルゴリズムとは Raft の特徴 Raft が満たす性質 Election Safety Leader Append-Only Log Matching Leader Completeness State Machine Safety TLA+ とは TLA+ による Raft の形式的仕様 TLA+ による Raft の検証方法 TLA+ Toolbox のインストール 新規 Spec の作成 Model の作成と実行 補足: コマンドラインでの検証 Raft の拡張について Leadership Transfer Membership Change Log Compaction Client Interaction おわりに Raft 理解度を調べるクイズ 参考資料 Raft に関する資料 TLA+ に関する資料 はじめに この
![分散合意アルゴリズム Raft を TLA+ で検証する - 俺の Colimit を越えてゆけ](https://cdn-ak-scissors.b.st-hatena.com/image/square/cd66adf9e5b82d8e2b8706006ae3c567d1432e35/height=288;version=1;width=512/https%3A%2F%2Fm.media-amazon.com%2Fimages%2FI%2F51Ii4vClDtL._SL160_.jpg)