tlaplus

分散プロトコルは単体テストできないが、モデル検証はできる

分散バグはデプロイ後の修正コストが高い。モデル検証を使えば、実装コードを1行も書く前にそれらを発見できる。以下はTLA+を使った方法である。