# Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects

arXiv: https://arxiv.org/abs/2507.14330 · HTML: https://mlsanity.com/paper/2507.14330/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 18 Jul 2025.

## Built on by (most cited first, 5 of 5)

- [Watchdogs and Oracles: Runtime Verification Meets Large Language Models for Autonomous Systems](https://mlsanity.com/paper/2511.14435/) (2025)
- [Evaluating LLM-Generated ACSL Annotations for Formal Verification](https://mlsanity.com/paper/2602.13851/) (2026)
- [Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation](https://mlsanity.com/paper/2606.05792/) (2026)
- [Ambiguity Detection and Elimination in Automated Executable Process Modeling](https://mlsanity.com/paper/2604.10884/) (2026)
- [Towards an Agentic LLM-based Approach to Requirement Formalization from Unstructured Specifications](https://mlsanity.com/paper/2604.18228/) (2026)

## Abstract (arXiv)

Software correctness is ensured mathematically through formal verification, which involves the resources of generating formal requirement specifications and having an implementation that must be verified. Tools such as model-checkers and theorem provers ensure software correctness by verifying the implementation against the specification. Formal methods deployment is regularly enforced in the development of safety-critical systems e.g. aerospace, medical devices and autonomous systems. Generating these specifications from informal and ambiguous natural language requirements remains the key challenge. Our project, VERIFAI^{1}, aims to investigate automated and semi-automated approaches to bridge this gap, using techniques from Natural Language Processing (NLP), ontology-based domain modelling, artefact reuse, and large language models (LLMs). This position paper presents a preliminary synthesis of relevant literature to identify recurring challenges and prospective research directions in the generation of verifiable specifications from informal requirements.