It has been observed that formal verification methods for mathematical proofs, computer programs, communication protocols and the like are usually illustrated by ‘toy’ examples and that such proofs tend to be discouragingly long. In order to demonstrate that it is feasible to verify a ‘real-life’ communication protocol by means of process algebra, we picked one from the literature.

In his Ph.D. thesis, Mullender investigates issues he considered while developing the Amoeba distributed operating system. In Section 3.2.4 of a transaction protocol is described to which we will refer as the Amoeba protocol. In the preceding sections of the design goals are described that this protocol is supposed to satisfy. He does not give a formal verification that his protocol meets this criteria. In fact, it turns out that one of them is not met. Note that this only applies to the simplified version of the protocol that appears in, the actual implementation uses a much more complicated version in which this mistake is not found.

Section 1 of this article gives the minimum background information necessary for understanding the rest of the article.

In Section 2 the design goals are formulated in English and in terms of process algebra.