I/O Automata in Isabelle/HOL

We have embedded the meta-theory of I/O automata, a model for describing and reasoning about distributed systems, in Isabelle's version of higher order logic. On top of that, we have specified and verified a recent network transmission protocol which achieves reliable communication using single-bit-header packets over a medium which may reorder packets arbitrarily.

paper