# A Short Survey on Formalising Software Requirements using Large Language Models

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 13 Jun 2025.

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

- [AgentGuard: Runtime Verification of AI Agents](https://mlsanity.com/paper/2509.23864/) (2025)
- [StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion](https://mlsanity.com/paper/2508.04440/) (2025)
- [Working Document -- Formalising Software Requirements with Large Language Models](https://mlsanity.com/paper/2506.14627/) (2025)
- [AI for software engineering: from probable to provable](https://mlsanity.com/paper/2511.23159/) (2025)

## Abstract (arXiv)

This paper presents a focused literature survey on the use of large language models (LLM) to assist in writing formal specifications for software. A summary of thirty-five key papers is presented, including examples for specifying programs written in Dafny, C and Java. This paper arose from the project VERIFAI - Traceability and verification of natural language requirements that addresses the challenges in writing formal specifications from requirements that are expressed in natural language. Our methodology employed multiple academic databases to identify relevant research. The AI-assisted tool Elicit facilitated the initial paper selection, which were manually screened for final selection. The survey provides valuable insights and future directions for utilising LLMs while formalising software requirements.