Ram, K. TLA+ Linearizability proof for a concurrent union-find object [Computer software]. https://github.com/KamiV2/linearizability-jt-union-find