The return of formal requirements engineering in the era of large language models

Context and Motivation: Large Language Models (LLMs) have made remarkable advancements in emulating human linguistic capabilities, showing potential in executing various traditional software engineering tasks, including code generation. [Question/Problem] Despite their generally good performance, utilizing LLM-generated code raises legitimate concerns regarding its correctness and the assurances it can provide. [Principal Idea/Results] To address these concerns, we propose turning to formal requirements engineering—a practice currently predominantly used in developing complex systems where adherence to standards and accountability are required. [Contribution] In this vision paper, we discuss the integration of automatic formal requirements engineering techniques as a complement to LLM code generation. Additionally, we explore how LLMs can facilitate the broader acceptance of formal requirements, thus making the vision proposed in this paper realizable.