I'm starting to use TLA+ to verify lock-free algorithms. The tool is essential when all your code fits on the screen, yet you can't comprehend what is going on

I'm starting to use TLA+ to verify lock-free algorithms. The tool is essential when all your code fits on the screen, yet you can't comprehend what is going on and miss a race here and there. So far it's more a personal interest, but I'm advocating for spending more time verifying critical pieces of our code base like MPMC containers, synchronization primitives, etc. PS. Doing C/C++/C# in gamedev.