As an emerging system programming language with a focus on safety, Rust ensures memory and concurrency safety through its innovative ownership model and borrowing mechanism. Despite its design for safety, existing research has identified several safety challenges that Rust still faces. Formal verification, grounded in rigorous mathematical principles, provides robust assurances for enhancing Rust’s security. By constructing precise and well-defined semantic models, it becomes possible to formally prove that programs adhering to Rust’s type system meet safety requirements. Automated verification tools for Rust further enable users to validate the safety and correctness of their programs. This study presents a comprehensive and systematic analysis of formal verification approaches for Rust. It begins by introducing Rust’s core semantics and complex features, followed by an exploration of research and verification efforts in Rust’s formal semantics, emphasizing the role and potential of Rust’s type system in formal verification. Next, the study systematically compares the capabilities, supported language features, underlying techniques, and application scenarios of various automated Rust verification tools. These comparisons are instrumental in guiding tool selection and integration within real-world Rust development workflows. In addition, this study summarizes exemplary cases of verified Rust programs, demonstrating the significant impact of formal verification in ensuring program correctness and providing practical tool usage recommendations for developers. Finally, it discusses the key challenges in the field and outlines promising directions for future research, including the verification of unsafe Rust code, concurrent code verification, trustworthy compilation, and large model-driven formal verification. This study aims to establish a strong security foundation for the Rust community and foster the broader adoption of formal verification methods in Rust development.