Sure. That is not the sort of thing that is guaranteed to catch all bugs. Model checking approaches are better at providing proofs of non-trivial properties.
The problem is that model checking checks a model which often fails to properly match the actual implementation. Plenty of people have used model proven algorithms but had implementation bugs that mean that the highly desired properties proven for the model are not upheld.
Being able to automatically check the implementation against specific race conditions (etc.) helps to provide confidence in the implementation working correctly, which means your model proven results are more likely correct for the actual implementation.
The problem is that model checking checks a model which often fails to properly match the actual implementation. Plenty of people have used model proven algorithms but had implementation bugs that mean that the highly desired properties proven for the model are not upheld.
Being able to automatically check the implementation against specific race conditions (etc.) helps to provide confidence in the implementation working correctly, which means your model proven results are more likely correct for the actual implementation.