A TLA+ specification is generally a simplified model of a real system design. So issues can definitely arise when building the real thing, but model testing on a TLA+ spec can definitely help with quickly surfacing bugs that would exist even in a simplified design. Just don't expect it to do more than that.