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.

When engineers were designing completely autonomously operated Paris Métro line 14, they had to ensure the safety of tens of millions passengers each year, its 22 stations across Paris as well as smooth running of trains. How to approach development of software that allows for the automation of public transit? The French team decided to use formal verification – learn what it means!