The reliability of distributed database management systems is essential in modern applications with inherently distributed architectures, such as cloud services and e-commerce platforms. The atomicity property of distributed transactions is crucial for data integrity and is typically implemented using the Two-Phase Commit (2PC) protocol. However, the correctness of 2PC in the presence of site failures, timeouts, and recovery scenarios remains complex and challenging to validate through traditional proofs alone. This work presents a formal model and verification of the 2PC protocol, including its recovery and termination subprotocols, using the CSP# language and the PAT model checker. Our approach abstracts certain system behaviors, such as communication reliability and log persistence, to improve verification efficiency while preserving correctness semantics. We explore the impact of bounded site failures and timeout occurrences on the protocol’s verifiability, revealing a direct correlation between error frequency and state-space explosion.