Refusal instead of loss

A transition that cannot be proved does not occur. This sounds like a restatement of the model and it is the single most consequential line in it. On an execution chain, a flawed transaction runs anyway: it executes, burns fees, and leaves whatever state its flaw produced. On Modulus

the failure surfaces at proving time, on the author's machine, before anything is submitted. There are no failed transactions that cost money anyway, no partially applied state, no half completed multi-step operations to unwind. The worst outcome a defective predicate can produce is that transitions it should have admitted are refused. That converts a class of safety failures into liveness failures, and downtime is a different kind of bad day from a drained contract.