Aren’t there formal analysis techniques that can help ferret those out? My MSCS had a course called “science of programming”. The focus used to be proofs for correctness of programs, which included concurrent programs.