Continuing from our previous article, let us take an example of how to write a TLA+ proof for a real-world specification of a distributed system. For this exercise we will go through the Voucher Trading System process as specified by the RFC3506 hosted by IETF. The distributed and concurrent systems require a consensus protocol to achieve overall system reliability and immunity to failures of nodes. We decided to select for this VTS network a simple Two-phase commit protocol.