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

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

ナンプレ(数独)は難しさを定義するのが難しい。ナンプレサイトの作成を通して苦労したところを解説します。作成した問題は puzzle.dev で毎日無料で遊べます。