Developing distributed and concurrent systems is a complex task that requires careful attention to the details. Testing such systems is challenging because it’s difficult to simulate all possible states, including those that can happen due to system failures, network latency, and other factors. This makes it hard to ensure that the system behaves correctly in all circumstances.
Therefore it’s essential to have a proactive approach that involves modeling the system’s behavior in a formal way. Such an approach can help identify potential issues before they occur, saving time and preventing costly flaws.
TLA+ is a formal specification language developed by Leslie Lamport based on the idea of specifying systems using simple mathematics. It is used for designing, modelling, documentation, and verification of programs, especially concurrent and distributed systems. TLA+ and its tools are useful for eliminating fundamental design errors, which are hard to find and expensive to correct in code.
To know more about TLA+, check The TLA+ Home Page.
Pactus consensus specification has written in TLA+ format. It includes all invariants that can be held in every state of every execution that the protocol allows. The TLA+ specification is compiled into PDF file.
By defining some invariants we can ensure the safety of the consensus protocol in any possible and distinct state, and therefore we have the informal safety proof of the Pactus consensus protocol using TLA+.
Checking the liveness is not easy, but with defining some constraints, we have the informal proof of liveness of Pactus consensus protocol using TLA+.