add a simple model
TLA+ 是一个形式化验证工具，可以用来检查算法或系统的正确性。 multi-raft是一种分布式一致性算法，CRDB和TiDB都是这种算法保证其数据一致性。
但是在各种场景下，比如Leader-Transfer，Split-Region下，是否multi-raft仍然满足分布式一致性，是个十分有意义的研究课题。
本项目为使用TLA+来验证multi-raft的正确性。
CRDB，TiDB（TiKV）等分布式数据库存储数据时采用multi-raft形式，本项目的任务是利用TLA+这一款形式化工具验证multi-raft协议的正确性。
利用TLA+语言验证multi-raft模型
TLA+ 是一个形式化验证工具，可以用来检查算法或系统的正确性。 multi-raft是一种分布式一致性算法，CRDB和TiDB都是这种算法保证其数据一致性。
但是在各种场景下，比如Leader-Transfer，Split-Region下，是否multi-raft仍然满足分布式一致性，是个十分有意义的研究课题。
本项目为使用TLA+来验证multi-raft的正确性。