In recent years, the number of scenarios requiring secure communication between multiple users has increased, driven by factors such as the rise of remote work and the increased use of social networking services. As a result, many new cryptographic protocols have been developed. However, these protocols are often modified and employed without sufficient security verification. The aim of this study is to verify that the Messaging Layer Security (MLS) protocol, standardized as RFC 9420 in 2023, satisfies security requirements using ProVerif. The MLS protocol provides mechanisms to ensure message secrecy, message integrity, and sender authentication. In this study, we verify the soundness of a formalized MLS model and evaluate its compliance with security requirements. The model is based on the Ratchet Tree structure, which is the core technology of MLS. Although MLS provides both forward and backward secrecy, we focus on the latter, particularly in the case of secret key leakage. Our results demonstrate that the formalized model meets MLS security requirements.