# Formalising Software Requirements using Large Language Models

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 13 references that are in the map.
- First posted on arXiv 12 Jun 2025.

## Builds on (most cited first, 8 of 8)

- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [SpecGen: Automated Generation of Formal Program Specifications via Large Language Models](https://mlsanity.com/paper/2401.08807/) (2024)
- [Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving](https://mlsanity.com/paper/2405.01379/) (2024)
- [AssertLLM: Generating Hardware Verification Assertions from Design Specifications via Multi-LLMs](https://mlsanity.com/paper/2411.14436/) (2024)
- [SpecLLM: Exploring Generation and Review of VLSI Design Specification with Large Language Model](https://mlsanity.com/paper/2401.13266/) (2024)
- [Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods](https://mlsanity.com/paper/2406.15540/) (2024)
- [Formal Methods: From Academia to Industrial Practice. A Travel Guide](https://mlsanity.com/paper/2002.07279/) (2020)
- [BIS: NL2SQL Service Evaluation Benchmark for Business Intelligence Scenarios](https://mlsanity.com/paper/2410.22925/) (2024)

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

- [Working Document -- Formalising Software Requirements with Large Language Models](https://mlsanity.com/paper/2506.14627/) (2025)
- [Neurosymbolic Auditing of Natural-Language Software Requirements](https://mlsanity.com/paper/2605.13817/) (2026)

## Abstract (arXiv)

This paper is a brief introduction to our recently initiated project named VERIFAI: Traceability and verification of natural language requirements. The project addresses the challenges in the traceability and verification of formal specifications through providing support for the automatic generation of the formal specifications and the traceability of the requirements from the initial software design stage through the systems implementation and verification. Approaches explored in this project include Natural Language Processing, use of ontologies to describe the software system domain, reuse of existing software artefacts from similar systems (i.e. through similarity based reuse) and large language models to identify and declare the specifications as well as use of artificial intelligence to guide the process.