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. The project is written primarily in TLA, distributed under the Apache License 2.0 license, first published in 2017.
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.
Contributors
Showing top 11 contributors by commit count.
Related Repositories
tlaplus/Examples
A collection of TLA⁺ specifications of varying complexities.
spacejam/tla-rust
writing correct lock-free and distributed stateful systems in Rust, assisted by TLA+
tlaplus/DrTLAPlus
Dr. TLA+ series - learn an algorithm and protocol, study a specification
ongardie/raft.tla
TLA+ specification for the Raft consensus algorithm
lemmy/BlockingQueue
Tutorial "Weeks of debugging can save you hours of TLA+". Each git commit introduces a new concept => check the git history!
tlaplus/CommunityModules
TLA+ snippets, operators, and modules contributed and curated by the TLA+ community