Pith. sign in

REVIEW 3 major objections 4 minor 1 cited by

Formalising Software Requirements using Large Language Models

T0 review · 3 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper announces VERIFAI, a project to automatically generate formal software specifications from natural-language requirements using large language models, with traceability from initial design through verification.

desk verdict A clear, honest two-page project announcement; the only substantive flaw is the '50% helper-assertion rate → viable to deploy' over-read, which the project's rationale leans on. read the letter →

arxiv 2506.10704 v1 pith:G6W6CTJD submitted 2025-06-12 cs.SE cs.AI

Arshad Beg , Diarmuid O'Donoghue , Rosemary Monahan This is my paper
classification cs.SEcs.AI
keywords largelanguagemodelsformalspecificationsDafnyverificationrequirementstraceabilityneuro-symbolicmethodspromptengineeringchain-of-thought
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper introduces VERIFAI, a project to automatically generate formal software specifications from natural-language requirements using large language models. The authors argue that recent tools such as Laurel, nl2spec, AssertLLM, and SpecGen show the approach is becoming viable, and they plan to push it further with better prompts, chain-of-thought reasoning, and neuro-symbolic systems that let theorem provers correct the LLM's output. If the project succeeds, requirements could be traced from initial design through implementation and verification, reducing the cost and training burden of formal methods. The paper is a position statement rather than a report of results; its central claim is that this research agenda is feasible and worth pursuing.

What carries the argument

The central object is the VERIFAI pipeline, which is not yet implemented but is described as combining LLM-based generation of formal specs, domain ontologies to describe the software system, similarity-based reuse of existing artifacts, and a neuro-symbolic loop where a theorem prover checks and provides feedback on generated assertions. The Dafny verification-aware programming language serves as the target notation in the paper's running example, where a helper assertion inserted into a lemma helps the SMT solver prove string-concatenation properties.

What would settle it

Take a benchmark of natural-language requirements with known correct formal specifications, run VERIFAI's full pipeline (prompt engineering, chain-of-thought, neuro-symbolic refinement) on them, and compare the fraction of generated specifications that pass verification and match the reference spec. If it does not exceed Laurel's 50% helper-assertion rate or SpecGen's 279-out-of-384 success rate, the claimed feasibility is not established.

Watch

Extended reading notes

Core claim

The paper's central claim is that the gap between informal natural-language requirements and rigorous formal specifications can be bridged more effectively than current tools do, by combining refined prompt engineering, chain-of-thought reasoning, and hybrid neuro-symbolic approaches. It cites existing systems that already generate substantial fractions of correct specifications, such as Laurel's 50% helper-assertion success and SpecGen's 279 verified programs out of 384, as evidence that the underlying approach is viable, and it presents the VERIFAI project as the next step to improve on those results. No experimental results from VERIFAI itself are reported; the paper is a proposal and a survey.

Load-bearing premise

The whole project rests on the premise that prompts, chain-of-thought steps, and theorem-prover feedback can push LLM-generated formal specifications to be correct enough for automated verification.

Editorial extensions

If this is right

  • If the agenda works, developers without formal-methods training could produce verifiable specifications directly from natural language, easing the 30% overhead cited for formal methods adoption.
  • Traceability from a natural-language requirement through implementation to a machine-checked proof would become automated, which matters for safety-critical certification.
  • The proposed neuro-symbolic loop would let theorem-prover feedback correct LLM output, turning verification failures into training or refinement signals.
  • Success would extend demonstrated results like Laurel's 50% helper-assertion rate and SpecGen's 279/384 verifiable programs toward higher coverage and broader language targets.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the approach generalizes beyond Dafny, the same prompt-plus-refinement pattern could apply to other target notations such as JML, ACSL, and temporal logics, lowering the entry barrier across safety-critical domains.
  • The traceability claim, if realized, could shorten certification evidence chains by linking each verified implementation step back to the original natural-language requirement.
  • A testable extension would be a benchmark that measures not just whether a generated spec passes verification but whether it matches the user's intended meaning, since a syntactically correct but semantically wrong spec can pass verification.
  • The project's feasibility ultimately depends on whether LLM-generated specs can meet the bar of being correct enough that a theorem prover can finish the proof, which may require not just better prompts but also a way to detect and repair specifications that are internally consistent yet wrong.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. This short paper introduces VERIFAI, a recently initiated project on the traceability and verification of natural-language requirements. It reproduces a Dafny helper-assertion example from the Laurel framework, surveys recent LLM-based specification generation tools (nl2spec, AssertLLM, SpecLLM, JML translation studies, Explanation-Refiner, PathCrawler/EVA, SpecGen, BPM-to-NL, and NL2SQL), and states the project's intended directions: refinement of prompt engineering, incorporation of chain-of-thought reasoning, and development of hybrid neuro-symbolic approaches. The paper presents no experimental results of its own.

Significance. If the VERIFAI agenda succeeds, it could reduce the cost of formal specification generation and traceability in safety-critical software, which is a recognized bottleneck for the industrial adoption of formal methods. The paper's current contribution is as a project announcement and a selective literature review; it does not yet provide a technical solution or validation. The cited related work demonstrates growing activity in the area, and the proposed integration of neuro-symbolic feedback and traceability is a reasonable topic for further research. A strength of the paper is that it consolidates recent results in one table, which is useful for positioning the project.

major comments (3)
  1. [Section 2] The statement that Laurel's generation of "over 50% of the required helper assertions" makes it "a viable approach to deploy" is not supported by the cited result: a 50% generation rate leaves half of the assertions to be supplied manually, and the paper does not report an end-to-end verification success rate or an analysis showing that the missing assertions are easy to supply. Because this viability judgment is the main empirical premise motivating the VERIFAI agenda in Section 4, the claim needs to be either replaced with accurate quantitative evidence or explicitly softened.
  2. [Section 4] The paper's stated plan to "improve the techniques" through prompt engineering, chain-of-thought reasoning, and hybrid neuro-symbolic approaches is only a list of directions; the paper provides no architecture, evaluation methodology, or preliminary results for any of these ideas. As a project introduction, the paper should at least specify concrete research questions, success criteria, and comparison baselines so that the proposed agenda can be assessed.
  3. [Abstract and Section 4] The abstract and Section 4 mention NLP, ontologies, similarity-based reuse, and an AI-guided process as part of VERIFAI, but the body of the paper does not describe how these approaches will be integrated or what role they play relative to LLM-based generation. This omission makes it difficult to distinguish the project's intended contribution from the related work surveyed in Section 3.
minor comments (4)
  1. [Section 2.2] The Dafny code block has a formatting error: "asserts1 + "." + s2 == [s1[0]]..." should read "assert s1 + "." + s2 == [s1[0]]..." (missing space). The ensures clause "ParseDecStr(s1+"."+s2).value.1" also appears to be a typo (likely ".value.0" or similar) and should be corrected.
  2. [Section 3] The sentence "It is done in three phases, first understanding specifications, mapping signal definitions and generating assertions." is a sentence fragment and should be completed, for example as "The pipeline proceeds in three phases: understanding specifications, mapping signal definitions, and generating assertions."
  3. [References] The reference list has inconsistent formatting: [1] is dated 2024 but the arXiv URL is 2002.07279; [4] lacks page numbers or an article number; [11] contains a stray period before "Berlin". These should be harmonized with the venue's style.
  4. [Table 1] The table header is typeset as "Table 1:Summary", missing a space after the colon. In addition, the table is not referenced in the body text, so readers do not know how the table relates to the surrounding discussion.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the paper is a position/survey piece with no fitted parameters, no derivation chain, and no load-bearing self-citations.

full rationale

The paper makes no predictive or derivational claim that could reduce to its own inputs. It summarises existing external tools (Laurel, nl2spec, AssertLLM, SpecLLM, SpecGen, etc.) and then states a research agenda for the authors' own project VERIFAI: 'In VERIFAI, we aim to improve the techniques that bridge this gap, through refinement of prompt engineering, the incorporation of chain-of-thought reasoning and the development of hybrid neuro-symbolic approaches.' This is explicitly an aim, not a result, and no equation, fitted parameter, or benchmark outcome is derived from it. The only quantitative claims quoted, such as Laurel's 'over 50% of the required helper assertions' and SpecGen's '279 out of 384 programs', are attributed to external papers with citations, and they are not used to define any output of this paper. There is no self-citation chain: the authors cite only external prior work, and none of those citations is invoked to force a conclusion in the present paper. The skeptical concern that a 50% helper-assertion rate does not establish that LLM-based specification generation is 'a viable approach to deploy' is a critique of evidential strength or logical sufficiency, not circularity: the claim is borrowed from an external source and is not being used to derive the same claim by construction. The paper therefore imposes no circularity burden, and the appropriate finding is no significant circularity with score 0.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The paper's agenda rests on the reported success of existing LLM-to-specification tools, the value of formal verification, and the assumption that prompt engineering, chain-of-thought, and neuro-symbolic refinement will produce correct specifications. None of these are demonstrated in this paper.

assumptions (3)
  • domain assumption LLM-generated helper assertions can substantially automate program verification, based on Laurel's reported 50% success rate.
    Section 2 relies on [2]'s reported result as a motivating example, but the paper offers no independent replication.
  • domain assumption Formal specifications and verification are necessary for correctness in safety-critical software, and the 30% cycle-time increase from formal methods [1] is accurate.
    The Introduction cites [1] for the 30% overhead and treats formal verification as the desired standard without questioning it.
  • ad hoc to paper Large language models can be steered by prompt engineering, chain-of-thought, and neuro-symbolic feedback to generate correct formal specifications.
    Section 4 states this as the project's plan, but no experiment in this paper demonstrates it.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Formalising Software Requirements using Large Language Models." pith.science (2026). https://pith.science/paper/G6W6CTJD

@misc{pith2026250610704,
  author       = {Pith},
  title        = {Pith review of: Formalising Software Requirements using Large Language Models},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/G6W6CTJD}},
  note         = {Machine review of arXiv:2506.10704}
}
read the original abstract

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.

Discussion (0). Sign in to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects

    cs.SE 2025-07 conditional novelty 4.0 of 10

    LLM-based formalisation of software requirements is promising but faces five persistent challenges; the proposed VERIFAI framework plans to address them with human-in-the-loop and tool-neutral pipelines.

Reference graph

Works this paper leans on

11 extracted references · 4 canonical work pages · cited by 1 Pith paper

  1. [1]

    Formal methods: From academia to industrial practice. a travel guide,

    M. Huisman, D. Gurov, and A. Malkis, “Formal methods: From academia to industrial practice. a travel guide,” 2024. [Online]. Available: https://arxiv.org/abs/2002.07279

    arXiv 2024

  2. [2]

    Laurel: Generating dafny assertions using large language models,

    E. Mugnier, E. A. Gonzalez, R. Jhala, N. Polikarpova, and Y . Zhou, “Laurel: Generating dafny assertions using large language models,” 2024. [Online]. Available: https: //arxiv.org/abs/2405.16792

    arXiv 2024

  3. [3]

    nl2spec: Interactively translating unstructured natural language to temporal logics with large language models,

    M. Cosler, C. Hahn, D. Mendoza, F. Schmitt, and C. Trippel, “nl2spec: Interactively translating unstructured natural language to temporal logics with large language models,” 2023. [Online]. Available: https://arxiv.org/abs/2303.04864

    arXiv 2023

  4. [4]

    As- sertllm: Generating hardware verification assertions from design specifications via multi-llms,

    W. Fang, M. Li, M. Li, Z. Yan, S. Liu, H. Zhang, and Z. Xie, “As- sertllm: Generating hardware verification assertions from design specifications via multi-llms,” in2024 IEEE LLM Aided Design Workshop (LAD), 2024, pp. 1–1

    work page 2024

  5. [5]

    Specllm: Exploring generation and review of vlsi design specification with large language model,

    M. Li, W. Fang, Q. Zhang, and Z. Xie, “Specllm: Exploring generation and review of vlsi design specification with large language model,” 2024. [Online]. Available: https://arxiv.org/abs/ 2401.13266

    arXiv 2024

  6. [6]

    Translating natural language require- ments to formal specifications: A study on gpt and symbolic nlp,

    I. T. Leong and R. Barbosa, “Translating natural language require- ments to formal specifications: A study on gpt and symbolic nlp,” in2023 53rd Annual IEEE/IFIP International Conference on De- pendable Systems and Networks Workshops (DSN-W), 2023, pp. 259–262

    work page 2023

  7. [7]

    Verification and refinement of natural language explanations through llm-symbolic theorem proving,

    X. Quan, M. Valentino, L. A. Dennis, and A. Freitas, “Verification and refinement of natural language explanations through llm-symbolic theorem proving,” 2024. [Online]. Available: https://arxiv.org/abs/2405.01379

    arXiv 2024

  8. [8]

    Specify what? en- hancing neural specification synthesis by symbolic methods,

    G. Granberry, W. Ahrendt, and M. Johansson, “Specify what? en- hancing neural specification synthesis by symbolic methods,” in Integrated F ormal Methods, N. Kosmatov and L. Kovács, Eds. Cham: Springer Nature Switzerland, 2025, pp. 307–325

    work page 2025

Show all 11 references
  1. [9]

    Specgen: Automated generation of formal program specifications via large language models,

    L. Ma, S. Liu, Y . Li, X. Xie, and L. Bu, “Specgen: Automated generation of formal program specifications via large language models,” 2024. [Online]. Available: https: //arxiv.org/abs/2401.08807

    2024 arXiv

  2. [10]

    Supporting pro- cess model validation through natural language generation,

    H. Leopold, J. Mendling, and A. Polyvyanyy, “Supporting pro- cess model validation through natural language generation,”IEEE Transactions on Software Engineering, vol. 40, no. 8, pp. 818– 840, 2014

    2014

  3. [11]

    Bis: Nl2sql service evaluation benchmark for business intelligence scenarios,

    B. Caglayan, M. Wang, J. D. Kelleher, S. Fei, G. Tong, J. Ding, and P. Zhang, “Bis: Nl2sql service evaluation benchmark for business intelligence scenarios,” inService- Oriented Computing: 22nd International Conference, ICSOC 2024, Tunis, Tunisia, December 3–6, 2024, Proceedin...

    2024 doi

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.