TLA+ Spec for Async Commit
- Mentors
- Andy Lok, Ziqian Qin
- Organization
- CNCF
The goal of this project is to offer a formal verification using TLA+ for TiKV’s new “Async Commit” transaction model, which brings us more confidence in the improved performance.