As an emerging safe system programming language, Rust provides guarantees for memory safety and concurrency safety with its innovative ownership model and borrowing mechanism. Although Rust focuses on safety, existing works has revealed numerous safety challenges it still faces. Formal verification is a method based on rigorous mathematical foundations. It offers strong assurance for enhancing Rust's security. By formalizing precise and clear semantic models, it is possible to prove that programs adhering to Rust's typing rules meet safety requirements. Automated Rust verification tools can assist users in ensuring the safety and correctness of Rust programs. This survey provides a comprehensive and systematic analysis of Rust formal verification. First, it introduces the core semantics and complex features of Rust, and discusses research and verification work on Rust's formal semantics afterwards, highlighting the potential of Rust's type system in formal verification. Second, the paper systematically compares the abilities, language features supported, underlying technologies, and applicable scenarios of different Rust automated verification tools. It is significant for guiding the selection and integration of tools in the actual development process of Rust projects. Additionally, this paper summarizes verified Rust systems, demonstrating the remarkable effectiveness of formal verification in ensuring program correctness, and provides tool selection recommendations for users. Finally, this paper concludes by discussing the current challenges in the field and pointing out directions for future research, including the verification of unsafe Rust code, concurrent code verification, trustworthy compilation, and formal verification driven by large models. This paper aims to provide a solid security foundation for the Rust community and promote the application of formal verification in Rust development.