A protocol isn’t your happy path.
It’s what still holds under adversarial execution.

If you can’t define invariants over all state transitions, you’re not designing a protocol. You’re describing intent.

“Exploits” are just valid executions you failed to model.

#FormalMethods #ProtocolDesign #Cryptography