LLM-Based Static Verification of Code Against Natural-Language Requirements: An Industrial Experience Report

• URL: http://arxiv.org/abs/2605.17926v1
• Date: Mon, 18 May 2026 06:34:03 GMT
• Title: LLM-Based Static Verification of Code Against Natural-Language Requirements: An Industrial Experience Report
• Abstract summary: This article presents a two-stage LLM-based workflow for addressing this challenge in an intelligent-vehicle cybersecurity case study.<n>In the first stage, an AI-based rule miner extracts verifiable rules from natural-language requirements.<n>In the second stage, an AI-based code auditor checks implementation evidence against the extracted rules.
• Score: 3.5867640049033054
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models (LLMs) are increasingly used to generate requirements specifications, design documents, code, and test cases. In contrast, much less attention has been given to a more difficult assurance problem: statically verifying whether implemented code satisfies requirements written in natural language. Conventional static analysis tools are effective at detecting coding defects and known vulnerability patterns, but they cannot determine whether program behavior matches intended business logic. Detecting such defects requires reasoning over the specification rather than the code alone. Software testing can expose some of these mismatches, but its effectiveness depends heavily on test design, executable artifacts, and runtime environments. This article presents a two-stage LLM-based workflow for addressing this challenge in an intelligent-vehicle cybersecurity case study. In the first stage, an AI-based rule miner extracts verifiable rules from natural-language requirements while explicitly identifying ambiguity, self-contradiction, and other non-verifiable statements. In the second stage, an AI-based code auditor checks implementation evidence against the extracted rules. Instead of asking a single LLM to directly verify code against lengthy natural-language specifications, the workflow introduces a structured intermediate representation to reduce hallucination, output variability, limited explainability, and context loss. The resulting approach is a requirement-aware and semantics-aware form of static analysis that complements software testing. By analyzing requirements and source code without requiring compilation, execution, or runtime environments, the method shifts verification and validation activities left in the development lifecycle. This LLM-based static analysis is also a new approach to addressing the test oracle problem.

Related papers

• The Imitation Game: When LLMs Learn to Reason Like Programs via Code-Centric Reasoning Data Synthesis [50.473217152006875]
  MIMIC is a framework that leverages executable code as a rigorous medium for reasoning data synthesis.<n>MIMIC transforms algorithms into verifiable reasoning trajectories through narrative fusion, code-guided test synthesis, and dynamic code instrumentation.<n>Our method significantly elevates accuracy across general reasoning, complex mathematical benchmarks, and fine-grained deterministic tasks.
  arXiv  Detail & Related papers  (2026-09-13T17:04:16Z)
• ClarifyCodeBench: Evaluating LLMs on Clarifying Ambiguous Requirements for Code Generation [54.788849448970154]
  We introduce ClarifyCodeBench, a novel interactive benchmark for evaluating Large Language Models' capability in resolving requirement ambiguity.<n>We conduct a systematic evaluation of six state-of-the-art LLMs using ClarifyCodeBench.<n>Our empirical results yield three critical insights: 1) Capability Decoupling: Strong code generation performance does not inherently translate to effective requirement clarification; 2) The Reasoning Paradox: While increased computational thinking enhances code correctness, it yields marginal gains in identifying ambiguities.
  arXiv  Detail & Related papers  (2026-07-01T09:58:59Z)
• From I/O to Code with Discovery Agent [103.88427301265669]
  We propose DIO-Agent, a discovery agent for IO2Code.<n>Our method frames IO2Code as an evolutionary search over discrete program space.<n>Extensive experiments show that DIO-Agent consistently outperforms both traditional program-by-example method and SOTA evolution-agent baselines.
  arXiv  Detail & Related papers  (2026-05-14T18:57:32Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  Large language models (LLMs) and agents have shown promising progress, but their true capabilities and failure modes remain unclear.<n>We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs.
  arXiv  Detail & Related papers  (2026-05-02T11:31:33Z)
• Assessing the Impact of Requirement Ambiguity on LLM-based Function-Level Code Generation [14.755517753769837]
  We introduce Orchid, the first code generation benchmark specifically designed with ambiguous requirements.<n>It comprises 1,304 function-level tasks covering four distinct types of ambiguity: lexical, syntactic, semantic, and vagueness.<n>Our results demonstrate that ambiguity consistently degrades the performance of all evaluated LLMs, with the most pronounced negative effects observed in highly advanced models.
  arXiv  Detail & Related papers  (2026-04-23T10:07:33Z)
• Are LLMs Reliable Code Reviewers? Systematic Overcorrection in Requirement Conformance Judgement [8.059802912761919]
  We uncover a systematic failure of large language models (LLMs) in matching code to natural language requirements.<n>More detailed prompt design, particularly with those requiring explanations and proposed corrections, leads to higher misjudgment rates.<n>We propose a Fix-guided Verification Filter that treats the model proposed fix as executable counterfactual evidence.
  arXiv  Detail & Related papers  (2026-02-28T08:35:25Z)
• Operational Robustness of LLMs on Code Generation [2.9232837969697965]
  It is now common practice in software development for large language models (LLMs) to be used to generate program code.<n>This paper is concerned in particular with how sensitive LLMs are to variations in descriptions of the coding tasks.<n>Existing techniques for evaluating this robustness are unsuitable for code generation because the input data space of natural language descriptions is discrete.
  arXiv  Detail & Related papers  (2026-02-21T11:21:13Z)
• Environment-Aware Code Generation: How far are We? [52.69113158357018]
  It is unclear whether large language models (LLMs) can reliably generate executable code tailored to a user's specific environment.<n>We present the first systematic study of Environment-Aware Code Generation (EACG), where generated code must be functionally correct and directly executable under arbitrary software configurations.<n>Our results show that current LLMs struggle with environment-specific code generation, while our adaptations improve environment compatibility and executability.
  arXiv  Detail & Related papers  (2026-01-18T04:58:15Z)
• Rethinking Testing for LLM Applications: Characteristics, Challenges, and a Lightweight Interaction Protocol [83.83217247686402]
  Large Language Models (LLMs) have evolved from simple text generators into complex software systems that integrate retrieval augmentation, tool invocation, and multi-turn interactions.<n>Their inherent non-determinism, dynamism, and context dependence pose fundamental challenges for quality assurance.<n>This paper decomposes LLM applications into a three-layer architecture: textbftextitSystem Shell Layer, textbftextitPrompt Orchestration Layer, and textbftextitLLM Inference Core.
  arXiv  Detail & Related papers  (2025-08-28T13:00:28Z)
• Uncovering Systematic Failures of LLMs in Verifying Code Against Natural Language Specifications [0.6813925418351435]
  Large language models (LLMs) have become essential tools in software development, widely used for requirements engineering, code generation and review tasks.<n>In this paper, we uncover a systematic failure of LLMs in evaluating whether code aligns with natural language requirements.<n>Our results reveal that LLMs frequently misclassify correct code implementations as either not satisfying requirements'' or containing potential defects.
  arXiv  Detail & Related papers  (2025-08-17T13:07:26Z)
• FaultLine: Automated Proof-of-Vulnerability Generation Using LLM Agents [17.658431034176065]
  FaultLine is an agent workflow that automatically generates proof-of-vulnerability (PoV) test cases.<n>It does not use language-specific static or dynamic analysis components, which enables it to be used across programming languages.<n>On a dataset of 100 known vulnerabilities in Java, C and C++ projects, FaultLine is able to generate PoV tests for 16 projects, compared to just 9 for CodeAct 2.1.
  arXiv  Detail & Related papers  (2025-07-21T04:55:34Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  Code generation with large language models (LLMs) is increasingly adopted in production but fails to ensure code quality.<n>We propose REAL, a reinforcement learning framework that incentivizes LLMs to generate production-quality code.
  arXiv  Detail & Related papers  (2025-05-28T17:57:47Z)
• Exploring Software Naturalness through Neural Language Models [56.1315223210742]
  The Software Naturalness hypothesis argues that programming languages can be understood through the same techniques used in natural language processing. We explore this hypothesis through the use of a pre-trained transformer-based language model to perform code analysis tasks.
  arXiv  Detail & Related papers  (2020-06-22T21:56:14Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.