The Development of a TLA $$^{+}$$ Verified Correctness Raft Consensus Protocol

The Development of a TLA $$^{+}$$ Verified Correctness Raft Consensus Protocol

연구 분야: Software Development

학회: Asia-Pacific Web (APWeb) and Web-Age Information Management (WAIM) Joint International Conference on Web and Big Data

Distributed consensus protocols require significant effort to design, develop, and verify correctly. Traditional software quality assurance methods rely on developers creating extensive test cases to cover all code branches, which depend heavily on human experience and prolonged testing. While formal methods offer a reliable means of designing correct protocols, they ensure correctness only at the design level. Ensuring implementation correctness remains challenging once it deviates from its original design. This paper introduces our development of a verified correctness Raft protocol using an innovative specification-driven approach. We first specified Raft using TLA and verified its correctness with a model checker. Subsequently, we implemented the protocol based on this verified specification. Finally, we employed model checker tools to automatically generate test cases covering the entire design space for implementation verification, ensuring the implementation is an exact specification refinement. This approach ensures the correctness of both the implementation and the design.