diff --git a/README.md b/README.md
new file mode 100644
index 0000000..e4c3ed6
--- /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](https://github.com/pingcap/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).