You could use TLA+ to model the data structure operations and check the invariant. Checking the invariant with assert is also useful in my limited experience wi

You could use TLA+ to model the data structure operations and check the invariant. Checking the invariant with assert is also useful in my limited experience with concurrency. https://lamport.azurewebsites.net/tla/tla.html https://lamport.azurewebsites.net/tla/tla.html