Software bugs often arise from inconsistencies between software requirements documented in natural language and their code implementations. Formal verification is a proven technique for solving this problem by formalizing requirements into specifications. However, specifications are notoriously difficult to write correctly. Consequently, automating the formalization of natural language requirements has attracted growing interest, especially after the advent of large language models (LLMs). This paper investigates the capability and potential of LLMs to formalize task requirements into Dafny specifications. We propose and evaluate three progressively enhanced prompting strategies—Basic Prompting, Syntax-Augmented Prompting, and Semantics-Augmented Prompting—to assess LLMs’ capability of generating Dafny specifications. Additionally, we develop an evaluation method to assess specification correctness, applicable both with and without ground truth. Experiments are carried out across three LLMs (GPT-4, DeepSeek-V3, and DeepSeek-R1) on two datasets derived from MBPP, a benchmark consisting of basic Python programming problems. Results show that Semantics-Augmented Prompting effectively improves both syntactic and semantic correctness of LLM-generated Dafny specifications. To deepen our understanding of LLMs’ formalization potential, we also conduct manual inspections and qualitative analysis, revealing the limitations of generating Dafny specifications with LLMs and bring up suggestions.