Formal software verification ensures the correctness and reliability of software systems through mathematical methods and logical reasoning, and it is widely applied in domains with high safety requirements. However, traditional formal verification techniques face challenges such as low levels of automation, insufficient reasoning efficiency, and difficulties in scaling, making it hard to meet the rapidly evolving demands of complex software systems. In recent years, the rapid development of large language models (LLMs) has brought revolutionary breakthroughs in fields such as natural language processing, code understanding, and code generation, offering new automated solutions for formal verification. To systematically review and analyze the current research status and future trends of LLM-powered software formal verification, this paper provides a comprehensive survey of relevant studies. First, it outlines the core processes and methods of software formal verification, as well as the key LLM-related technologies applied in this domain. The paper then focuses on two major application scenarios of LLMs: (1) the transformation from natural language to formal specifications, which explores how LLMs can automatically convert ambiguous natural language requirements into formal specifications, thereby lowering the barriers to model construction and property specification in formal verification; (2) specification synthesis and reasoning support in program verification, which investigates the potential of LLMs to assist in proof generation within theorem prover technologies, including the automatic extraction of intermediate properties such as preconditions, postconditions, and invariants through code analysis, and their potential to optimize verification strategies or reduce state space exploration in model checking. Finally, this paper summarizes the challenges faced by LLM technologies in software formal verification and discusses potential future research directions.