Requirements engineering digest, week 39 of 2026

1. Djinnlang: Higher-Level Programming by Unambiguous Specification with an LLM in the Compiler

   Simon Henniger, Stephen Chong, Nada Amin

   arXiv (cs.SE) · preprint

   Introduces Djinnlang, a specification language in which programs consist only of formal specifications that an LLM implements and proves correct against, using an unambiguity constraint that forces the specification to fully determine program behaviour.

   Abstract

   Programmers write formal specifications, and LLMs implement them, proving that each implementation matches its spec. Taken to its extreme, this makes specification languages the new programming languages. We argue that an unambiguity constraint is key: in addition to proving that its implementation satisfies the specification, the LLM must also prove that any other implementation satisfying it must produce the same outputs on the same inputs, i.e. that the relation formed by the constraints is deterministic. This leaves the LLM no leeway on program semantics: as with a conventional compiler, the generated code never needs to be read and can be regenerated from the spec at any time. Under this constraint and with a powerful LLM, the difference between a specification language and a programming language becomes essentially meaningless, and the LLM essentially becomes a part of the compiler toolchain. The arrangement doubles as a strong form of AI control: an untrusted model writes the code, yet its work is tightly checked by a verifier. To demonstrate that our LLM-in-the-compiler paradigm is feasible when supported by our unambiguity constraint, we present Djinnlang, a high-level specification language built for this future. A Djinnlang program consists only of specifications --- the programmer never writes executable code. In place of a traditional compiler, a symbolic translator lowers each spec to Dafny stubs and proof obligations, and a driver harness orchestrates an LLM that fills in implementations and proofs, all checked by the Dafny verifier. We evaluate our language and implementation on multiple examples and we show that it is self-hosting: an LLM can implement the Djinnlang translator from its specification and the reimplementation can verify itself.

   Source: arxiv.org/abs/2609.23954

2. Specifying and Maintaining Agentic Workflows: An Empirical Study of GitHub Agentic Workflows

   Jasem Khelifi, Issam Oukhay, Ali Ouni, Mohammed Sayagh, Mohamed Aymen Saied

   arXiv (cs.SE) · preprint

   An empirical study of 1,248 GitHub Agentic Workflow files across 276 repositories, examining how developers structure, evolve, and maintain these Markdown files as operational specifications for recurring, agent-executed repository tasks.

   Abstract

   Agentic workflows shift software development from prompting AI agents for individual tasks to defining recurring work that agents execute automatically. GitHub Agentic Workflows (gh-aw) enables this approach through Markdown files that combine natural-language instructions with configuration and compile into executable GitHub Actions workflows. Unlike conventional workflows that primarily prescribe scripted operations, these files delegate tasks requiring interpretation to AI agents. They also couple agent instructions with execution triggers, making those instructions operational specifications for repeated repository activities. However, how developers structure and maintain these specifications, and which execution requirements and safeguards they express, remains insufficiently understood. In this paper, we examine the structure, evolution, and instruction content of gh-aw Markdown files to inform how practitioners define and maintain agent-run work. We analyze 1,248 files from 276 repositories, 20,841 commit-file events, and 288 resolved instruction-label sets from a sample of 294 files. Our results show that workflow instructions extend beyond short prompts, with a median of 556.5 words and code blocks in 62.1% of files. Among files with at least 120 days of observed activity, 78.2% still receive updates in month 4, while size-normalized churn decreases after the first month. Tasks, outputs, constraints, and process instructions each appear in over 93% of labeled workflows, yet only 9.4% explicitly address prompt-injection defense. LLM classification achieves an F1 score of 0.818 and Cohen's Kappa of 0.715 against the resolved human labels. These findings suggest that developers should account for the evolution of workflows copied or referenced across repositories and consider adding prompt-injection defenses, resource budgets, and evidence-credibility checks where applicable.

   Source: arxiv.org/abs/2609.27263

3. Constraint-Driven Context Engineering: Designing Domain Interfaces for AI Systems

   Xiwei Xu, Chen Wang, Mengmeng Yang, Yipeng Zhang, Jacky Jiang, Suyu Ma, Youyang Qu, Ming Ding, Liming Zhu

   arXiv (cs.SE) · preprint

   Proposes Constraint-Driven Context Engineering, a Domain-Driven-Design-based method for eliciting and operationalising the technical, regulatory, and normative constraints that govern deployed AI systems, evaluated through case studies in education, healthcare, and finance.

   Abstract

   Generative AI systems are increasingly deployed to address domain problems. These systems operate under technical, regulatory, institutional, and normative constraints that define acceptable AI behaviour and outcomes within their domains. We observe a recurring pattern in our industry engagement: partners often arrive with a functioning but relatively generic AI solution. The challenge is no longer to build an AI system from scratch, but to improve the quality and domain appropriateness of an AI-generated solution. In these settings, the limiting factor is often the quality, scope, and structure of the context available to the system. Yet, existing context engineering approaches primarily focus on supplying domain knowledge through retrieval, memory, and tools, with limited support for systematically identifying and operationalising the constraints that govern AI systems in their operational environments. This paper proposes Constraint-Driven Context Engineering (CDCE), a design approach for engineering domain interfaces for AI systems. Drawing on software architecture design and Domain-Driven Design (DDD), CDCE treats domain constraints as first-class design drivers. It identifies and characterises constraints, determines the required context assets, and designs representations through which these assets are made available to AI systems. We conducted a comparative multiple-case study with industry and public-sector partners across educational assessment, healthcare decision support, and financial-distress prediction. Depending on their characteristics, constraints can guide AI behaviour, enforce permissible boundaries, or support verification of AI-generated outcomes. The cases demonstrate CDCE's applicability across contrasting domains and show how constraint characteristics shape the resulting domain interfaces.

   Source: arxiv.org/abs/2609.27354

4. LLM-Assisted Workflow for Structural Difference Visualization in Evolving Software Requirements

   Koi McFarland, Songhui Yue

   arXiv (cs.SE) · preprint

   Presents an LLM-assisted workflow that represents evolving software requirements as triple-based semantic graphs and visualizes structural differences between baseline and current requirement sets to support requirements-change review.

   Abstract

   This paper presents an LLM-assisted workflow for visualizing structural differences in evolving software requirements. Implemented in the OntologyWeb environment, the workflow represents baseline and current requirements as triple-based semantic graphs and supports side-by-side comparison of curated graph snapshots. The comparison view aligns matched entities and uses visual encoding to highlight structural changes.

   Source: arxiv.org/abs/2609.28002

5. Developing a Unified Verification and Validation Activity Standard at JPL

   Maximilian Vierlboeck, Ellen Van Wyk, Natalia Sanchez, Bogdan Oaida, Torrance James Eberhart, Marie Piette Gomez, Christopher Delp, Marijke G. Jorritsma, Alex Desharnais

   arXiv (cs.SE) · preprint

   Reports on a human-centered design effort at NASA JPL to unify verification and validation practice across missions into a single SysML-based schema linking requirements, V&V activities, venues, and evidence, implemented in the Jama platform.

   Abstract

   Verification and validation practices (V&V) at NASA's Jet Propulsion Laboratory (JPL) have diverged over the past decade, creating fragmentation that increases overhead, reduces cross-project efficiencies, and inhibits institutional knowledge transfer. We present a unified V&V activity schema developed through human-centered design workshops involving 29 practitioners across multiple mission types and disciplines. The schema builds on a relationship-based architecture that allows for separating methods (Test, Analysis, Inspection, Demonstration, and Review of Design) while maintaining a common attribute set. Formalized as a platform-agnostic SysML model, the schema defines bidirectional relationships between requirements, V&V activities, venues, and evidence. Implementation in JPL's Jama platform demonstrates controlled customization through templates and modular item types, balancing rigor with agility while enabling automations, pattern reuse, and digital thread integration.

   Source: arxiv.org/abs/2609.28600

6. Specification-Driven Benchmarking for Automated Program Repair From Static Corpora to Executable Specifications

   Yasser Ebrahim

   arXiv (cs.SE) · preprint

   Proposes specification-driven benchmarking for automated program repair, in which benchmarks are defined by executable specifications of their intended properties and realised by a generation pipeline, replacing static, contamination-prone benchmark corpora.

   Abstract

   Automated Program Repair (APR) benchmarks have traditionally been constructed as static datasets whose characteristics are inherited from the defects they contain. While this paradigm has enabled decades of progress, finite corpora provide limited experimental control, become increasingly susceptible to contamination as they are reused, and cannot be systematically regenerated or adapted as evaluation requirements evolve. We propose specification-driven benchmarking, a paradigm in which benchmarks are defined by executable specifications and realized through benchmark generation. The specification explicitly declares the intended properties of the benchmark (including program context, fault taxonomy, difficulty, validation strategy, and corpus constraints) while a generation pipeline realizes those requirements through independent generation, validation, and corpus management components. We develop the conceptual foundations of this approach by introducing a taxonomy of benchmark specification dimensions, establishing how each specification dimension maps to deterministic architectural responsibilities, and arguing that independent validation is a structural requirement for trustworthy benchmark generation. An end-to-end example illustrates how specification choices propagate through the pipeline to produce benchmark instances whose properties are independently verifiable. By treating the benchmark as an executable specification rather than a static dataset, the proposed paradigm shifts benchmark construction from artifact curation to declarative experimental design.

   Source: arxiv.org/abs/2609.28896

7. On the Impact of Requirement Smells in LLM-Based Code Generation

   Hugo Villamizar, Jannik Fischbach, Mert Şahin, Julian Frattini, Alessio Ferrari, Alexander Korn, Andreas Vogelsang, Daniel Mendez

   arXiv (cs.SE) · preprint

   Extends prior requirements-traceability work to show that progressively injecting semantic, syntactic, and lexical requirement smells into otherwise clear requirements reduces the functional correctness of LLM-generated code, though smell-free requirements do not guarantee correctness either.

   Abstract

   Software requirements are typically incorporated into prompts used in LLM-assisted software development. Recent work has shown that requirement smells can affect automated traceability between requirements and code, but empirical evidence on their effects in code generation remains limited. To address this gap, we build upon a prior study on automated traceability by reusing its dataset and requirement smell taxonomy, while extending it to evaluate the functional correctness of LLM-generated code. Using a benchmark consisting of requirements and corresponding system tests for four applications, we progressively introduced semantic, syntactic, and lexical smells into otherwise clear requirements and analyzed their influence on generated implementations. Our results suggest that increasing smell density was generally associated with lower test-suite-based functional correctness, although non-smelly requirements could still produce faulty code. We also found that different smell categories had similar effects. These findings provide additional empirical evidence of the importance of requirement quality in LLM-assisted code generation, while showing that high-quality requirements alone do not guarantee correctness, as these depends on several factors, including the LLM. Compared with previous work, our results suggest that the impact of requirement smells depends on the software engineering task: whereas their effects on traceability were modest, code generation appears more sensitive. Overall, this work motivates further investigation into task-dependent quality effects in LLM-assisted software engineering.

   Source: arxiv.org/abs/2609.29208

8. Formal Model Construction Guided by Model-Based Proof Sketches

   Hongshu Wang, Xinyue Zuo, Yufan Cai, Neeraj Kumar Singh, Yamine Ait Ameur, Jin Song Dong

   arXiv (cs.SE) · preprint

   Proposes ProGS, an LLM-based autoformalization method that organises formal model construction around hierarchical model-based proof sketches so verification failures can be localized and repaired at the right subgoal, improving on prior generate-and-repair approaches to specification synthesis.

   Abstract

   Formal modeling provides strong guarantees about system correctness, but developing and repairing formal models remains labor-intensive and requires substantial expertise in logic and formal reasoning. Recent LLM-based autoformalization agents seek to reduce this burden by generating candidate formal models and revising them using feedback from formal tools. However, the existing approaches follow a generate-and-repair paradigm, in which repairs are driven by verification failures of the generated model and therefore depend heavily on both the granularity of the feedback and the LLM's repair capability. As a consequence, a repair targeting one level of verification may invalidate properties at another level, which requires reasoning over the complete set of event guards. To address these limitations, we propose Proof-Sketch-Guided Formal Model Synthesis (ProGS), an autoformalization method centered on model-based proof sketches. A model-based proof sketch represents the proof structure of the target formal system as a tree. Internal nodes capture case splits and inductive reasoning steps, while leaf nodes correspond to concrete state-transition events that realize individual subgoals. ProGS uses LLMs to generate and repair these sketches, with verification failures mapped back to specific nodes and subtrees to provide structured guidance for iterative repair. Our evaluation on a benchmark of 27 formal systems shows that ProGS improves over state-of-the-art agentic formal modeling approaches in syntactic validity, deductive verifiability, and behavioral correctness, demonstrating the benefit of organizing formal model construction around hierarchical proof sketches.

   Source: arxiv.org/abs/2609.29870

9. Provided and requested services in the specification and design of services and service-oriented architectures

   Manfred Broy

   Software and Systems Modeling · published

   Develops a formal calculus for specifying and composing service-oriented system components in terms of their provided and requested services, addressing feedback cycles, error handling, and feature interaction in service-oriented architectures.

   Abstract

   In service-oriented systems and service-oriented architectures (SOA), system components offer services and request services. Well-known examples of this paradigm are layered architectures where each layer provides services to its layer above and requests services from its layer below. This concept is generalized and extended to SOA designed in terms of the flow of services between the system components. We end up with the generalization of the concept of layered architectures where service components are composed in terms of their provided and requested services. Key aspects are service access protocols, which define the rules for getting access to a service. Service-oriented systems and SOA are graphically represented by service flow diagrams. A general approach to the formal specification and concurrent composition of service-oriented system component specifications is worked out based on a formal system model capturing services, service-oriented components, and SOA. We treat, in particular, formally the situation where concurrent composition of components and their services leads to feedback cycles in architectures. Typically, if in a SOA for some components their services are error prone, the system works properly at least until some error occurs. To handle such cases, the calculus is extended to specific rules for input assumptions which identify erroneous situations. Moreover, we study feature interactions between families of services offered by service components as well as the refinement and refactoring of services and service architectures.

   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: doi.org/10.1007/s10270-026-01429-y · doi:10.1007/s10270-026-01429-y

10. A model for integrating regulatory requirements into continuous software delivery in financial organizations

    Irina Titova

    American Impact Review · published

    Develops a classification and measurement model for systematically integrating financial-sector regulatory requirements (DORA, FFIEC guidance, NYDFS cybersecurity rules, and others) into continuous software delivery pipelines to support demonstrable compliance.

    Abstract

    Continuous software delivery requires financial organizations to reconcile frequent changes with regulatory controls. This study develops a model for systematically integrating regulatory requirements into delivery processes to support demonstrable compliance while accounting for delivery-time constraints. The methods combine comparative analysis of published US and European Union regulatory and supervisory documents, analysis of published research, and structural-functional modeling. Sources include the Digital Operational Resilience Act, Commission Delegated Regulation 2024/1774, Federal Financial Institutions Examination Council guidance, and New York State Department of Financial Services cybersecurity requirements. The proposed classification distinguishes the stage at which an action must be completed, the control object, and the status of its source. The methodological contribution connects this classification with rules for translating and measuring controls: applicability, fulfillment, and evidence sufficiency are assessed separately, while the measurement unit follows the control object and frequency. A release-approval comparison identifies evidence that can be shared across sources and assessments that must remain separate. Analysis of software packages, test data, and release approval establishes sequencing constraints and conditions for evidence reuse. Normal and emergency routes are differentiated through prerequisites and follow-up actions. The proposed metrics cover delivery speed and stability, control fulfillment, evidence completeness, and time spent on controls. The result is a theoretical and methodological model supported by analytical reasoning; implementation effects were not measured.

    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: doi.org/10.66308/air.e2026079 · doi:10.66308/air.e2026079