This study conducts a rigorous investigation into the inherent limitations of existing blockchain consensus protocols, particularly with respect to security, scalability, and resilience against adversarial behaviors. A critical gap in current designs is the lack of formal verification to ensure protocol correctness under various operating conditions. Centered on the ChainMaker platform, this work develops a formal model of its consensus mechanism and employs model checking techniques to verify essential protocol properties. The proposed methodology integrates CSP# for formal modeling, Linear Temporal Logic (LTL) for property specification, and the Process Analysis Toolkit (PAT) for exhaustive verification under both normal execution and timeout scenarios. The experimental evaluation reports quantitative metrics such as verification time and state space size, accompanied by a detailed analysis of key attributes including liveness, safety, and fault tolerance. The primary contributions of this work are threefolds: (1) we construct complete formal models of the TBFT and HotStuff consensus protocols using CSP#, capturing core message interactions and state transitions; (2) we specify and verify key correctness properties—including safety, liveness, and delay attack resilience—using LTL and the PAT model checker; (3) we uncover a critical vulnerability in TBFT, where the proposer identity in a proposal cannot be authenticated by verifiers, enabling potential consensus manipulation. We address this flaw by introducing proposer identity consistency checks, significantly improving protocol security.