Skip to content

IANTHEREAL/tla-plus

 
 

Repository files navigation

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.

About

No description, website, or topics provided.

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • TLA 84.6%
  • Coq 15.1%
  • Makefile 0.3%