From 16d9b21f8b14477b36a63ec2072cb67563884540 Mon Sep 17 00:00:00 2001 From: Queeny Date: Tue, 8 May 2018 22:32:38 -0700 Subject: [PATCH] Create README.md --- README.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 README.md diff --git a/README.md b/README.md new file mode 100644 index 0000000..045159a --- /dev/null +++ b/README.md @@ -0,0 +1,12 @@ +# 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](https://github.com/pingcap/raft-rs). +- To verify the implementation of distributed transaction. + +For further information about TLA+, see [tla-plus-resources](https://github.com/cmschmtt/tla-plus-resources).