Raft is one of the most popular distributed consensus protocols. Since it was proposed in 2014, Raft and its variants have been widely used in different kinds of distributed systems. To prove the correctness of the Raft protocol, developers use the TLA+ formal specification to model and verify its design. However, due to the gap between the abstract formal specification and its practical implementation, distributed systems that implement the Raft protocol (i.e., Raft systems) can still violate the protocol design and introduce intricate bugs. In this paper, we propose a novel testing technique based on TLA+ formal specification to unearth bugs in Raft systems. To be specific, we map Raft’s formal specification to the corresponding Raft system, and then use the specification-defined state space to guide the testing in the Raft system. To evaluate the feasibility and effectiveness of our approach, we apply it on two different Raft systems, and find 3 previously-unknown bugs.