github-repos/tla-plus

mirror of https://github.com/pingcap/tla-plus.git synced 2026-08-19 10:03:30 +08:00

Go to file

Queeny f4d588f0d0 Update the format

2018-05-08 22:50:54 -07:00

ConcurrentPercolator

concurrent percolator: fix a copy-then-paste error (#17 )

2018-04-02 14:20:36 +08:00

OptimizedCommitTS

OptimizedCommitTS: fork from concurrent percolator (#19 )

2018-05-08 13:48:07 +08:00

percolator: allow clients having different primary keys. (#16 )

2018-04-02 14:04:53 +08:00

Port raft from ongardie/raft.tla as-is. (#3 )

2018-02-01 15:20:23 +08:00

RaftMerge: rollback and TLC models. (#11 )

2018-03-22 14:56:07 +08:00

Fix silly error in Coq proof.

2018-01-21 20:45:05 +08:00

.gitignore

percolator: allow clients having different primary keys. (#16 )

2018-04-02 14:04:53 +08:00

LICENSE

Initial commit

2017-12-19 19:12:25 +08:00

README.md

Update the format

2018-05-08 22:50:54 -07:00

README.md

tla-plus in TiDB

About 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.

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