> You can't formally verify your application works correctly under transient network error conditions if you never thought about what your application should do under those conditions.

This is why it's so important to separate functional from stateful code. Functional code is generally easier to specify. And, by isolating stateful code, one can e.g. fail fast and avoid stepping into undefined behavior.