All Projects → pingcap → Tla Plus

pingcap / Tla Plus

Licence: apache-2.0

TLA+ in TiDB

About TLA+

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.

Using TLA+ 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.

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].