分散合意アルゴリズム Raft を形式仕様記述言語の TLA+ を用いて検証する手順を紹介します。

分散合意アルゴリズム Raft の Log Matching Property について可能な限り形式的な証明をしました。