github-repos/tla-plus
1
0
Fork 0
mirror of https://github.com/pingcap/tla-plus.git synced 2024-12-25 12:00:10 +08:00
Code Issues Packages Projects Releases Wiki Activity
54 Commits 2 Branches 0 Tags 1.4 MiB
TLA 89.1%
Coq 10.7%
Makefile 0.2%
master
Go to file
Neil Shen 8ae629ddf9
Add ResolvedTS spec (#27)
2022-04-21 18:37:21 +08:00
CollapseRollbacks move collapserollback optimization to a new separate directory (#24) 2018-08-22 11:33:57 -07:00
ConcurrentPercolator move collapserollback optimization to a new separate directory (#24) 2018-08-22 11:33:57 -07:00
DistributedTransaction add check txn status, read key, read SI check (#37) 2021-08-22 22:06:49 +08:00
OptimizedCommitTS optimized commit ts: remove the cost of getting commitTS (#20) 2018-05-14 17:55:33 +08:00
Percolator percolator: allow clients having different primary keys. (#16) 2018-04-02 14:04:53 +08:00
Raft Port raft from ongardie/raft.tla as-is. (#3) 2018-02-01 15:20:23 +08:00
RaftMerge RaftMerge: rollback and TLC models. (#11) 2018-03-22 14:56:07 +08:00
ResolvedTS Add ResolvedTS spec (#27) 2022-04-21 18:37:21 +08:00
TwoPC Fix silly error in Coq proof. 2018-01-21 20:45:05 +08:00
.gitignore add check txn status, read key, read SI check (#37) 2021-08-22 22:06:49 +08:00
LICENSE Initial commit 2017-12-19 19:12:25 +08:00
README.md Update README.md 2018-05-08 22:52:09 -07:00

README.md

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.