Requirements engineering digest, week 34 of 2026

1. The Specification Paradox: Rethinking Requirements Engineering in the Age of AI

   Tassio Sirqueira, Jessica Faciroli

   arXiv (cs.SE) · preprint

   Argues that the language models writing the code do not remove the difficulty of building software, they move it: into domain understanding, elicitation, specification, validation and evolution. From that the authors state the Specification Paradox, that the better machines get at generating software from a specification, the more everything depends on that specification being correct, complete, verifiable and explainable, and name the failure modes on the way, automation bias, ambiguity propagation, specification overfitting and specification debt.

   Abstract

   The growing adoption of Large Language Models (LLMs) in Software Engineering has reinforced the expectation that coding activities can be largely automated. However, this perception may represent yet another historical search for a solution capable of eliminating the inherent challenges of software development. This article discusses the transition from a code-centered paradigm to Specification-Driven Development. We argue that artificial intelligence reduces some of the effort associated with writing source code, but it does not eliminate the complexity of developing professional software systems. Instead, it shifts this complexity toward domain understanding, requirements elicitation, specification development, validation, maintenance, and software evolution. Building on this perspective, we discuss the renewed centrality of Requirements Engineering, considering its implications for productivity and software quality, as well as risks associated with automation bias, ambiguity propagation, Specification Overfitting, and the accumulation of Specification Debt. Finally, we propose the Specification Paradox: the more capable artificial intelligence systems become at automatically generating software, the greater the dependence on correct, complete, verifiable, and explainable human-produced specifications. We conclude that the future of Software Engineering will depend not only on machines' ability to generate code, but also on humans' ability to correctly specify, evaluate, and evolve what is intended to be built.

   Source: arxiv.org/abs/2608.16618

2. LadderTeam: Dual-Agent Laddering Elicitation Framework

   Manjushree Aithal, Alexander Kotz, James Mitchell

   arXiv (cs.SE), to appear at ACM AI Summit 2026 · accepted

   Automates the laddering interview, an elicitation technique that is effective and manual and therefore does not scale, with two agents: an interviewer running one of three probing strategies over usability feedback, and a judge watching each probe-response pair and pulling the interview back when it drifts. Evaluated over 216 simulated interviews against scripted ground-truth transcripts, so that probe quality is the only variable and no participant variance is in the way.

   Abstract

   Eliciting detailed and actionable software requirements from end-users is a critical phase in the iterative development of a software product or application. To ensure the feedback collected is detailed and actionable, software teams can leverage the laddering interview technique. While effective for ensuring granular and actionable items from the software feedback, these interviews are subject to several limitations. They are traditionally a manual process associated with a time and financial burden, limiting scalability; interviewers must balance probing for depth while managing interviewee behavioral and cultural constraints. To address these limitations, we present LadderTeam, an open, reproducible framework that automates UX wireframe interviews using a dual-agent Large Language Model (LLM) architecture. An active interviewer agent executes one of three probing strategies (ACV, 5-Whys, and JTBD) to elicit actionable software requirements from usability feedback comments, while a concurrent background Judge agent evaluates probe-response pairs and triggers real-time guardrails to prevent topic drift. To rigorously evaluate LLM laddering without participant variance confounds, we introduce a controlled simulation methodology utilizing scripted ground-truth transcripts to isolate probe quality as the sole experimental variable. Across 216 interviews, LadderTeam achieved 99.1% chain convergence and an 81.0% ground-truth actionable response match (86.1% reluctant personality, 75.9% terse personality) with zero drift across all runs. All evaluation code, all transcripts, inputs, and a live demonstration platform will be open-sourced upon acceptance.

   The source publishes this abstract as raw markup. Macros have been replaced by the text the publisher's own rendering shows for them, and the rest of the markup removed. The authors' wording is unchanged.

   Source: arxiv.org/abs/2608.17029

3. Measuring What a Specification Determines: A Formal Semantic-Block Model and an Execution-Judged Benchmark

   Oleg Grynets, Dmytro Kostetskyi, Vasyl Lyashkevych

   arXiv (cs.SE) · preprint

   Models a specification as semantic blocks with dependencies, block-owned rules, decision points and explicitly open questions, under four machine-checkable well-formedness conditions, and defines determinacy as agreement among all conforming implementations. Tested on an Oracle to PostgreSQL migration specification with language models as the implementers and live databases as the judge, determinacy holds up as a formal concept but not as a standalone measure of specification quality.

   Abstract

   This work introduces a formal semantic-block model for specifications and an execution-judged benchmark for evaluating specification quality independently of model capability. A specification is represented as a structure comprising semantic blocks, dependency relations, block-owned rules, decision points, and explicitly open questions, subject to four machine-checkable well-formedness conditions: acyclicity, single ownership, constraint domination, and totality or ambiguity-stop. Determinacy is defined model-theoretically as agreement among all conforming implementations and is estimated empirically through convergence across independent implementers. The model is instantiated on an Oracle-to-PostgreSQL migration specification containing 18 blocks and 19 dependency edges. Computational validation shows that the five-layer decomposition reduces mean per-task context by approximately 71% through dependency closures, covers 85.5% of the study-defined Oracle construct taxonomy with all identified gaps triaged, is not Pareto-dominated by the tested alternative partitions, and is recovered at the 99.9th percentile from citation-derived edges not used to define the original structure. The benchmark keeps the implementer panel fixed, includes a mandatory no-specification control arm, and uses PostgreSQL 16 and a live Oracle instance as deterministic execution judges. Six designed studies, including three pre-registered manipulations and three diagnostic analyses, further examine specification effects. Repeated runs on a 25-unit subsample reveal an empirical variability floor with a median arm-delta spread of 14.4 percentage points. The results support determinacy as a formal concept but not as a standalone empirical quality metric for the evaluated contemporary LLM implementers.

   Source: arxiv.org/abs/2608.19475

4. An Agentic RAG and Evaluation Framework for Assurance Case Generation: Industrial Use Case for the EU Cyber Resilience Act Compliance

   Fariz Ikhwantri, Iker Lasa Ojanguren, Dusica Marijan, Maria I. Maslioukova, José Arias Marin, Pavlos Kosmides

   arXiv (cs.SE), to appear at ISSRE 2026, industry track · accepted

   Conformity assessment under the EU Cyber Resilience Act is expensive for a small company, and most of the work is mapping technical documentation requirements onto evidence. This pipeline derives assurance cases from that documentation, grounded in Claim-Argument-Evidence logic, and checks each one for grounding with a natural language inference evaluator. Validated on a wildfire monitoring product, where it produced 70 assurance cases at roughly 4.4 artefacts each.

   Abstract

   Complying with the EU Cyber Resilience Act (CRA) is a resource-intensive challenge for SMEs due to the complexity of cybersecurity conformity assessment. Yet, it is essential for demonstrating regulatory compliance and ensuring product security and resilience. To address this, we introduce an automated framework for generating Assurance Cases (ACs) using an agentic Retrieval-Augmented Generation grounded in a formal Claim-Argument-Evidence logic. By systematically mapping technical documentation requirements, the framework streamlines the generation of certification evidence. We validate our approach on a case study of Catalink's PATROLIoT wildfire monitoring system, where the agentic RAG generated 70 ACs with high grounding density (~4.4 artefacts per AC). The proposed Natural Language Inference (NLI) evaluator achieves 0.88 accuracy, which provides robust evidence grounding and traceability, while expert-validated plausibility (3.06) supports interpretable justifications. For practitioners, this work provides a scalable, interpretable approach for automating mandatory CRA conformity assessments, reducing manual effort while maintaining transparent decision support.

   Source: arxiv.org/abs/2608.19509

5. Trace-Based Execution-Level Observability of VDM-SL Specifications

   Tomohiro Oda, Han-Myung Chang

   arXiv (cs.SE), presented at the 24th Overture Workshop · published

   A VDM specification can be animated and stepped through in a debugger, but what happens inside an operation is gone as soon as the run ends. This records the assignments, operation calls and returns as execution traces, which makes the internal behaviour persistent and analysable as a state-based model, with an implementation in ViennaTalk and an application to visualisation.

   Abstract

   VDM has been pursuing rigorous verification through mathematical theorem proving and software testing via simulated execution. Animation through an interpreter enables validation of the specification to ensure it meets the required functionality. Step-by-step execution in a debugger also allows the user to follow the internal behavior of operations. In this paper, we propose the recording and utilization of execution traces of assignments, operation calls, and return statements to make the internal behavior of operations persistent and analyzable as state-based models. The data model of events in execution traces, its implementation in ViennaTalk, and its application to visualization will be introduced.

   Source: arxiv.org/abs/2608.19510

6. Escaping the Quicksand: A Call to Arms

   Peter Sewell, Jean Pichon-Pharabod

   arXiv (cs.PL) · preprint

   Seventy-five years of building systems to prose specifications with test-and-debug development has left foundations the authors call shaky, and AI-assisted engineering is adding technical debt faster while automating the discovery of the vulnerabilities in it. Their answer is not proof everywhere but executable partial specifications co-developed alongside the prose, the code and the tests, and the semantics infrastructure that would make this practical for the main programming languages.

   Abstract

   Computing has been an astonishing success - but the accumulated technical debt exposes us all to huge costs in business and societal risk. For 75 years, we've built systems to prose specifications with test-and-debug development. That works well enough for industry to thrive, but it's an expensive and ineffective feedback loop, and leaves everyone relying on shaky foundations. Now, AI-enabled engineering is amplifying the success by reducing coding costs, but also amplifies the risks, by rapidly increasing technical debt, and by automating detection of the vulnerabilities therein. How can we do better? Research has long pursued mathematical proof of correctness, which, unlike testing, can cover all cases. This too has advanced massively, but it remains hard to apply, both technically and because of a deep-seated cultural disconnect. Instead, we argue for a pragmatic approach to flexible combinations of testing, *specification*, and proof, that provides more effective feedback loops for both AI and human development. Most simply, one can incrementally co-develop executable-as-test-oracle partial specifications alongside conventional prose descriptions, code, and tests. This clarifies design and makes testing much more discriminating. Developers can and should do it today. Or, even better, one can use specifications that support the full gamut of testing, property-based testing, symbolic execution, and proof. This enables a range of intertwined feedback loops, again both for AI and humans, from cheap testing to more expensive proof. However, making it really practical needs *semantics infrastructure*: specifications and tooling for the main programming languages and other abstractions, which we now more-or-less know how to build, but which is not yet in place. We call the community to arms to create and deploy it - to enable a future built on firmer ground.

   Source: arxiv.org/abs/2608.19674

7. Specification-delta-driven data governance: an empirical study of the «spec-delta» as the unit of change in lakehouse data platforms

   Pablo Ramirez Amador

   arXiv (cs.AI) · preprint

   Spec-driven development has settled on the specification rather than the code as the artefact that governs AI-assisted work, but the specification delta, the reviewable increment of requirements that each change should produce, has not been studied where changes are contractual rather than code: new datasets, service-level agreements, metric semantics, access policies. This formalises the spec-delta, classifies data platform changes by how well they suit incremental specification, and designs the experiment against a conventional pull-request workflow.

   Abstract

   Spec Driven Development SDD has consolidated the idea that the specification rather than the code should be the primary artefact governing AI assisted work. Tools such as GitHub Spec Kit, and proposals such as Constitutional SDD, have formalised this principle in the software domain, while the executable data-contracts literature has extended it to schema and quality enforcement at run time. Nevertheless, the treatment of the specification delta OpenSpec's core idea that every change should produce a reviewable increment of requirements as the unit of change in data platforms remains empirically unexplored, even though many data-platform changes are contractual (new datasets, service-level agreements, metric semantics, access policies) rather than purely code changes. This work formalises the spec-delta concept, proposes a taxonomy of data platform changes according to their suitability for incremental specification, and defines a controlled experiment comparing a spec-delta-driven workflow against a conventional code pull-request workflow without a delta. The response variables are discovery to deployment time, the density of defects reaching the Silver and Gold lakehouse layers, cross-tool metric divergence, and reviewer cognitive load measured with NASA TLX. The paper explicitly reserves a demonstration-and-laboratory section for instantiation on a real lakehouse environment. The contribution is not a tool but reproducible evidence and an applicability guide that helps to avoid the up front over specification antipattern.

   Source: arxiv.org/abs/2608.19838

8. Further Progress Towards Operation Proof Obligation Generation for VDM

   Nick Battle, Carlo Rende, Peter Gorm Larsen

   arXiv (cs.SE), presented at the 24th Overture Workshop · published

   VDM checks a model against itself by generating proof obligations, the assertions that would have to hold for it to be internally consistent. This instalment improves the treatment of loop invariants, adds loop variants, extends obligations to operation calls including implicitly declared operations and specification statements, and adds recursive measures for operations.

   Abstract

   The VDM formalism can ensure that models are internally consistent. Potential inconsistencies are highlighted by assertions called proof obligations. This paper is an update to the work described in [1], regarding proof obligation generation for VDM operations. We present the latest work which improves the approach to loop invariants, adds loop variants, improves proof obligations for operation calls, including implicitly declared operations and specification statements, and adds recursive measures for operations. The new features are illustrated with examples.

   Source: arxiv.org/abs/2608.19848