Traceable and Verifiable Software Requirements: A Synthesis of AI-Enabled Formal Methods

Received: Added at production Revised: Added at production Accepted: Added at production DOI: xxx/xxxx R E G U L A R P A P E R Traceable and Verifiable Software Requirements: A Synthesis of AI-Enabled Formal Methods Arshad Beg Diarmuid O’Donoghue Rosemary Monahan 1Department of Computer Science, Maynooth University, Co. Kildare, Ireland Correspondence Corresponding author: Arshad Beg, Email: [email protected] Diarmuid O’Donoghue, Email: [email protected] and Rosemary Monahan, Email: rosemary[email protected]. Present address Department of Computer Science, Maynooth University, Ireland. Abstract The generation of formal specifications from informal, natural language requirements remains a critical challenge in ensuring software correctness, particularly in safety-critical domains such as aerospace, autonomous systems, and medical devices. This paper presents a comprehensive survey and synthesis of recent research exploring the use of large language models (LLMs) and AI-driven techniques in the formalisation of software requirements. Drawing on an analysis of more than one hundred studies, it identifies state-of-the-art methods for translating natural language requirements into formal specifications across various programming languages and verification tools, including model checkers and theorem provers. Beyond technical methodologies, the work highlights key challenges in requirements traceability, tool integration, and specification reuse. Complementing this survey, the paper reports an empirical evaluation of Frama-C plugins, including the Runtime Error (RTE) and Value Analysis (EVA) analysers, as well as the PathCrawler automatic test generation tool. These experiments assess the capability of formal analysis tools to infer assertions, generate ANSI/ISO C Specification Language (ACSL) annotations, detect runtime anomalies, and produce test cases for representative C programs. The study identifies practical barriers such as solver instability, path coverage constraints, and tool-specific restrictions, proposing strategies like dataset adaptation, selective path exploration, and local configuration to overcome them. The findings demonstrate that automated formalisation and verification workflows can enhance program correctness while emphasising the continued importance of human-guided intervention and coordinated multi-tool use. KEYWORDS Static Program Analysis, ACSL Annotation, Frama-C EVA, Runtime Error Detection, Specification Automation 1 INTRODUCTION Relying solely on natural language to express software requirements has long been recognised as a persistent source of ambiguity and misinterpretation. Even when written with care, natural language statements frequently conceal implicit assumptions, under-specify critical behaviours, or introduce unintended vagueness that becomes apparent only during system testing or operation. Such ambiguities are not merely stylistic defects: when left unresolved, they propagate throughout the development process, influencing architectural decisions, implementation strategies, and verification activities. More critically, requirements that are not grounded in a precise mathematical notation cannot benefit from the guarantees provided by formal verification techniques, which are essential for demonstrating compliance with rigorous industrial and regulatory standards for safety-critical software systems1,2,3. These standards increasingly demand evidence that system behaviour has been analysed exhaustively and that potential faults–especially those arising from concurrency, non-determinism, or intricate reactive control–have been eliminated before deployment. However, bridging this gap between natural language and formal verification remains a substantial challenge in practice. Abbreviations: Value Analysis (EVA) Tool, Runtime Error (RTE) Tool, ANSI/ISO C Specification Language (ACSL), Java Modelling Language (JML). J. Softw. Test. Verif. Reliab. 2025;00:1–35 wileyonlinelibrary.com/journal/ © 2025 wileyonlinelibrary.com/journal/stvr 1 2BEG ET AL. Creating formal specifications e.g.4is a technically demanding task, requiring a solid foundation in formal logic, specification languages, and reasoning techniques. Engineers must not only understand the domain but also possess the specialised training needed to express requirements in a mathematically rigorous form and to manipulate these expressions through proof obligations, model-checking artefacts, or refinement steps. As a consequence, introducing formal specifications into an existing development workflow can significantly increase the effort and time required; empirical observations suggest that the specification and verification phases may lengthen the development cycle by roughly thirty percent5. For many organisations, operating under tight commercial timelines, the use of formal methods is compromised. We seek to mitigate the burden of writing formal specifications, enabling practitioners to reap the advantages of formal verification without requiring deep expertise in advanced proof methods or accepting prohibitive overheads. By doing so, we aim to narrow the long-standing gap between the theoretical value of formal verification and its limited adoption in mainstream software engineering practice. The importance of accessible and effective formalisation becomes particularly clear when examining real-world systems in which subtle concurrency or coordination errors can have catastrophic consequences. Formalising requirements ensures not only clarity and internal consistency but also the ability to subject system behaviour to algorithmic scrutiny using techniques such as theorem proving and model checking. A compelling demonstration of this appears in the foundational work of6, which apply model checking to the plan execution module of NASA’s Remote Agent, flown on the Deep Space 1 mission. By translating ESL–a domain-specific reactive control language implemented in multi-threaded Common Lisp–into the PROMELA modelling language used by the SPIN model checker, the authors uncovered five previously undetected concurrency defects. Remarkably, one of these defects corresponded directly to a bug that later manifested as an in-flight deadlock, demonstrating that even extensive testing campaigns can fail to reveal elusive design flaws that formal analysis exposes with precision. As highlighted poignantly in6: “In fact, in a different part of the system, a concurrency bug identical to one discovered by this study escaped testing and caused a deadlock during an in-flight experiment 96 million kilometers from Earth.” This incident not only reaffirms the indispensable role of formal verification tools in safety-critical contexts but also stimulated the evolution of SPIN itself, inspiring the introduction of procedural abstraction through inline procedures to better support complex system modelling. Together, these observations illustrate both the necessity and the challenge of integrating formalism into requirements engineering. On one hand, formal methods demonstrably enhance system correctness, resilience, and predictability; on the other, their steep learning curve and labour-intensive nature impede widespread adoption. Like all other fields, the development of Large Language Models (LLMs) has opened a world of opportunities where we can exploit their power to generate formal requirements and accompanying specifications. This work aims to provide a feasibility to make the process of writing formal specifications more inituitive, less time-consuming, and more compatible with modern industrial development practices. Generating Assertions Adding annotations in imperative languages such as C, Java, and Dafny makes the intended behaviour of functions and contracts explicit, providing a precise semantic basis for verification tools. These annotations allow formal verifiers to reason about state changes and invariants, turning implicit programmer intent into machine-checkable correctness guarantees. Dafny is a verification-aware programming language that has native support for expressing formal specifications and is equipped with a static program verifier to automatically verify implementations against specifications using deductive verification. We illustrate an example using a Dafny lemma as reported in7, where a helper assertion is needed in the verification process. Lemmas are used in Dafny to specify properties that may be used in the verification process. The lemma, defined below, ensures that the integer and fractional parts are correctly extracted while parsing a decimal string. The figure 1 presents the formal specification of the ParseDigitsAndDot lemma across three different languages and specification tools: Dafny, JML, and ACSL. Subfigure (a) illustrates the Dafny version of the lemma, which uses preconditions and postconditions to specify the correct behavior of string parsing, along with helper assertions in both the base and recursive cases. Subfigure (b) shows the JML annotations within a Java implementation, where similar preconditions and postconditions are defined, ensuring the string parsing behaves as expected. Finally, subfigure (c) demonstrates the equivalent ACSL annotations within C code, specifying the same formal properties and using assertions to validate the base and recursive cases. Now, we explain the lemma body presented in Figure 1: The function’s precondition (the requires clause) states that every character in s1 must be a digit ranging from ’0’ to ’9’. Its postcondition (the ensures clause) guarantees that when ParseDecStr is applied to the concatenation of s1 and s2, the resulting pair preserves s1 as the integer part while placing "." + s2 as the fractional part. In the base case, where s1 consists of only one character, the function asserts that parsing "." + s2 yields an empty integer part. In the recursive case, the function processes the tail of s1 by recursively calling Traceable and Verifiable Software Requirements: A Synthesis of AI-Enabled Formal Methods 3 (a) Dafny Lemma lemma ParseDigitsAndDot(s1: string, s2: string) requires forall i | 0 <= i < |s1| :: ’0’ <= s1[i] <= ’9’ ensures ParseDecStr(s1 + "." + s2).value.1 == "." + s2 { if |s1| == 1 { assert ParseDecStr("." + s2).None?; } else { ParseDigitsAndDot(s1[1..], s2); assert s1 + "." + s2 == [s1[0]] + (s1[1..] + "." + s2); } } (b) JML Annotations with Java Code /*@ requires (\forall int i; 0 <= i && i < s1.length() ==> (’0’ <= s1.charAt(i) && s1.charAt(i) <= ’9’)); @ ensures ParseDecStr(s1 + "." + s2) .value[1].equals("." + s2); @*/ void ParseDigitsAndDot(String s1, String s2) { if (s1.length() == 1) { //@ assert ParseDecStr("." + s2).isNone(); } else { ParseDigitsAndDot(s1.substring(1), s2); //@ assert (s1 + "." + s2).equals( //@ s1.charAt(0) + "" + (s1.substring(1) + "." + s2)); } } (c) ACSL Annotations with C Code /*@ requires \forall integer i; 0 <= i < strlen(s1) ==> (’0’ <= s1[i] && s1[i] <= ’9’); ensures ParseDecStr(concat3(s1, ".", s2)).value_1 == concat(".", s2); */ void ParseDigitsAndDot(char*s1, char*s2) { if (strlen(s1) == 1) { //@ assert ParseDecStr(concat(".", s2)).None; } else { ParseDigitsAndDot(s1 + 1, s2); //@ assert concat3(s1, ".", s2) == //@ concat3(char_to_string(s1[0]), //@ s1+1, concat(".", s2)); } } F I G U R E 1 (a) Dafny lemma, (b) JML annotations with Java code, and (c) ACSL annotations with C code for the ‘ParseDigitsAndDot’ lemma. itself. To make the intended string decomposition clear to the verifier, an assertion is added: assert s1 + "." + s2 == [s1[0]] + (s1[1..] + "." + s2);. This assertion explicitly demonstrates how the string is broken down, which helps the SMT solver reason about the transformation and verify correctness. Role of the Helper Assertion: Without the assertion, the Dafny verifier struggles to establish the correctness of the postcondition due to the complexity of reasoning about string concatenation. The assertion serves as an intermediate step, breaking down the transformation into a form that is easier for the solver to handle. This example motivates our work by demonstrating the importance of inserting specifications in the form of helper assertions in formal proofs using different specification languages. Tools like Laurel7aim to automate this process by leveraging Large Language Models to determine the relevant assertions. Key Contributions This paper makes the following key contributions to the field of automated formal specification and software verification: 1. Comprehensive Survey of AI-driven Formalisation: We present an extensive review of more than one hundred recent research studies on translating natural language requirements into formal specifications. The survey highlights state-ofthe-art methodologies, including natural language processing (NLP), ontology-based domain modelling, software artefact reuse, and the application of large language models (LLMs), providing a structured overview of effective approaches across programming languages and verification tools. 4BEG ET AL. 2. Empirical Evaluation of Verification Tools: The study performs a detailed empirical assessment of Frama-C plugins (RTE and EVA analysers) and the PathCrawler test generation tool. Experiments evaluate their capability to infer assertions, generate ACSL specifications, detect runtime errors, and explore execution paths in representative C programs. The results offer practical insights into tool strengths, limitations, and areas requiring human-guided intervention. 3. Identification of Practical Challenges: Through both survey and experiments, we highlight key barriers in automated formalisation, including solver instability, limited path coverage, ambiguous postconditions, and tool-specific constraints. This analysis informs strategies such as dataset adaptation, selective path exploration, and configuration tuning to enhance verification reliability. 4. Roadmap for Intelligent Specification Workflows: Based on observed results, we propose future directions for improving automation, traceability, and verifiability in high-assurance systems. This includes stronger solver support, richer ACSL templates, cross-tool orchestration, and human-in-the-loop strategies to achieve reliable and scalable formalisation. The paper is structured as follows. Section 2 surveys existing research and synthesises key observations. This section contains several subsections that review major research directions, including LLM prompting strategies for program analysis, deductiveverification tooling, static-analysis frameworks, test-generation tools, and automated ACSL specification generation. Each subsection outlines core contributions, methodological trends, and gaps in the current state of the art. Section 3 then describes our methodology for running initial experiments with PathCrawler, using prompts adapted from8. Here, sub-section 3.2 presents the empirical evaluation of deductive verifiers on the 36-program Frama-C tutorial set. Following this, sub-section 4.1 reports the results of static analysis performed with EVA on the dataset provided by8, after which ACSL annotations generated by RTE are evaluated with deductive verifiers. Experience with Pathcrawler test case generation is reported in sub-section 4.3. Section 5 synthesises insights from both the literature and empirical evaluations to outline the major challenges and corresponding future research directions. Each subsection discusses a specific challenge–such as variability in LLM-generated prompts, limitations in ACSL specification quality, interoperability issues across verification tools, scalability constraints when analysing larger programs, insufficient standardised benchmarks, and the need for more rigorous evaluators–and pairs it with actionable future directions aligned with these findings. Finally, Section 6 concludes the paper by summarising contributions and outlining possible avenues for extending automated verification workflows. 2 STATE OF THE ART This section reviews prior work that forms the basis for our investigation into automated software verification and specification generation. The goal is to situate our methodology and experimental design within the broader context of existing tools, analysis techniques, and recent attempts to incorporate large language models into verification workflows. We survey contributions spanning deductive verification, static analysis, automated test generation, and ACSL specification inference, with particular attention to empirical findings and methodological practices reported in the literature. By examining these developments together, we identify the recurring patterns, assumptions, and limitations that shape current approaches. The synthesis provided here serves as the foundation for the experimental choices and evaluation criteria used in the remainder of the paper. 2.1 Methodology for Literature Review In this section, we present the results of our structured literature review which examines how large language models are currently used to assist in writing formal specifications. Main research questions for conducting systematic literature review on the topic are as follows: RQ1: What methodologies leverage Large Language Models (LLMs) to transform natural language software requirements into formal notations? RQ2: What are the emerging trends and future research directions in using LLMs for software requirements formalisation? To conduct a structured and thorough review of literature on Natural Language Processing (NLP), Large Language Models (LLMs), and their use in software requirements, the following approach is followed. Several academic databases, including IEEE Xplore, ACM Digital Library, Scopus, Springer Link, and Google Scholar, are searched using specific keywords. The core search terms include “NLP,” “LLMs,” and “Software Requirements,” with broader terms such as “specification,” “logic,” “verification,” “model checking,” and “theorem proving” used to expand the scope. The number of results differs notably across Traceable and Verifiable Software Requirements: A Synthesis of AI-Enabled Formal Methods 5 databases, with some sources returning only small collections of studies, while Google Scholar provides large volume of 8,640 references. It reduced to 7,780 when filter of since 2021 is applied. These discrepancies highlight the importance of applying precise selection methods to extract the most relevant studies. To streamline the process of locating strong contributions, the AI-powered tool Elicit9is used. Elicit supports the literature review by offering summarised content and DOIs for suggested papers. While it helps reduce the manual workload during the initial phase, every suggested paper in this review is manually reviewed to ensure its relevance. This ensures that the final list excludes any unrelated or off-topic material. After the initial filtering, a manual review is performed to confirm the relevance and quality of each paper. Abstracts are first assessed to judge suitability. If the abstract lacks clarity or depth, a further examination of the full text is conducted. Abstracts are closely read, and when necessary, the full text is reviewed using the following exclusion and inclusion criteria: Inclusion Criteria: Studies are included if they offer meaningful theoretical or empirical insights related to NLP, LLMs, and their application in software requirements. This includes topics like specification, formal logic, verification, and formal methods. Exclusion Criteria: Papers are excluded if they show in-sufficient relevance to the intersection of NLP/LLMs and software requirements, or if their abstracts or full texts lack sufficient detail. Non-peer-reviewed materials, duplicates, and items suggested by Elicit but deemed irrelevant after manual review are also removed. Figure 2 represents a tree-like structure of the literature review related to LLM-Based Specification and Verification. F I G U R E 2 LLM-Based Verification and Specification Literature Overview 2.2 Formalising Requirements through LLMs This section provides an integrated overview of the literature surveyed, supported by a set of structured tables that summarise and categorise the body of work examined. Table 5 organises the surveyed papers according to the methodological lens through which they approach specification generation, verification, and tool-assisted reasoning, enabling readers to quickly identify clusters of research such as prompt-only approaches, verifier-in-the-loop workflows, fine-tuned models, neuro-symbolic pipelines, and dataset-driven contributions. A more detailed breakdown is provided in Table 6, which extends the classification by including for each reference the specific tool, framework, or technique under consideration as well as a concise summary of its contribution, evaluation method, and reported outcomes. This granular presentation illustrates how diverse approaches–from NL-to-LTL translation and class-invariant inference to dataset construction and IDE-integrated verification 6BEG ET AL. assistance–contribute to the broader landscape of automation in software verification. Later, we used the iterative approach to extend the state-of-the-art, while conducting our experiments. Table 7 compiles the most recent and state-of-the-art developments, offering extended descriptions of works that combine LLM-based inference with symbolic reasoning, retrieval-augmented pipelines, benchmark creation, interactive proof systems, agentic frameworks, and domain-specific verification. 2.2.1 LLM-Assisted Verification and Specification Tools PALM is introduced in10, which is a generate-then-repair framework that combines large language models with symbolic reasoning to improve formal proof generation in Coq. Through analysis of 520 proof generation errors made by GPT-3.5, Minghai et al. identify that LLMs often capture the high-level proof structure but fail in low-level details, motivating PALM’s iterative repair mechanism. Evaluated on a dataset of over 10,000 theorems, PALM achieves 76.6%-180.4% higher success rates and proves 1,270 additional theorems beyond existing methods, demonstrating strong performance and generalizability across multiple LLMs. The paper11 introduces AutoSpec, an automated framework for synthesizing formal specifications that enables end-to-end program verification without extensive manual effort. It extends beyond prior approaches that are limited to narrow domains, supporting complex program structures involving arrays, pointers, nested loops, and function calls. AutoSpec combines static analysis and program verification in an iterative synthesis loop that incrementally refines and validates candidate specifications, ensuring satisfiability and proof adequacy throughout the process. Empirical evaluation demonstrates its strong performance, successfully verifying 79% of benchmark programs–a 1.592x improvement over existing methods–and further confirming its applicability through verification of the real-world X509-parser project. The paper12 proposes using LLMs, like GPT-3.5, to verify code by analysing requirements and explaining whether they are met. The work13 provides verification and refinement of natural language explanations by making LLMs and theorem provers work together. A neuro-symbolic framework i.e. Explanation-Refiner is represented. LLMs and theorem provers are integrated together to formalise explanatory sentences. The theorem prover then provides the guarantee of validated sentence explanations. Theorem prover also provides feedback for further improvements in NLI (Natural Language Inference) model. Error correction mechanisms can also be deployed by using the tool Explanation-Refiner. Consequently, it automatically enhances the quality of explanations of variable complexity. The work14 evaluated GPT-4o’s ability to generate specifications for C programs that can be verified using VeriFast, a static verifier based on separation logic. Their experiments, which use different user inputs and prompting techniques, show that while GPT-4o’s specifications maintain functional behaviour, they often fail verification and include redundancies when verifiable. The paper15 introduced OntoChat, a conversational agent that integrates large language models to assist users throughout the Ontology Requirements Engineering (ORE) process. It addresses the limitations of traditional, manual ORE methods by exploring how LLMs can automate and enhance tasks such as requirements elicitation, documentation, and validation.15 presented preliminary findings from the first year of research, demonstrating the potential of LLM-driven interaction to make ontology engineering more efficient, consistent, and collaborative. The paper16 presents HILBERT, an integrated agentic framework that unites informal mathematical reasoning with formal verification to advance automated theorem proving. The system coordinates four synergistic components–an informal reasoning model for high-level mathematical insight, a Lean 4–optimized prover, a formal verifier, and a semantic theorem retriever–to collaboratively construct, verify, and refine formal proofs. When the prover encounters unsolved problems, HILBERT applies recursive decomposition to partition them into smaller subgoals, which are then resolved using either the prover or the informal reasoning agent. The framework incorporates verifier-guided feedback loops to iteratively correct and strengthen incomplete or erroneous proofs, ensuring semantic consistency across the reasoning process. Experimental evaluation demonstrates that HILBERT achieves state-of-the-art performance, with 99.2% accuracy on miniF2F—surpassing the best existing method by 6.6 percentage points–and solving 462 out of 660 problems (70.0%) on PutnamBench, outperforming proprietary systems such as SeedProver (50.4%) and achieving a 422% improvement over the best publicly available baseline. Collectively, these results establish HILBERT as a major step forward in bridging the divide between informal mathematical reasoning and fully verified formal proof synthesis. 2.2.2 Frameworks for Specification Synthesis The work17 details about nl2spec, a framework that leverages LLMs to generate formal specifications from natural language, addressing the challenge of ambiguity in system requirements. Users can iteratively refine translations, making formalization Traceable and Verifiable Software Requirements: A Synthesis of AI-Enabled Formal Methods 7 easier. The work17 provides an open-source implementation with a web-based interface. An automatic synthesis of software specifications is provided through LLMs in18. Work18 proposed SpecSyn framework that uses an advanced language model to automatically generate software specifications from natural language text. It treats specification generation as a sequenceto-sequence learning task and outperforms previous tools by 21% in accuracy, extracting specifications from both single and multiple sentences. The paper19 introduces LEMUR, a rigorous framework that integrates automated reasoning with structured synthesis to improve loop invariant generation and program verification. Unlike prior learning-based approaches such as Code2Inv, which rely solely on reinforcement learning, LEMUR establishes a formal calculus that unifies symbolic reasoning and guided invariant inference under a provably sound framework. Evaluated on the Code2Inv benchmark set of 133 C programs, LEMUR employs the ESBMC k-induction verifier to validate synthesized invariants and significantly outperforms both ESBMC alone and Code2Inv. Specifically, LEMUR(GPT-4) solves 107 benchmarks within a 10-minute timeout, compared to only 68 by ESBMC and fewer by Code2Inv under a longer one-hour limit. The framework’s adaptive generation strategy allows it to converge to correct invariants typically within four iterations, though complex cases may require more. Moreover, comparative evaluation with LEMUR(GPT-3.5) reveals that stronger symbolic reasoning oracles lead to both faster convergence and higher verification success rates, highlighting the importance of well-structured reasoning integration rather than heuristic generation. Extending the evaluation to the SV-COMP 2023 benchmark suite,19 demonstrates LEMUR’s robustness on challenging verification tasks that traditional tools cannot resolve. On 47 benchmarks unsolved by ESBMC and UAutomizer, LEMUR(GPT-4) successfully verifies 25 instances, including programs with multiple nested loops, achieving dramatic performance gains where baseline verifiers each solved only one. The results reveal LEMUR’s ability to infer non-trivial invariants–such as modular arithmetic relationships and disjunctive conditions—not explicitly represented in source code, surpassing the expressiveness of predicate-abstraction-based techniques. The framework’s iterative refinement mechanism, guided by verifier feedback, ensures that candidate invariants remain both semantically sound and provably sufficient. Beyond empirical achievements, the paper outlines a clear path for future research, including specialization to back-end verifiers, adaptation to functional languages, and development of domain-specific prompting languages for complex logical formula synthesis. Together, these contributions establish LEMUR as a comprehensive and extensible foundation for formal verification through structured invariant synthesis, setting new standards in precision, scalability, and theoretical grounding for automated reasoning frameworks. The paper20 introduced Req2Spec, an NLP-based tool that analyses natural language requirements to create formal specifications for HANFOR”, a large-scale requirements and test generation tool. Tested on 222 automotive software requirements at BOSCH, it correctly formalized 71% of them. The work21 represents a novel framework named SpecGen to generate specifications through LLMs. Two phases are applied. First phase is about having prompts in conversational style. Second phase is deployed where correct specifications are not generated. Here, four mutation operators are applied to ensure the correctness of the generated specifications. Two benchmarks i.e. SV-COMP and SpecGen are used. Verifiable specifications are generated successfully for 279 out of 384 programs, making21 a viable approach. The paper22 introduces RvLLM, a runtime verification framework that leverages domain-specific knowledge encoded in a custom specification language (ESL) to systematically detect and correct erroneous outputs. RvLLM operates in a two-stage process of interpretation and reasoning, where context-driven interpretations guide the identification of inconsistencies, and iterative follow-up queries ensure output consistency. The framework was evaluated on three representative tasks–violation detection against the Singapore Rapid Transit Systems Act, numerical comparison, and inequality solving–across multiple LLMs including Qwen (max, plus, turbo, 2.5 variants), GPT-4.1 (mini, nano), Gemini 2.0 Flash (Lite), and DeepSeek-V322. In violation detection, RvLLM improved true positive rates substantially, for instance raising Qwen max from 56.2% to 86.1% and GPT-4.1 from 57.7% to 81.1%, while maintaining or slightly adjusting true negative rates. On numerical comparison tasks, LLMs guided by RvLLM consistently produced correct and inconclusive results, with Qwen 2.5 (32B) achieving 98 correct and 2 inconclusive outputs within 4.98 seconds, demonstrating considerable gains over baseline performance. In inequality solving involving factorization, interval analysis, and endpoint checking, RvLLM enabled higher true positive rates, reaching 50% for Qwen 2.5 (32B) on factorization tasks, showcasing its ability to enforce domain-specific constraints effectively. 23 presents SpecVerify, a framework that integrates large language models with formal verification tools to automatically derive and verify properties from natural language requirements. By combining Claude 3.5 Sonnet with the ESBMC verifier, it achieves verification accuracy comparable to NASA’s CoCoSim while reducing false positives and extending assertion expressiveness beyond traditional logics. The paper24 presents a structured approach for automatically synthesizing runtime verification monitors directly from natural language specifications. The method operates in staged transformations–first translating informal requirements into propositional past-time LTL formulas, and then generating corresponding runtime monitors 8BEG ET AL. based on these formal representations. The process incorporates self-validation steps within each synthesis stage, allowing the system to iteratively refine outputs and substantially improve the correctness of the generated monitors. The paper25 investigates an integrated approach for automatically discovering inductive loop invariants, a long-standing challenge in formal verification. Using a curated benchmark comprising 1,025 C programs with diverse loop structures, the study evaluates GPT-4, GPT-3.5, and Code Llama in conjunction with Frama-C’s WP tool and SMT solvers to assess the soundness of generated invariants. The proposed method combines symbolic reasoning with data-driven synthesis, where candidate invariants are generated and formally validated through automated proof obligations. 2.2.3 Domain-Specific and Security-Focused Applications AssertLLM tool is presented in26. The tool generates assertions to do hardware verification from design specifications, exploiting three customised LLMs. It is done in three phases, first understanding specifications, mapping signal definitions and generating assertions. The results show that AssertLLM produced 89% correct assertions with accurate syntax and function. The work27 reports on formal verification of NASA’s Node Control Software natural language specifications. The software is deployed at International Space Station. Errors found in the natural language requirements are reported by the authors with a commentary on lessons learnt. SpecLLM28 explores the space of generating and reviewing VLSI design specifications with LLMs. The utility of LLMs is explored with the two stages i.e. (1) generation of architecture specifications from scratch and from register transfer logic (RTL) code; and (2) reviewing these generated specifications. In29, the potential and power of LLMs is exploited for smart grid requirement specifications improvement. Here, the performance of GPT-4o and Claude 3.5 Sonnet is analysed through f1-scores, achieving in range of 79% - 94%. The research presented in30 introduces SV-LLM, a multi-agent large language model system purpose-built for automating security verification of complex system-on-chip (SoC) designs. The framework integrates domain-specialized agents that coordinate tasks such as security asset identification, threat modeling, property generation, vulnerability detection, and simulation-based bug validation. Each agent operates using distinct learning paradigms–fine-tuning, in-context learning, and retrieval-augmented generation—to generate precise, verifiable security specifications from design data and documentation. This agentic architecture directly targets SoC-level verification challenges by embedding reasoning capabilities tailored to register-transfer-level (RTL) semantics and design constraints. Experimental evaluations in30 demonstrate substantial gains in RTL security analysis accuracy and efficiency. The fine-tuned Security Vulnerability Detection Agent, based on Mistral-7B-Instruct, achieves 84.8% accuracy–an improvement of 42.3 percentage points over its non-fine-tuned baseline—while remaining transparent and resource-efficient compared to closed-source models. The Bug Validation Agent attains up to 89% validated testbench generation across diverse RTL designs, outperforming zero-shot prompting methods by more than fourfold. These results confirm that30 delivers a practical and high-performing framework for scalable, explainable, and domain-adapted SoC security verification. 2.2.4 Safety-Critical and Prover-Integrated Applications The work31 introduced LeanDojo, an open-source toolkit that enables programmatic interaction with Lean theorem prover. Using LeanDojo’s extracted data,31 developed ReProver, a retrieval-augmented LLM-based prover. Thor32 is a framework developed to integrate language models with theorem provers. It improved the accuracy from 39% to 57% using the PISA dataset and also outperformed previous works on the MiniF2F dataset. The paper33 explores integrating Co-pilot with formal methods. The integration of Copilot and formal methods is proposed through development of IDE containing language servers. Granberry et al.8explored combining LLMs with symbolic analysis to generate specifications for C programs. They enhanced LLM prompts using outputs from PathCrawler and EVA to produce ACSL annotations. 34 investigates the feasibility of applying formal software verification to LLM-generated code using the SPARK framework for Ada.34 introduced Marmaragan, a tool that employs an LLM to automatically generate SPARK annotations for existing programs, thereby enabling their formal verification. Evaluated on a curated SPARK benchmark with selectively removed annotations, Marmaragan powered by GPT-4o achieves 50.7% correctness in annotation generation. The study35 explores the use of Generative AI for the automatic synthesis of code contracts–specifically preand postconditions–for Java programs without relying on any auxiliary artifacts. The authors fine-tuned CodeT5 and CodeT5+ models on a newly curated dataset of over 14,000 Traceable and Verifiable Software Requirements: A Synthesis of AI-Enabled Formal Methods 9 Java methods annotated with Java Modeling Language (JML) specifications, enabling the models to learn precise contract generation. Their evaluation on unseen software projects demonstrated that over 95% of the generated contracts were syntactically valid and exhibited strong semantic accuracy and completeness, underscoring the potential of LLMs to advance automated software verification and Design-by-Contract methodologies. The work by36 presents a compiler that translates higher-order logic meaning representations, derived from Java method-level comments, into formal Java Modeling Language (JML) specifications. This translation bridges natural-language-based semantic representations and formal verification by resolving predicate ambiguities and aligning them with first-order logic constructs. Evaluation on Java API benchmarks demonstrates high accuracy, with 94% correct JML generation and 97% of those verifiable using an automated theorem prover. In37, symbolic NLP and ChatGPT performance is compared while generating correct formal contracts written in the Java Modelling Language (JML) which have been extracted from natural language specifications. The paper38 reports the translation between NL and Linear Temporal Logic (LTL) formulas through the use of LLMs. Dynamic prompt generation and human interaction with LLMs are amalgamated to deal with the mentioned challenges. Unstructured natural language requirements are converted to NL-LTL pairs. The approach achieved up to 94.4% accuracy on publicly available datasets with 36 and 255,000 NL-LTL pairs. The primitive work39 described automatic translation from natural language sentences to temporal logic, in order to deploy formal verification of the requirements. 2.2.5 Hybrid Symbolic-LLM Methodologies SAT-LLM, a unique framework to remove conflicting requirements is represented in40. It integrated Satisfiability Modulo Theories (SMT) solvers with LLMs. SAT-LLM performed better than ChatGPT alone, identifying 80% of conflicts with a Precision of 1.00, Recall of 0.83, and an F1 score of 0.91.41 outlines key research directions for the stages of software requirement engineering, conducts a SWOT analysis, and share findings from an initial evaluation. The purpose of Dafny is to automate proofs by outsourcing them to an SMT solver.7presented a framework named Laurel to generate Dafny assertions using LLMs. Laurel was able to generate over 50% of the required helper assertions.42 used input of error messages, variable names, procedure documentation and user questions. They discussed available literature for generating assertions by synthesising sentences in testing phase. Reporting about DafnyBench43, Chloe et al. evaluated the capability of GPT-4 and Claude 3 to automatically generate sufficient hints, enabling the Dafny formal verification engine to successfully verify over 750 programs comprising approximately 53,000 lines of code. The most effective combination of model and prompting strategy achieved a 68% verification success rate, with further analysis showing that this rate improves through iterative retries using error feedback but declines as program size and hint complexity increase. The paper44 introduced a model-based language (Requirements Specification Language - RSL). The framework functionality is integrated as development platform named ReDSeeDS. A similar work is reported in45 which describes the ARSENAL framework and methodology designed to perform automatic requirements specification extraction from natural language. An interesting work is presented in46. It includes generation of natural language from business process models. The generated natural language is found complete and more understandable. In primitive work of 199647, software requirements were expressed in a limited set of natural language referred to as controlled natural language. The primitive work in the domain is about RML48. RML bundled with features of writing requirements, which are based on conceptual model. 2.2.6 Advanced Prompt Engineering In this sub-section, we outline prospective directions informed by the literature review. Much of the literature in this review employed queries containing a problem description and some instructions to achieve a desired outcome. Such querying of LLMs without training or examples of the current task is typically referred as zero-shot prompting and shows excellent performance on many tasks49. Surprisingly, they also showed that the performance of LLM on some challenging problems can be improved by encouraging the LLM to reason using intermediate steps through a simple addition to problem prompts (Lets think step by step). Beyond this approach is one-shot prompting that includes an example of a solved problem to guide the LLM into generating the desired output50. This can be extended to few-shot prompting where a number of differing examples guide the LLM. But improved results are not assured as some studies e.g.51 show that zero-shot can outperform the few-shot case52.53 reviewed the evolution of prompt engineering in LLMs, including discussions on self-consistency and multimodal prompt learning. It also reviewed the literature related to adversarial attacks and evaluation strategies for ensuring robust AI interactions. 16 BEG ET AL. satisfies the intended properties. Typically, this approach involves annotating code with preconditions, postconditions, and invariants, which are then translated into verification conditions (VCs). SMT solvers and theorem provers are used to automatically or semi-automatically discharge these conditions, providing strong guarantees of correctness when proofs succeed. This methodology is particularly effective for critical software domains, such as safety-critical embedded systems, where runtime errors or logical flaws can have severe consequences. Recent developments in deductive verification have focused on improving automation, scalability, and solver integration. Modern SMT solvers, such as Z3, Alt-Ergo, CVC4, and CVC5, enable efficient reasoning over arithmetic, pointers, arrays, and quantified expressions, which are common in real-world programs. Toolchains like Frama-C leverage these solvers to translate high-level specifications into proof obligations, allowing verification engineers to focus on specifying program intent rather than manual proof construction. Additionally, advances in solver strategies, heuristics, and preprocessing techniques have reduced the incidence of timeouts and improved success rates on complex verification conditions, making deductive verification more practical for larger codebases. Together, these innovations are pushing deductive verification toward a more automated, reliable, and widely applicable paradigm in formal software verification. 3 METHODOLOGY OF INITIAL EXPERIMENTS This section outlines the methodology used to conduct our initial experiments aimed at assessing the behavior of automated test-generation and verification tools under controlled conditions. The approach is grounded in a representative example provided by PathCrawler and guided by prompt templates adapted from prior work. Our objective here is to establish a clear and reproducible experimental setup that illustrates how the tools respond to structured inputs before extending the evaluation to larger and more diverse datasets. The Frama-C platform is configured and executed within a Linux environment running on Windows Subsystem for Linux (WSL 2), hosted on a Windows 11 system equipped with an Intel Core Ultra 5 125U processor (3.60 GHz) and 32 GB of RAM (31.5 GB usable) operating under a 64-bit architecture.The procedures detailed in the following subsections define the basis for the empirical analyses that appear later in the paper. 3.1 Experimental Re-Simulation and Verification of TriType.c We re-simulated the methodology presented in8by applying it to the TriType.c program, selected from the PathCrawler tool in the Frama-C ecosystem. The workflow integrated Large Language Models (LLMs) with symbolic outputs from PathCrawler and EVA to automatically generate ACSL specifications. Input C Program PathCrawler Analysis Symbolic Paths + I/O Examples Prompt LLM for ACSL Specs Annotated C Code (with ACSL) Frama-C WP + SMT Solvers Verification Goals + Outcomes FIGURE 3 Methodology of the initial experiments following the approach of8, combining LLM with symbolic analysis tools in the Frama-C ecosystem. The workflow integrates path-based I/O examples and verification outputs to guide the generation of context-aware ACSL specifications. PathCrawler provided path-based input/output examples that guided the LLM toward producing semantically accurate annotations. Table 1 shows the tool’s output. Our ongoing plan includes experiments with simple and complex programs featuring diverse control structures, enabling evaluation of the methodology’s generality. The function under test is shown below. /*Should return the type of the triangle which has sides of these lengths. 3 = not a triangle 2 = equilateral triangle 1 = isoceles triangle 0 = other triangle */ Traceable and Verifiable Software Requirements: A Synthesis of AI-Enabled Formal Methods 17 int Tritype(double i, double j, double k){ int trityp = 0; if (i < 0.0 || j < 0.0 || k < 0.0) // line 10 return 3; if(i+j<=k||j+k<=i||k+i<=j)//line12 return 3; if (i == j) trityp = trityp + 1; // line 14 if (i == k) trityp = trityp + 1; // line 15 if (j == k) trityp = trityp + 1; // line 16 if (trityp >= 2) // line 17 trityp = 2; return trityp; } T A B L E 1 Output of the Pathcrawler for TriType Example Test Case i j k Return Value Path Path Predicate 1 -196 364 18 3 tritype.c:+10 i<0 2 260 364 18 3 tritype.c:-10:-10b:-10c:-12:-12b:+12c i>=0; j>=0; k>=0; (j+i)>k; (k+j)>i; (i+k)=<j 3 197 940 1087 0 tritype.c:-10:-10b:-10c:-12:-12b:-12c:-14:- 15:-16:-17 i>=0; j>=0; k>=0; (j+i)>k; (k+j)>i; (i+k)>j; i<>j; i<>k; j<>k 4 887 986 986 1 tritype.c:-10:-10b:-10c:-12:-12b:-12c:-14:- 15:+16:-17 i>=0; j>=0; k>=0; (j+i)>k; (k+j)>i; (i+k)>j; i<>j; i<>k; j=k 5 952 990 952 1 tritype.c:-10:-10b:-10c:-12:-12b:-12c:- 14:+15:-16:-17 i>=0; j>=0; k>=0; (j+i)>k; (k+j)>i; (i+k)>j; i<>j; i=k; j<>k 6 108 108 177 1 tritype.c:-10:-10b:-10c:-12:-12b:-12c:+14:- 15:-16:-17 i>=0; j>=0; k>=0; (j+i)>k; (k+j)>i; (i+k)>j; i=j; i<>k; j<>k 7 646 646 646 2 tritype.c:-10:-10b:-10c:-12:-12b:- 12c:+14:+15:+16:+17 i>=0; j>=0; k>=0; (j+i)>k; (k+j)>i; (i+k)>j; i=j; i=k 8 232 67 158 3 tritype.c:-10:-10b:-10c:-12:+12b i>=0; j>=0; k>=0; (j+i)>k; (k+j)=<i 9 96 457 1530 3 tritype.c:-10:-10b:-10c:+12 i>=0; j>=0; k>=0; (j+i)=<k 10 260 364 -886 3 tritype.c:-10:-10b:+10c i>=0; j>=0; k<0 11 260 -533 18 3 tritype.c:-10:+10b i>=0; j<0 PathCrawler achieved 100% branch coverage while generating 11 test cases, all marked “unknown.” This outcome suggests that execution paths were traversed correctly, yet verdict classification failed due to incomplete postconditions or ambiguous return-value specifications. Of 19 identified paths, 11 were feasible and eight infeasible. The coverage demonstrates effective instrumentation, though the absence of successful verdicts highlights the need for refined oracles and explicit assertions. The dataset nevertheless provides rich insights into path feasibility and constraint diversity across valid, invalid, and boundary inputs. Reproducing the baseline from8revealed that Frama-C’s analysis, using Alt-Ergo, Z3, CVC4, and CVC5, generated only two trivial verification goals–termination and unreachability–both successfully proven. This confirms structural soundness and absence of infinite loops or dead code but exposes the limits of minimal ACSL specification. The lack of user-defined pre/postconditions and missing assigns clauses restricted verification to syntactic validation, leaving functional correctness untested. While no runtime errors were reported, the omission of Run-Time Error (RTE) guards means potential overflows or edge-case failures remain unchecked. Overall, all solvers performed equivalently under these basic conditions, verifying the function’s structural integrity but offering little semantic assurance. The PathCrawler-augmented version (pp. 21-22,8) introduced detailed ACSL annotations, generating 20 verification goals– 18 derived from explicit pre/postconditions plus the standard structural checks. This enriched specification significantly increased solver complexity. While all provers confirmed termination and reachability, only Alt-Ergo and CVC5 proved 15 goals, whereas Z3 and CVC4 proved 13 each. Unverified goals predominantly involved disjunction-heavy triangle classification logic and arithmetic inequalities. These failures stem from the difficulty solvers face in reasoning over conditional branches with subtle numeric constraints. The results underscore that symbolic-annotation synergy improves verification depth but stresses solver capacity. Integrating stronger lemma decomposition or intermediate assertions may enhance success rates in future iterations. 18 BEG ET AL. T A B L E 2 Prover Results Comparison (with Baseline and Pathcrawler Output Augmented Prompt) (a) Baseline Example1-Tritype.c Prover Total Goals Proved Notes Alt-Ergo 2 2 All default goals proved Z3 2 2 All default goals proved CVC4 2 2 All default goals proved CVC5 2 2 All default goals proved (b) Pathcrawler Augmented Example1-Tritype.c Prover Total Goals Proved Failed Type Failed Count Z3 20 13 Timeout 7 Alt-Ergo 20 15 Timeout 5 CVC4 20 13 Unknown 7 CVC5 20 15 Timeout 5 3.2 Empirical Evaluation on Frama-C iFM2024 tutorial program set To evaluate the effectiveness of different SMT solvers in deductive verification, four provers–Z3, Alt-Ergo, CVC4, and CVC5– were tested on 36 representative C programs from the Frama-C tutorial suite. Each example includes arithmetic, pointer, and array manipulation constructs verified using the WP plugin. Table 3 presents a sample subset illustrating the comparative proof coverage and goal completion across these provers. T A B L E 3 Sample verification outcomes across four SMT provers (subset of 36 code snippets). C File Goals Z3 Alt-Ergo CVC4 CVC5 Timeouts Timeout % Success Rate % 01-abs-2.c 6 6/6 6/6 6/6 6/6 0 0.0 100.0 02-max-1.c 7 5/7 5/7 5/7 5/7 2 28.6 71.4 03-max_ptr-1.c 8 6/8 6/8 6/8 6/8 2 25.0 75.0 04-swap-0.c 8 4/8 4/8 4/8 4/8 4 50.0 50.0 06-max_abs-3.c 13 13/13 13/13 13/13 13/13 0 0.0 100.0 All four SMT provers–Z3, Alt-Ergo, CVC4, and CVC5–exhibited comparable verification performance across the tested benchmarks, consistently solving most arithmetic, pointer, and array-related goals. Here, we are including table for reference, reporting output of Z3. Timeout rates were generally low, and differences in success rates were minimal, indicating that each solver can reliably handle typical verification conditions. While minor variations appeared on more complex or nested constructs, no prover showed a clear advantage, suggesting that any of these tools can serve effectively in automated verification workflows within the Frama-C ecosystem. The execution times taken by each prover is given in figure 4. F I G U R E 4 Graph of Execution Times of Alt-Ergo, Z3, CVC4 and CVC5 Traceable and Verifiable Software Requirements: A Synthesis of AI-Enabled Formal Methods 19 4 EMPIRICAL EVALUATION OF FRAMA-C EVA AND RTE FOR ACSL ANNOTATION AND STATIC VERIFICATION In this part of the study, we present a comprehensive empirical evaluation of the Frama-C EVA (Evolved Value Analysis) and RTE (Runtime Error) plugins, which support the creation and verification of formal specifications for C programs. The goal of this evaluation is to examine how these tools contribute to the automation of specification generation through ACSL (ANSI/ISO C Specification Language) annotations and to assess their practical capabilities when applied to a curated benchmark of real C code. The hardware used kept same as specified in paragraph 1, Section 3. A benchmark consisting of fifty C programs, each exhibiting distinct structural complexity, was adopted without modification from a publicly available GitHub repository ‡‡ used for prompt engineering reported in8. Following the design of the original work, these programs were grouped into three predefined categories: (i) correct implementations, (ii) implementations exhibiting obvious differences between function variants, and (iii) implementations with subtle differences in their function bodies. Each of the fifty base programs was analyzed across these three categories, yielding a total of 150 evaluated instances. This multi-category organization enables the systematic study of tool behavior across a controlled spectrum of semantic and syntactic variations. Within this setup, the EVA plugin performed sound abstract interpretation to analyze each program’s control flow and data dependencies, identifying potential runtime anomalies and verifying functional behavior. In parallel, the RTE plugin automatically generated ACSL annotations to express inferred preconditions, postconditions, and invariants that capture candidate formal contracts. All outputs–EVA logs, inferred specifications, and analysis results–were collected and organized for subsequent tabular presentation and comparative study. This empirical analysis is motivated by the broader goal of improving automation in formal methods workflows. Reliable software systems, especially those deployed in safety-critical or high-assurance domains, require early defect detection and strong guarantees of correctness. While formal methods provide these guarantees, their adoption remains limited due to the substantial effort required to create, interpret, and maintain mathematically precise specifications. Developers are typically expected to not only implement functionality but also encode behavioral intent in specification languages interpretable by automated verifiers. This task demands specialized expertise and significant additional development time, representing a key barrier to widespread industrial uptake. Tools such as Frama-C, and specifically the EVA and RTE plugins, are designed to mitigate this challenge by bridging the gap between implementation and formal reasoning. The findings from this evaluation are contextualized within a broader methodological framework that integrates benchmarkdriven analysis with dataset-based validation. In addition to the empirical evaluation of Frama-C plugins, several datasets were incorporated to assess the consistency and scalability of specification generation and verification processes. Evaluation Metrics. Evaluation across all datasets employed a consistent set of quantitative and qualitative metrics. These included specification accuracy (through manual review and ground-truth comparison), verification success rate (based on Frama-C WP outcomes), model completeness (coverage of preconditions, postconditions, and frame conditions), and context sensitivity (measured through performance changes under varying prompt scopes). Solver coverage was quantified in terms of goals proven per solver. All datasets, experimental prompts, synthesized specifications, and verification outcomes have been released in an open-access GitHub repository to facilitate transparency, reproducibility, and collaborative exploration. 4.1 EVA Analysis and Results The EVA plugin’s analysis evaluates the extent to which Frama-C can detect and classify potential runtime issues through abstract interpretation. A consolidated overview of the EVA results across the three categories–Correct, Obvious, and Subtle–is presented in Table 4. Figure 5(a) summarises the total number of alarms produced per program category. Correct programs yield the fewest alarms overall, typically limited to minor boundary or division-by-zero checks. Programs with obvious functional differences show a moderate increase in alarm count, as EVA identifies deviations in data flow and control structures that could lead to runtime faults. Subtle-difference programs, by contrast, exhibit the highest number of alarms, reflecting EVA’s sensitivity to small but semantically significant variations that introduce uncertain execution paths. This trend illustrates EVA’s precision in differentiating between benign and critical deviations in program behavior. ‡‡ https://github.com/ggranberry/intent_dataset 20 BEG ET AL. T A B L E 4 EVA Category-wise Result Summary Category Files Mean Coverage (%) Median Coverage (%) Mean Alarms Median Alarms Success Rate Correct 52 75.00 96.0 38.66 3.0 0.308 Obvious 60 77.73 97.0 0.68 0.0 0.650 Subtle 53 58.84 88.0 7.59 3.0 0.623 The nature of detected alarms is illustrated in Figure 5(b), which categorizes them by type, including uninitialized memory access, division by zero, invalid pointer dereference, and out-of-bounds array indexing. Across all categories, pointer-related alarms dominate–indicating EVA’s conservative bias toward ensuring memory safety. Division and bounds-related alarms occur less frequently but tend to cluster in subtle-difference programs, where small logical shifts affect variable ranges. The distribution highlights EVA’s layered reasoning approach: it prioritizes memory safety while maintaining comprehensive coverage of arithmetic and control-flow conditions. Figure 5(c) presents the statement coverage achieved by EVA, representing the proportion of executable statements analyzed and instrumented with abstract value information. Coverage remains highest for correct programs–often exceeding 90%–thanks to well-defined data flow and stable control paths. Coverage decreases for programs with obvious and subtle differences, where undefined behaviors, pointer aliasing, or non-deterministic inputs limit full propagation of abstract domains. This reduction reveals the inherent trade-off between precision and scalability in static value analysis, particularly when handling complex pointer manipulations or dynamic structures. Finally, Figure 5(d) aggregates the success rate of EVA’s analysis, indicating the proportion of alarms successfully discharged as non-critical or safe after propagation and refinement. Correct programs achieved the highest success rates, confirming that EVA can confidently validate the absence of runtime errors. Obvious-difference cases retained moderate success rates, while subtle-difference programs displayed lower rates due to compounded uncertainties and partially explored states. Importantly, no category resulted in complete analysis failure, demonstrating EVA’s robustness in handling diverse program structures and maintaining soundness under all evaluation conditions. In summary, this section presented a detailed empirical investigation of Frama-C’s EVA plugin as an automated static analyzer for detecting potential runtime errors and assessing program reliability. By evaluating a benchmark of fifty C programs across three categories, the study demonstrated EVA’s effectiveness in identifying subtle behavioral discrepancies and ensuring soundness under diverse control-flow conditions. The results confirm EVA’s practical role as a foundational tool for static verification, complementing later proof-oriented analyses. They also highlight current challenges related to analysis coverage and precision, motivating further work on domain refinement and hybrid symbolic approaches to improve the scalability and expressiveness of Frama-C based analyses. 4.2 RTE Analysis and Results The Runtime Error (RTE) plugin in Frama-C operates as an automated assertion generator and runtime property checker, complementing EVA’s abstract interpretation by directly targeting sources of undefined or unsafe behavior such as overflows, invalid memory access, and division by zero. Whereas EVA reconstructs abstract value domains, RTE instruments the program with concrete checks and passes the generated proof obligations to SMT solvers. This study presents a quantitative evaluation of RTE across the three benchmark families correct,obvious-difference, and subtle-difference focusing on solver stability, proof coverage, and verification scalability. For the correct program category (Figure 6), proof success rates for Alt-Ergo,Z3,CVC4, and CVC5 approach full coverage, confirming RTEs strong alignment with provable safety properties. Solver outcome heatmaps are uniformly saturated, reflecting consistent convergence, and timeout counts are negligible. Overall, these results demonstrate stable and efficient verification for programs without functional differences. For the obvious-difference category (Figure 7), proof success rates are slightly lower, and solver outcome heatmaps show localized patches of failure at array-bound or nested arithmetic checks. Timeout counts increase modestly due to denser assertion sets. These observations indicate a moderate increase in verification complexity, though partial proofs remain common across solvers. For the subtle-difference category (Figure 8), proof success rates diverge significantly across solvers, with Alt-Ergo generally performing better on arithmetic-heavy proofs. Solver outcome heatmaps appear fragmented, revealing clusters of challenging assertions. Timeout counts increase substantially, reflecting higher semantic coupling among assertions. Despite Traceable and Verifiable Software Requirements: A Synthesis of AI-Enabled Formal Methods 21 (a) Alarm types by category (b) Total alarms by category (c) Statement coverage by category (d) Analysis success rate by category FIGURE 5 EVA analysis results across the three program categories: (a) distribution of alarm types, (b) total alarms detected, (c) statement coverage of analyzed code, and (d) overall success rate of EVA’s runtime error analysis. this, partial proofs are typically present, demonstrating that RTE-generated assertions remain valid and useful for downstream verification. Across all categories, verification cost under RTE is influenced more by assertion heterogeneity and semantic coupling than by program size, with proof-time dispersion increasing super-linearly with functional deviation. Solver heterogeneity highlights the value of multi-prover strategies, as each solver contributes unique strengths in arithmetic reasoning, quantifier handling, and pointer alias resolution. The consistently high success rates for correct programs confirm RTE as a dependable source of automatically generated runtime contracts, suitable as a foundation for deductive verification with WP. Overall, RTE proves effective both as a runtime-safety analyzer and as a benchmark for solver scalability in formal verification workflows. 4.3 PathCrawler Experiments and Progress PathCrawler is a Frama-C plugin designed for automatic generation of test cases based on path exploration of C programs. During the course of our research, several challenges emerged that required careful resolution in order to integrate PathCrawler into our formal verification workflow alongside EVA and RTE. Initial Barriers and Setup: The online version of PathCrawler proved unreliable, repeatedly failing during attempted executions. This reinforced the need for a local configuration to ensure stable and repeatable experimentation. The plugin was independently configured and compiled with Frama-C, resolving dependency and environment issues, particularly those related to ECLiPSe-CLP, the underlying constraint solver. Initial runs with example programs, including Swap and RunningSum, were partially successful, but outputs were inconsistent and incomplete. Compilation issues were addressed by updating PathCrawler to a version compatible with the latest ECLiPSe-CLP and recompiling the sources, which resulted in a functioning local installation. 22 BEG ET AL. (a) Std. Dev. of QED Times (b) Proof Success Rate (c) Solver Heatmap (d) Timeouts per Solver FIGURE 6 RTE runtime verification results for correct program category. Subfigures show (a) standard deviation of QED times, (b) proof success rate, (c) solver performance heatmap, and (d) solver timeouts. Tool Limitations: PathCrawler imposes several inherent restrictions on the programs it can handle. The current version cannot process input operations reading from the console or files (scanf,fscanf, etc.); floating-point types (float)–double is partially supported but computations involving trigonometric functions slow down constraint resolution significantly; explicit or implicit casts beyond integer-to-floating-point types, including pointer casts; assembly code embedded in functions; pointers to functions used as input parameters, or formal parameters which are themselves functions; recursive structures or recursive functions; void*pointers as function inputs; functions with variable-length argument lists; functions whose source code is unavailable, including standard library functions, which may prevent correct test case generation; and integer constants exceeding the representable range for the target type. These constraints necessitated careful preparation of the dataset and highlighted that programs successfully analyzed with EVA or RTE may not yield test cases with PathCrawler without modifications. Dataset Modification: To work around these restrictions, the dataset of C files was systematically modified. Interrupt signals generated during PathCrawler test case generation were traced to unhandled code constructs, and a Python script was developed to preprocess each C file. The script encapsulated the function under test together with a main function, suppressed unsupported operations, and ensured compatibility with PathCrawlers limitations. With these modifications, test case generation succeeded for a subset of the dataset. Initially, only four out of twenty files produced valid test cases without errors. Iterative refinement of the preprocessing script enabled successful generation for fifteen out of twenty files in the correct/basic subfolder. Path Coverage and Generator Options: One major bottleneck arose from PathCrawlers default coverage strategy. By default, it attempts to explore all possible paths, which frequently resulted in zero successful test cases. To address this, the OCaml wrapper functions were modified and a new -pc-max-paths N option was implemented, allowing the user to limit the number of explored paths. Despite this, the .pl scripts responsible for generating path exploration commands still enforced the "all paths" coverage mode. A practical workaround involved specifying the function body for analysis and disabling standard library translation, using the following command: frama-c -pc -wp -pc-branches-func "functionBody" -no-frama-c-stdlib -variadic-no-translation file.c > output_file.txt Traceable and Verifiable Software Requirements: A Synthesis of AI-Enabled Formal Methods 23 (a) Std. Dev. of QED Times (b) Proof Success Rate (c) Solver Heatmap (d) Timeouts per Solver FIGURE 7 RTE runtime verification results for obvious-difference program category. Subfigures show (a) standard deviation of QED times, (b) proof success rate, (c) solver performance heatmap, and (d) solver timeouts. This approach permitted selective path exploration and the generation of traces for functions that did not contain unsupported constructs such as pointers or external library calls (printf,memset). Manual editing of C files was sometimes required to ensure compatibility. Test Case Generation: After these adjustments, PathCrawler successfully generated test cases across multiple programs. For example, the binarySearch and tritype functions produced seven and ten test cases, respectively, when executed with: frama-c -pc -pc-drivers -lib-entry -main "quicksort" -no-frama-c-stdlib -variadic-no-translation quicksort.c The -pc-drivers option enabled automatic generation of test drivers, which was previously unavailable. Additionally, the -pc-iter-limit N option was tested to limit the number of iterations during test case generation, providing better control over execution time and resource usage. Successful generation was particularly observed for functions without external dependencies or complex pointer manipulations. Pathcrawler Output Log for QuickSort function: The PathCrawler (Frama-C) automatic test-generation session for the quicksort function completed normally and generated a total of eleven test cases intended to cover all feasible execution paths. The session explored 110 total execution paths or partial paths, out of which 11 were feasible and successfully associated with generated test cases, while the remaining 99 were classified as infeasible. The oracle used during execution was unable to determine correctness, and therefore each of the eleven test cases received the verdict unknown. No user assertions were violated, and the process finished within approximately one second of total execution time. Each generated test case is associated with a path prefix identifier and a corresponding symbolic execution trace through quicksort.c, expressed in PathCrawlers path-notation format (e.g., -11a,+23,-36b, etc.). These traces collectively represent the distinct feasible control-flow paths encountered during symbolic exploration. Test cases differ primarily in the structure and repetition of their pivot-comparison and recursive-call path segments, revealing how PathCrawler unfolds and prunes the quicksort recursion under varying symbolic constraints. All generated test cases exhibit the unknown verdict solely because the oracle for validating output correctness was not provided or was insufficient for classification. 24 BEG ET AL. (a) Std. Dev. of QED Times (b) Proof Success Rate (c) Solver Heatmap (d) Timeouts per Solver FIGURE 8 RTE runtime verification results for subtle-difference program category. Subfigures show (a) standard deviation of QED times, (b) proof success rate, (c) solver performance heatmap, and (d) solver timeouts. (a) Summary of PathCrawler Test-Case Generation Metric Value Total test cases generated 11 Verdict: success 0 Verdict: failure 0 Verdict: unknown 11 User-assertion violations 0 Total paths explored 110 Feasible paths covered 11 Infeasible paths detected 99 Test session duration 1 s Termination status normal Function under test quicksort Coverage criterion all feasible paths (b) Input and Output Data for TC_5 Input Values n3 arr[0] 0 arr[1] 0 arr[2] 0 Concrete Outputs arr[0] 0 arr[1] 0 arr[2] 0 Symbolic Outputs arr[0] 0 arr[1] 0 arr[2] 0 (c) Complete Execution Path for TC_5 -11a; -11b; -11c; +23; -28a; -28b; -28c; +35a; +35b; -36a; -36b; +38; +40a; +40b; +35a; +35b; -36a; -36b; +38; +40a; +40b; -35a; +49a; +49b; +56a; +56b; -62a; +23; -28a; -28b; -28c; +35a; +35b; -36a; -36b; +38; +40a; +40b; -35a; +49a; +49b; -56a; -62a; -23; (d) Path Predicate for TC_5 n> 0 ∧ n≤3∧ (n−1) < n∧ 0<(n−1) ∧ arr[0] ≤arr[(n−1)] ∧ 1<(n−1) ∧ arr[1] ≤arr[2] ∧ arr[0] ≤arr[1] F I G U R E 9 Combined results for Test Case TC_5: (a) summary, (b) I/O data, (c) execution path, (d) path predicate. Among the generated test cases, TC_5 is the only one for which a full test-case body is present in the log. For this case, PathCrawler produced an input array of size three with values 0, 0, 0 and input parameter n=3. The corresponding path predicate explicitly encodes ordering constraints that keep all array elements equal and ensure the chosen recursion branches remain feasible. The concrete and symbolic outputs coincide with the input array, which is consistent with the behavior of quicksort when processing identical elements. The complete execution path for TC_5 includes multiple nested quicksort invocations, exhibited by repeated +23 and -28a/-28b/-28c segments, faithfully reflecting the algorithmic structure encountered under these inputs. Observations and Bottlenecks: Despite these successes, several challenges remain. PathCrawlers handling of path coverage and default generator scripts necessitated manual intervention for reliable test case generation. Functions involving pointers, Traceable and Verifiable Software Requirements: A Synthesis of AI-Enabled Formal Methods 25 external library calls, or unsupported casts often required code adaptation. Additionally, fine-tuning the number of paths explored was crucial to avoid long execution times and incomplete outputs. Overall, these challenges underscore the importance of dataset preprocessing and careful configuration when integrating PathCrawler into a formal verification workflow. Ongoing work focuses on scaling PathCrawler experiments to larger datasets, integrating its outputs with analyses from EVA and RTE, and exploring the combination with AI-assisted testing tools such as Qwen and Ollama. The goal is to create a unified pipeline that leverages automated test generation, runtime property checking, and static analysis to improve coverage and reliability of software verification. 5 CHALLENGES AND FUTURE DIRECTIONS The attempt to position large language models (LLMs) within the practices of formal specification and verification raises philosophical questions about the nature of meaning, inference, and the limits of mechanised reasoning. At its core, formal verification demands a commitment to determinacy: every symbol must denote a precise concept, every statement must resolve to a truth value relative to a well-defined semantics, and every proof must be justified through inferential steps that are both sound and explicit. Natural language, by contrast, lives in a domain of interpretive openness, shaped by context, intention, and tacit knowledge. When an LLM maps informal narratives onto formal specifications, it is not merely performing translation; it is mediating between two radically different conceptions of meaning–one probabilistic, fluid, and distributed, while the other is deductive, sharp-edged, and grounded in mathematical ontology. The friction between these modalities is not incidental but structural: it reflects the philosophical divergence between linguistic practice in human communities and the logical formalism required for machine-checked reasoning. Addressing this tension requires more than improving models or datasets; it requires a deeper theoretical account of how semantic commitments are constructed, represented, and validated across these distinct epistemic regimes. A pressing difficulty arises from the absence of comprehensive datasets that faithfully bridge natural-language intentions with formal logical constructs in a way that reflects real-world complexity. However, the problem is not simply a lack of data; it is a lack of epistemically coherent corpora that map human concepts to formal invariants with philosophical integrity. Data of this sort is not merely collected but curated through informed judgement about meaning, relevance, and abstraction. In constructing such datasets, one confronts basic questions: What constitutes a faithful formalisation of a requirement? How do we distinguish essential semantic content from incidental narrative structure? How should ambiguity, intentional vagueness, or normative assumptions be represented–if at all–within a formal system that presupposes exactness? These questions reflect longstanding tensions in the philosophy of language and logic: the boundary between description and prescription, the nature of implicit commitments, and the status of meaning as inherently social rather than purely symbolic. Any dataset capable of supporting rigorous research into LLM-driven specification must therefore grapple with these philosophical issues rather than treat them as mere engineering obstacles. Another deep challenge concerns the fragmentation of the verification tool ecosystem and the implications this has for theories of representation. Different verification tools encode different worldviews i.e. different logics, abstraction mechanisms, and ontological commitments. Integrating LLMs into this landscape requires understanding these tools not as interchangeable mechanical components but as embodiments of distinct philosophical positions about computation, proof, and correctness. The absence of a unifying intermediate representation is thus more than a technical inconvenience; it is symptomatic of deeper theoretical disunity. A future in which LLMs and symbolic tools operate in a reciprocal, dialectical relationship–where neural inferences are shaped by logical constraints and symbolic proofs benefit from inductive heuristics–requires a synthesis between two kinds of reasoning historically seen as opposed: the inductive and the deductive, the heuristic and the foundational, the statistical and the formal. Developing such a hybrid architecture invites reflection on classical debates in the philosophy of mathematics regarding the interaction between intuition, pattern recognition, and formal proof such as in4. A further challenge lies in maintaining coherent traceability among evolving artefacts across the software lifecycle. Here the difficulty is not solely engineering complexity but the philosophical problem of identity over time: when a requirement changes, what exactly has changed–the words, the intention, the behavioural commitments, or the conceptual boundaries of the system itself? Traceability seeks to preserve a chain of meaning across transformations, yet automated systems struggle to model meaning as something that evolves holistically rather than as a collection of isolated statements. LLMs can produce plausible relational mappings, but plausibility is not a substitute for normatively valid justification. Addressing this issue requires 32 BEG ET AL. 86. Cleland-Huang J, Chang C, Christensen M. Event-based traceability for managing evolutionary change. IEEE Transactions on Software Engineering. 2003;29(9):796-810. doi: 10.1109/TSE.2003.1232285 87. Debiasi Duarte AM, Duarte D, Thiry M. TraceBoK: Toward a Software Requirements Traceability Body of Knowledge. In: 2016:236-245 88. Madaki AA, Zainon WMNW. A Review on Tools and Techniques for Visualizing Software Requirement Traceability. In: Mahyuddin NM, Mat Noor NR, Mat Sakim HA., eds. Proceedings of the 11th International Conference on Robotics, Vision, Signal Processing and Power ApplicationsSpringer Singapore 2022; Singapore:39–44. 89. Sengupta S, Kanjilal A, Bhattacharya S. Requirement Traceability in Software Development Process: An Empirical Approach. In: 2008:105-111 90. Cerbah F, Euzenat J. Using Terminology Extraction to Improve Traceability from Formal Models to Textual Requirements. In: Bouzeghoub M, Kedad Z, Métais E., eds. Natural Language Processing and Information SystemsSpringer Berlin Heidelberg 2001; Berlin, Heidelberg:115–126. 91. TORKAR R, GORSCHEK T, FELDT R, SVAHNBERG M, RAJA UA, KAMRAN K. REQUIREMENTS TRACEABILITY: A SYSTEMATIC REVIEW AND INDUSTRY CASE STUDY. International Journal of Software Engineering and Knowledge Engineering. 2012;22(03):385-433. doi: 10.1142/S021819401250009X 92. Pinheiro F, Goguen J. An object-oriented tool for tracing requirements. In: 1996:21993. Goknil A, Kurtev I, Berg v. dK, Veldhuis JW. Semantics of trace relations in requirements models for consistency checking and inferencing. Software & Systems Modeling. 2011;10(1):31–54. doi: 10.1007/s10270-009-0142-3 94. Hierons RM, Bogdanov K, Bowen JP, et al. Using formal specifications to support testing. In: . 41. 2009:9:1–9:76 95. Gaudel MC. Testing can be formal, too. In: Mosses PD, Nielsen M, Schwartzbach MI., eds. TAPSOFT95: Theory and Practice of Software Development, 6th International Joint Conference CAAP/FASE. 915 of Lecture Notes in Computer Science. Springer 1995:82–96 96. Kwiatkowska MZ, Norman G, Parker D. PRISM: probabilistic symbolic model checker. In: Field T, Harrison PG, Bradley JT, Harder U., eds. Computer Performance Evaluation, Modelling Techniques and Tools, 12th International Conference, TOOLS 2002. 2324 of Lecture Notes in Computer Science. Springer 2002:200–204 97. Hérault T, Lassaigne R, Magniette F, Peyronnet S. Approximate probabilistic model checking. In: Steffen B, Levi G., eds. Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004. 2937 of Lecture Notes in Computer Science. Springer 2004:73–84 98. Filieri A, Ghezzi C, Tamburrelli G. Run-time efficient probabilistic model checking. In: Taylor RN, Gall HC, Medvidovic N., eds. Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011ACM 2011:341–350 99. Agha G, Palmskog K. A survey of statistical model checking. ACM Transactions on Modeling and Computer Simulation. 2018;28(1):6:1–6:39. doi: 10.1145/3158668 100. Huang X, Ruan W, Huang W, et al. A survey of safety and trustworthiness of large language models through the lens of verification and validation. Artif. Intell. Rev.. 2024;57(7):175. doi: 10.1007/S10462-024-10824-0 101. Caglayan B, Wang M, Kelleher JD, et al. BIS: NL2SQL Service Evaluation Benchmark for Business Intelligence Scenarios. In: Springer-Verlag 2024; Berlin, Heidelberg:357372 102. Yan R, Cheng CH, Chai Y. Formal consistency checking over specifications in natural languages. In: 2015:1677-1682. 103. Tihanyi N, Jain R, Charalambous Y, Ferrag MA, Sun Y, Cordeiro LC. A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification. 2024. 104. Arora C, Sabetzadeh M, Briand L, Zimmer F. Extracting domain models from natural-language requirements: approach and industrial evaluation. In: MODELS ’16. Association for Computing Machinery 2016; New York, NY, USA:250260 105. Preda AR, Mayr-Dorn C, Mashkoor A, Egyed A. Supporting High-Level to Low-Level Requirements Coverage Reviewing with Large Language Models. In: MSR ’24. Association for Computing Machinery 2024; New York, NY, USA:242253 106. Casadio M, Dinkar T, Komendantskaya E, et al. NLP Verification: Towards a General Methodology for Certifying Robustness. 2025. 107. Necula SC, Dumitriu F, Greavu-erban V. A Systematic Literature Review on Using Natural Language Processing in Software Requirements Engineering. Electronics. 2024;13(11). doi: 10.3390/electronics13112055 108. Mukherjee P, Delaware B. Towards Automated Verification of LLM-Synthesized C Programs. 2024. 109. Luckcuck M, Farrell M, Dennis LA, Dixon C, Fisher M. Formal Specification and Verification of Autonomous Robotic Systems: A Survey. ACM Comput. Surv.. 2019;52(5). doi: 10.1145/3342355 110. Nouri A, Cabrero-Daniel B, Törner F, Sivencrona H, Berger C. Engineering Safety Requirements for Autonomous Driving with Large Language Models. In: 2024:218-228 111. Nazaruka E, Osis J. Determination of Natural Language Processing Tasks and Tools for Topological Functioning Modelling. In: ENASE 2018. SCITEPRESS - Science and Technology Publications, Lda 2018; Setubal, PRT:501512 Traceable and Verifiable Software Requirements: A Synthesis of AI-Enabled Formal Methods 33 T A B L E 5 Classification of Surveyed Literature by Methodology References Classification 1,2,12,13,41,29,38,8,54,101,19,61,59 33,52,18,12,13,55,52,54,35,24,25 Prompt-only 13,12,38,59,101 Prompt + Iterative / Human-in-loop / CoT 13,12,38,59,101 Prompt + Iterative / Human-in-loop / CoT 3,44,102,37,49,38,102,11,69 Fine-tuned 17,18,45,103,19,52,101,10,34,22,43,30 Verifier-in-loop 27,20,13,16,74 Neuro-symbolic (LLM + SMT/Theorem Prover) 28,47,44,5,28,47,34 Baseline / Manual / Controlled NL 37,104,42,21,104,100,23,36 Meta-analysis / Tool Support 46,34 IDE Integration Proposal 70,71,73,43,69,75,76 Dataset / Benchmark 15 Conversational / Ontology Requirements Engineering 34 BEG ET AL. T A B L E 6 Classification and Description of Surveyed Literature Ref. Tool / Work Classification Description 41 Domain Model Extractor Fine-tuned Generates domain models from NL requirements; evaluated in an industrial case study for performance and accuracy. 104 Symbolic NLP vs. ChatGPT Prompt-only Compares symbolic NLP and ChatGPT in generating correct JML from NL preconditions. 46 BPM-to-NL Translation Prompt-only Translates business process models to NL to support better stakeholder validation. 19 Lemur Verifier-in-loop Integrates LLMs with automated reasoners and defines sound transition rules for verification. 14 GPT-4o for VeriFast Verification Verifier-in-loop Assesses GPT-4os performance in generating C specs for VeriFast; captures issues in functional correctness. 45 ARSENAL Fine-tuned Extracts requirements from NL and performs automatic verification. 7Laurel for Dafny Prompt-only + Verifier-in-loop Automates generation of Dafny assertions to support SMT-based verification. 8PathCrawler + EVA Verifier-in-loop + Prompt PathCrawler generates context-aware ACSL annotations; EVA reduces runtime errors in Frama-C. 39 NL to Temporal Logic Translation Prompt-only Automatically translates NL into temporal logic for formal verification. 20 Req2Spec Prompt-only Converts NL requirements into formal specs (e.g., HANFOR); 71% accuracy on BOSCH data. 26 AssertLLM Multi-LLMs / Prompt-only Uses 3 customized LLMs to generate assertions from hardware design specs; 89% correctness achieved. 18 SpecSyn Fine-tuned Synthesizes software specifications from NL, improving over prior tools by 21%. 17 nl2spec Prompt-only + Iterative Refinement Iteratively generates formal specs from NL requirements, reducing ambiguity. 105 LLM-based Requirement Coverage Prompt-only Maps low-level requirements to high-level ones with 99.7% recall in coverage detection. 28 SpecLLM Prompt-only Uses LLMs to create and review VLSI design specs, enhancing chip documentation. 38 NL-to-LTL via LLMs Prompt-only Converts unstructured NL to NL-LTL pairs with 94.4% accuracy. 106 ANTONIO Toolkit Verifier-in-loop Introduces an NLP Verification Pipeline with metrics, gaps, and semantic subspace verification proposals. 12 GPT-3.5 for Code Verification Prompt-only Uses GPT-3.5 to verify code against requirements, providing feedback on requirement satisfaction. 29 GPT-4o + Claude for Smart Grid Verifier-in-loop Applies GPT-4o and Claude 3.5 for smart grid requirement verification, reaching 7994% F1-scores. 107 Systematic Review Meta-analysis Surveys NL-to-specification literature across domains and academic sources. 40 SAT-LLM Neuro-symbolic (LLM + SMT) Combines LLMs with SMT to detect complex conflicts in requirements. 32 Thor Neuro-symbolic Integrates LLMs with theorem provers using class methods like Hammers for proof completion. 67 Dafny Task Gen w/ CoT Prompt + Retrieval + CoT GPT-4 and PaLM-2 generate verified Dafny tasks via retrieval-augmented CoT prompting. 31 LeanDojo + ReProver Retrieval-augmented Retrieval-augmented LLM-based prover improves Lean theorem proving on 98K+ samples. 108 SynVer for C Verifier-in-loop Synthesizes and verifies C programs using VST with improved automation. 33 Copilot + Formal Methods IDE Integration Proposal Suggests integrating formal tools (e.g., Dafny, Coq, KeY) into IDEs like Copilot. 109 Robotic Systems Review Meta-analysis Reviews 10 years of literature on formal verification in autonomous robotic systems. 42 NLP for Software Dev Survey / Meta-analysis Evaluates NLP techniques in software development life cycle. 47 RML (1986) Manual / Controlled NL Introduces controlled NL framework for precise and consistent requirements writing. 103 ESBMC-AI Neuro-symbolic Uses LLMs + formal verification to detect vulnerabilities in software. 102 Specification Consistency Framework Manual / Baseline Aligns oral and formal specifications using semantic reasoning and input-output analysis. 110 LLM Safety Req. Pipeline Prompt-only Uses LLMs to decompose and refine autonomous vehicle safety requirements. 111 NLP Tools for TFM Prompt-only Compares NLP pipelines for topological modeling; CoreNLP and FreeLing perform best. Traceable and Verifiable Software Requirements: A Synthesis of AI-Enabled Formal Methods 35 T A B L E 7 Continued—Classification and Description of Surveyed Literature Ref. Tool / Work Classification Description 10 PALM (Proof-Aware LLM Method) Verifier-in-loop + Repair Framework Introduces PALM, a generatethenrepair framework combining large language models with symbolic reasoning to enhance formal proof generation in Coq. Analyzes 520 proof-generation errors by GPT-3.5 and introduces iterative repair mechanisms. Evaluated on 10,000+ theorems, achieving up to 180% higher success rates and proving 1,270 more theorems than prior systems, demonstrating strong generalizability. 11 AutoSpec Fine-tuned + Verifier-in-loop Presents AutoSpec, an automated framework synthesizing formal specifications that enables end-to-end program verification. Supports arrays, pointers, and nested loops via iterative synthesis and validation. Verifies 79% of benchmark programs (1.59Œ over existing methods) and validates real-world X509-parser project, ensuring satisfiable and provable specifications. 15 OntoChat Conversational LLM for ORE Introduces OntoChat, an LLM-powered conversational agent supporting Ontology Requirements Engineering (ORE). Automates and enhances tasks like elicitation, documentation, and validation in ontology development. Demonstrates improved efficiency, consistency, and collaboration compared to manual ORE pipelines. 16 HILBERT Agentic + Neuro-symbolic Verification Presents HILBERT, an integrated agentic framework combining informal reasoning, formal verification, and theorem proving. Coordinates reasoning agents, Lean 4 provers, and verifiers for collaborative proof construction. Achieves 99.2% accuracy on miniF2F and solves 70% of PutnamBench problems–surpassing proprietary and open baselines by large margins. 70 CLEVER Benchmark Dataset / Benchmark Introduces CLEVER, a benchmark for verifying code-level logical consistency in LLM-generated formal artifacts. Evaluates reasoning accuracy, specification completeness, and proof correctness across multiple verification engines. 71 CORE Dataset Dataset / Benchmark Provides CORE, a curated dataset linking natural-language software requirements to their formal counterparts in Dafny and Coq. Facilitates evaluation of NL-tospecification translation models for correctness and soundness. 73 VerifyThisBench Benchmark / Evaluation Presents VerifyThisBench, a comprehensive benchmark of 150+ verification problems. Measures LLM capabilities in producing provable Dafny, Coq, and Viper proofs, emphasizing stepwise reasoning and proof correctness. 43 DafnyBench Dataset / Verifier-in-loop Introduces DafnyBench, a large-scale benchmark for evaluating LLMs in generating and verifying Dafny specifications. Enables quantitative comparison of reasoning-based verification success rates. 22 RvLLM Framework Verifier-in-loop + Runtime Verification Combines runtime verification with LLM-based formalization to dynamically validate safety-critical behaviors in real-time systems. Integrates SMT-guided feedback for iterative correction. 34 Ada/SPARK-LLM Assistant Verifier-in-loop + IDE Integration Proposes LLM-assisted generation of Ada/SPARK contracts. Integrates within verification IDEs, enabling real-time correction of inconsistencies and generation of postconditions from natural language requirements. 35 GenAI-Driven Design-by-Contract Prompt-only + Formal Spec Generation Investigates how LLMs can automatically synthesize design-by-contract specifications in languages like Eiffel and SPARK from informal requirements, improving traceability and contract coverage. 74 ClassInvGen Neuro-symbolic + Invariant Synthesis Introduces ClassInvGen, a system for automatic generation of class invariants using hybrid symbolicLLM reasoning. Achieves 90% correctness in inferred invariants across benchmark programs. 24 PastLTL formulae Prompt-only + Temporal Logic Translation Presents a system for transforming natural language safety requirements into Past LTL formulae using LLM-guided semantic parsing, enabling temporal property verification. 25 LoopInvariantFinder Prompt + Symbolic Refinement Explores using GPT-4 and symbolic solvers to automatically infer loop invariants for C and Java programs. Achieves state-of-the-art generalization on the LoopInvGen dataset. 69 PURE Dataset Dataset / Fine-tuned Provides the PURE dataset mapping software requirements to Prolog-based logical rules, used to fine-tune LLMs for precise logic translation. 23 Farrel et al. 2025 Study Meta-analysis / Empirical Review Presents an empirical synthesis of model-based verification approaches leveraging LLMs and symbolic solvers across safety-critical domains. 100 Trustworthiness in LLM Verification Survey Meta-analysis / Survey Surveys approaches to evaluate and improve trustworthiness, interpretability, and safety of LLMs in software verification and formal reasoning contexts. 36 Barbosa et al. (2024) – JSS Review Meta-analysis / Review Reviews LLM-assisted formal verification frameworks in system design. Provides taxonomic classification of prompt-based, verifier-in-loop, and symbolic methods. 30 SV-LLM for SoC Verification Domain-specific / Verifier-in-loop Applies LLMs to SystemVerilog design verification tasks, generating functional assertions and testbench code. Demonstrates significant improvements in coverage for SoC-level validation. 16 HILBERT Neuro-symbolic / Agentic Proof Framework Integrates informal reasoning, formal verification, and theorem proving within an agentic architecture. Achieves SOTA results on formal mathematics benchmarks (miniF2F and PutnamBench). 75 Verina Dataset / Verifier-in-loop Comprising 189 manually curated coding tasks in Lean, each accompanied by precise problem statements, reference implementations, formal specifications, and exhaustive test suites. Evaluated dataset empirically. 76 CASP – C-ASCL Pairs Dataset / Verifier-in-loop / Human-in-loop introduced C-ACSL (CASP), a curated evaluation set comprising 506 C functions paired with ACSL specifications, constructed through a multi-stage extraction and verification pipeline.