The design of contemporary critical systems involves numerous requirements that must be clearly and coherently articulated, posing significant challenges for system designers. This paper addresses the challenge of translating ambiguous Natural Language (NL) requirements into unambiguous Computation Tree Logic (CTL) specifications, an essential task for maintaining consistency and precision in system design. We introduce Natural2CTL, a novel dataset comprising 2,095 pairs of NL requirements and their CTL specifications. textcolor{red}{A key aspect of this research includes a detailed methodology for data collection and annotation. The robustness of Natural2CTL is established through rigorous validation processes, including evaluations by academic and industry experts, inter-rater reliability assessments, and practical verification using UPPAAL case studies. These validation efforts underscore the dataset’s reliability and its potential applicability in both research and educational domains within Requirements Engineering (RE) and formal methods.