Are your focus and Dr. Kleppmann's mutually exclusive? I ask because it seems like the Isabelle formulation emerges from the protocol itself. The invariant is t

Are your focus and Dr. Kleppmann's mutually exclusive? I ask because it seems like the Isabelle formulation emerges from the protocol itself. The invariant is the only added work, yes? I'm effectively asking if the proof generation could replace the model checking as a way of verifying that you have appropriately specified your protocol. Big information exchange protocols can be confusing! (Maybe I'm misunderstanding what an invariant is... I'm thinking it's the property proved true by induction (and would go something along the lines of "if and only if the good has been sold, then the merchant has received payment for the good"))