Not that I don't agree with you but I find it a common failure mode of HDs to just never reply to things. I guess it's also a common failure mode of network systems too.
Can Coq detect that you are enforcing I/O timeouts in a way that guarantees finite time?
More generally, Coq is "just" a well integrated proof tool & I can't see any reason why you couldn't include such features but at some point you have to draw the line and be explicit about what it is that you're actually proving: if your proof assumes data store responsiveness then it's OK for it to do that so long as you're explicit about the resulting limitations IMO. The goal of ever increasing model fidelity is a rabbit hole from which the programmer/prover might never return otherwise :)
In practice, we should use a timeout in the implementation of all the external calls, but we did not and our model to not enforce it.