Flying Spaguetti Monster: Verifying protocols with types and finite state machines (Chris Ford)