We investigated the Tendermint protocol, a core Byzantine Fault Tolerance (BFT) consensus engine for the Cosmos Blockchain. When modelling this protocol, we faced significant challenges in the computational performance of verification. To mitigate the state-space explosion issue, we improve the model with optimisation techniques, such as partial-order reduction and role-based symmetry reduction. Through verification, we discovered vulnerabilities in the design of Tendermint, and we proposed fixes that regained both the safety and liveness properties. This paper describes our modelling techniques and optimisations, analyses the vulnerabilities and fixes, and discusses how the optimisations impact verification runtime and results.