对于开发过分布式系统的朋友们，相信大家都遇到过这种场景：系统开发完成后，通过了所有的测试用例，于是我们信心满满地将系统上线。可是线上系统跑着跑着，不知哪一天突然莫名其妙地出现了一些 bug。当我们打开日志，打开 gdb，准备追踪定位这些问题时，它们又无法复现了。可如果放任不管，不知什么时候，它们又会诡异的冒出来了。这种 bug 非常棘手，甚至让开发者很崩溃。这个问题本质上是因为分布式系统过于复杂，测试 case 很难覆盖所有可能的运行场景所导致的。无论再怎么细心，某些 corner case 总是存在的。当系统运行到这些 corner case 场景时，bug 就出现了。怎么系统地解决这种问题呢？答案就是本次直播分享的主角—-TLA+。
TLA+ 是 Paxos 算法发明者 Lamport 的大作。它是一套数学建模工具箱，用于给分布式系统建模。主要包括形式化建模语言 TLA+ 和形式化验证工具 TLC model checker。
TDengine 团队对 TLA+ 做了一些探索，用 TLA+ 为 TDengine Database 的分布式算法（基于时序场景下改进的 Raft 算法）建模，以保证在时序数据场景下一致性和正确性，并兼顾读写性能。也希望通过本次直播，分享下我们探索和实践 TLA+ 的过程，供大家参考。
TDengine 研发工程师李明昊结合 TLA+ 在 TDengine Database 的探索，为大家分享如何用 TLA+ 思维为分布式算法建模。
