It's essential to rule out certain happenings when performing analysis, and acts of God are commonly among them. For example, if you need to account for cosmic

It's essential to rule out certain happenings when performing analysis, and acts of God are commonly among them. For example, if you need to account for cosmic rays, you can't prove anything meaningful about software. Redundancy won't get you out of this: you add redundancy, I'll add more cosmic rays. All that does is force a useful analysis into a muddy and probabilistic one. It's actually pretty important to account for cosmic rays! But you do that on top of an analysis which presumes that the hardware performs correctly. It's not a useful reality to expose to a proof assistant. To anticipate an objection: yes, you absolutely can rule out network partitions in an analysis, if that's a useful thing to do. For a packet-switched network, it isn't useful. But different network topologies exist, or at least used to, ones where once a circuit is negotiated, you can say useful things about the network without accounting for the kind of equipment failure which might break that circuit. For packet switching, you're going to have a really bad time if you don't account for partitions, because those are expected behavior, one of the properties of the system under consideration.