Comment by xlii

That's true, just as I cannot possibly measure car speed given innate measuring error which is not a defense from getting a speeding ticket.

Formal proving isn't about getting to "my model is reality" but having step above mere imagination or educated guess. That's why it's possible to model paradoxical models. Given N systems they all can fail at the same time and there's nothing that can be done to guarantee message RECV+ACK. So at some point there's invariant saying "ok, we say that 3 out of 5 systems will always work". If you break invariant all hell is loose but at that point many weird stuff might happen.

Usually when one needs to think about message passing in a way like [0] formal proving can save lives (or bottoms, depending on the context).

[0]: https://xlii.space/eng/network-scenarios/