With the continuous development of blockchain technology and applications, the demand for interaction between blockchains is increasing. However, the lack of effective interoperability between different blockchain systems limits the further development of blockchain technology. To address the problem of heterogeneous interconnection between blockchains, cross-chain technology has emerged and quickly become a prominent research topic. Specifically, the XCMP protocol, one of the most popular cross-chain communication protocols, not only provides a secure and efficient communication mechanism but also offers a broad platform for future blockchain innovation and applications. However, the cross-chain massage passing (XCMP) protocol is still in a phase of continuous development and improvement, facing security challenges such as replay attacks, denial of service attacks, and delay attacks. This study formally verifies and improves the XCMP protocol, aiming to provide solid support for the development of more secure and feature-rich decentralized applications based on it. First, Z language, a formal description language based on classical set theory and first-order predicate logic, is used to summarize, refine, and formally model the 10 key security goals and protocol contents of the XCMP protocol. The security goals are then verified using Z/EVES, an automated verification tool supporting the Z language. The verification results show that the XCMP protocol does not meet three of the security goals. Second, after a comprehensive analysis of the verification results, the study introduces a commitment mechanism, a supervision mechanism, and a polling mechanism to address unmet security goals of the XCMP protocol, proposing an enhanced cross-chain message passing (E-XCMP) protocol. Finally, the E-XCMP protocol is formally modeled, and its security and reliability are evaluated using the security protocol analysis tool Scyther and the automatic verification tool Z/EVES. The evaluation results show that the E-XCMP protocol not only meets the three previously unmet security goals but also effectively solves security issues such as replay attacks, denial of service attacks, and delay attacks, demonstrating strong security and reliability.