TLA+ is basically an academic tool. It allows you to verify your specification, but it is useless to detect bugs in your implementation. In my experience, the process of writing your specification in TLA is a buggy enough process to make it all a waste of time.