利用TLA+语言验证multi-raft模型

TLA+ 是一个形式化验证工具，可以用来检查算法或系统的正确性。 multi-raft是一种分布式一致性算法，CRDB和TiDB都是这种算法保证其数据一致性。

但是在各种场景下，比如Leader-Transfer，Split-Region下，是否multi-raft仍然满足分布式一致性，是个十分有意义的研究课题。

本项目为使用TLA+来验证multi-raft的正确性。