mirror of
https://github.com/pingcap/tla-plus.git
synced 2025-01-13 21:30:08 +08:00
ConcurrentPercolator | ||
OptimizedCommitTS | ||
Percolator | ||
Raft | ||
RaftMerge | ||
TwoPC | ||
.gitignore | ||
LICENSE | ||
README.md |
tla-plus
TLA+ is a formal specification and verification language to help engineers design, specify, reason about, and verify complex software and hardware systems. It is widely used to verify the algorithms in distributed systems.
tla-plus in TiDB
In TiDB, we use TLA+ for the following purposes:
- To verify the distributed consensus algorithm - Raft.
- To verify the implementation of distributed transaction.
For further information about TLA+, see tla-plus-resources.