> Major flaws in a specification for one function are usually quickly picked up when the proof for another function relies on the missing specification properties

Great point! In a sense, it's testing by immediate use at compile time. I always imagine this to be the greatest productivity booster, even greater than AI. You'll notice things are wrong as you type.