Random inputs are a poor way to find a bug that depends on the order things happen in, because that order may turn up once in a thousand runs. So write down a small model of the system, and visit every state it can reach.
Model checking
Also called TLC, Explicit-state checking
A tool walks every state a small model of your system can reach, in every order the steps could happen, and checks an invariant in each. If one breaks, it hands you the shortest sequence of steps that gets there. The model is a short description of the design, not your code.
Agents write the happy order and test the happy order, and a race only shows on some other order. The checker doesn't need to be lucky. But it checks the model the agent wrote, so a step the model leaves out can't fail. Replay every counterexample on the real code, and make sure a broken model fails.
“Write a TLA+ model in specs/withdraw.tla: two requests, each with a separate check step and debit step, from a balance of 100. Add INVARIANT BalanceNeverNegative, run TLC and paste the shortest trace. Then replay that trace against the real code as a test, one step per action. If the bug doesn't appear, assume the model is wrong.”