Specification Engineering: Foundations for the Future of Software Development

The seminar consisted of (1) several invited, “anchoring” talks around the four major topics listed above, (2) a series of shorter, “lightning” talks where participants shared new ideas, open problems, or ongoing projects on the topic of specification, and (3) two sets of breakout discussions. The first set of breakouts was assigned based on the four topics; after the initial discussions, the participants were encouraged to suggest or form different groups based on their topics of interest that emerged. The resulting second set of breakouts were centered around the topic of AI, covering LLMs for specification activities, specification of LLMs, and the use of AI for domain modeling. These activities were interleaved with ad-hoc discussions around the very concept of “specification” itself as well as planning for post-seminar activities and collaborations.

Among many stimulating discussions around the topic of specification, two major themes emerged. First, the participants realized that the very idea of “specification” may not be as well-defined or agreed upon as many had previously thought before the seminar. For example, to some participants, a specification had a specific meaning as a type of artifact that describes the expected behavior of a program or a system (e.g., API contracts), while others thought that nearly every software artifact (e.g., code) could be considered a specification. After a seminar-wide discussion, the participants agreed that it would be more meaningful to talk about properties of a specification (e.g., whether it is formal or informal, readable, analyzable, modifiable, for what purpose it is used, etc.,) rather than attempting to define what a specification is (and is not).

Second, many participants agreed that specifications will have an essential role in the age of AI-driven development and provide new opportunities for research as well as engagement with practitioners. For example, natural language prompts are emerging as a common mechanism to specify developers’ intent and system requirements, from which an implementation is automatically generated. However, it was also noted that informal, unstructured prompts are not an ideal specification mechanism for developing, debugging, and maintaining complex software systems, and that more structured specification methods are needed to support both developers and AI agents in these tasks. On the other hand, the participants also agreed that traditional specification methods and tools developed by the research community will likely need to be adapted or rethought to support the fuzzy, interactive, and informal ways in which developers collaborate with AI to develop software.

The management of specifications at scale requires systematic coordination across multiple models written in multiple modeling languages and notations, each with its own semantics and interpretations. Our work focuses on the foundations of model-based software engineering, in particular the semantics of models and the construction of software tools that support precise, analyzable model representations. A central research question is how to formally relate heterogeneous models so that their structures, behavioral properties, and interdependencies remain coherent across levels of abstraction and domains. This includes investigating how symbols of various kinds defined in one model can be connected to in other models to lay the foundation for a robust and maintainable specification management. We want to apply these foundational principles for human-constructed models, but also derived models and potentially AI-generated artifacts, aiming to enable robustly shared syntactically connected models that support automated reasoning, collaborative design, and scalable model evolution. This direction to our belief is a core pillar for a unifying semantic basis for specification engineering in increasingly complex, heterogeneous system engineering environments, where even UML and SysML only cover a partial subset of viewpoints and are internally also not well integrated yet.

Formal specifications play an increasingly important role in enabling the adoption of formal methods and automated reasoning in industrial settings, yet the process of deriving them from natural-language requirements remains poorly understood. Current approaches to specification generation often treat it as a translation problem, assuming that requirements encode the information needed for formalization. We question this assumption, particularly in the context of rapid, iterative Systems Engineering and the growing interest in applying generative AI to support these processes.

In this talk, we presented preliminary results from studying the generation of formal specifications as a design transformation process characterized by a gradual reduction of epistemic uncertainty. We took two complementary perspectives. First, we studied the cognitive processes applied by humans to transform informal requirements into increasingly formal design artifacts. Second, we evaluated whether agentic generative AI systems could perform similar transformations with comparable epistemic rigor.

To structure this analysis, we used Gero’s Function–Behavior–Structure (F-S-B) ontology as a model of the design process and its successive refinements. Using this concept, we carried out an empirical study on a design challenge that involved exploring a large design space with the goal of generating adaptable search-and-rescue drones. We tasked human participants and different configurations of agentic generative AI systems with the same objectives and constraints.

Our findings indicated that while agentic LLM systems could generate syntactically well-formed artifacts, they struggle with context preservation, controlled abstraction, and uncertainty management. Common failure modes included premature concretization, cascading semantic errors, and ontology drift, resulting in artifacts that resemble specifications without supporting their intended epistemic role (“specifictions”). In contrast, human designers rely on implicit contextual knowledge and iterative reformulation to progressively stabilize meaning before formalization.

We conclude that generating formal specifications cannot be reliably delegated to autonomous agents without well-defined mechanisms for transparent uncertainty management, contextual grounding, and human oversight. These results suggest that future AI-assisted approaches to specification engineering should emphasize not only automation but also support the human users’ ability to steer the formalization process.

Modern software-based systems operate under rapidly changing conditions and face ever-increasing uncertainty. In response, systems are increasingly adaptive and reliant on artificial-intelligence methods. In addition to the ubiquity of software with respect to users and application areas (e.g., transportation, smart grids, medicine, etc.), these high-impact software systems necessarily draw from many disciplines for foundational principles, domain expertise, and workflows. Recent progress with lowering the barrier to entry for coding has led to a broader community of developers, who are not necessarily software engineers. As such, the field of software engineering needs to adapt accordingly and offer new methods to systematically develop high-quality software systems by a broad range of experts and non-experts. In [1], we look at these new challenges and propose to address them through the lens of Abstraction. Abstraction is already used across many disciplines involved in software development – from the time-honored classical deductive reasoning and formal modeling to the inductive reasoning employed by modern data science. The software engineering of the future requires Abstraction Engineering – a systematic approach to abstraction across the inductive and deductive spaces. We discuss the foundations of Abstraction Engineering, identify key challenges, highlight the research questions that help address these challenges, and create a roadmap for future research.

This breakout tackled fundamental definitional questions about specifications in the age of AI. They built on a list of essential properties of specifications that the entire seminar group came up with during an earlier discussion: adequacy to the problem, including: formality, readability, modifiability, precision, incrementality, comprehensibility, decomposability, and fitness to use case. The breakout group compared three development paradigms across multiple dimensions of properties: vibe coding (where the specification is the history of prompts and feedback iterated until user acceptance), specifications for correctness of AI components (assuming we cannot fully specify behavior, using lists of examples and accepting black-boxes as valid components), and traditional code contracts (formal, complete specifications like sorting algorithm contracts with precise logical properties). An outcome of this exercise was that specifications remain fundamentally about abstraction, communication, and intent – but the forms they take and the guarantees they provide may need to evolve in the AI era.

This group addressed the dual challenge of specifying AI systems themselves and using AI to assist with specification tasks. For specifying AI, key problems included handling the inherent uncertainty in task definitions, understanding what constitutes a “bug” in AI systems, managing the distance between problem space (context, users) and embedding space, and dealing with AI’s fundamentally different characteristics – built for vague problems, subject to novel attacks, operating in large state spaces that are hard to explore systematically. The group distinguished between approaches for small language models (built for single tasks, easier to specify and potentially verify) versus large language models, and discussed the gap between task-specific verification and the multi-task, multi-modal nature of modern AI systems.

For AI-assisted specification, the group explored how LLMs could help translate high-level intent to lower-level behavioral specifications, convert natural language to temporal logic, and translate between specification languages. Promising approaches included neuro-symbolic solutions, constraint-guided generation, tools like Amazon’s Kiro for conversational specification elicitation, and the concept of LLMs as judges for tasks without conventional oracles. However, fundamental questions remain about the role of humans in AI-assisted specification engineering, establishing notions of correctness (full versus partial, with or without certificates), handling the challenges of “vibe coding” where huge pull requests lead to knowledge loss, and managing the lifecycle from specification through manual code customization. The group emphasized the need for systematic frameworks, better traceability between high-level features and code artifacts, and principled approaches to collaboration between humans and AI in the specification process.

This breakout explored usability in the context of formal specification languages, tools, and methods through the lenses of established HCI frameworks such as ISO 9241 and Nielsen’s usability criteria. Participants emphasized that usability spans learnability, efficiency, effectiveness, and user satisfaction, while user experience further encompasses emotional, aesthetic, and value-driven dimensions. A recurring theme was that specification work is a creative, cognitively demanding activity involving diverse users – domain experts, programmers, students, formal methods specialists – each with different needs and expectations. As a result, understanding usability requires identifying the tasks users perform (e.g., expressing properties, validating interpretations, refactoring expressions, checking consistency) and studying how tools can support these tasks.

The group identified research gaps in generalizing usability studies, understanding trade-offs inherent in designing notation, and supporting mental-model alignment through visualization, navigation, and incremental interaction. Existing frameworks – such as the cognitive dimensions of notations, the “physics of notations,” and studies on programmer usability – offer valuable foundations but do not yet address the full complexity of specifying, debugging, or evolving formal models. Promising directions include supporting transformation and refactoring workflows, leveraging domain-specific or embedded DSLs to reduce cognitive distance for domain experts, and building persuasive interfaces that gently guide users toward sound practices. Participants also highlighted the need for benchmarks and representative tasks to systematically evaluate usability in specification contexts.

The breakout on Quality and Validation examined what it means for a specification to be “high-quality” and how one can systematically validate it. Participants noted that the field lacks shared definitions for quality attributes of specifications – attributes that range from those expressible purely in formal terms to those that also depend on informal understanding of the domain. Validation was characterized as ensuring correspondence between formal models and the real world or stakeholders’ mental models, encompassing accuracy, completeness, and generality. The group emphasized that, although examples exist (e.g., testing formal models, scenario or predicate generation, Zave and Jackson’s “turnstile” work), these methods have not sufficiently raised awareness of validation’s importance or made validation accessible across domains.

The group discussed several barriers to adoption: validation is under-taught, often domain-specific, and many engineers undervalue domain modeling. Physics-based disciplines offer instructive analogies where domain constraints assist validation within error bounds, but formal specification practice rarely incorporates similar reusable frameworks. Looking ahead, the group identified machine learning and large language models (LLMs) as both a challenge and an opportunity. As tools increasingly use AI to generate, analyze, or validate specifications, the community must develop ways to validate the outputs of such tools – and potentially use LLMs themselves as aids for scenario generation, explanation, and model exploration. This, they argued, presents a strategic opening to reassert the importance of validation in the broader software engineering ecosystem.

This breakout explored how large language models can support the creation, transformation, and understanding of specifications. The group developed a taxonomy of LLM uses – ranging from generating and translating specification artifacts, to refining and repairing them, to assisting with semantic comparison and cross-validation. LLM strengths lie especially in bridging informal and formal representations, offering multiple interpretations of ambiguous requirements, and generating explanations that help humans understand complex artifacts. The group noted that LLMs may accelerate tasks such as formalizing requirements, migrating between specification languages, producing test cases, and supporting exploratory design-space analysis.

At the same time, participants emphasized that LLMs must be used within a carefully designed human–AI workflow. Humans remain essential for comprehension, validation, and selection among alternative candidates. Concerns included dependence on input quality (with code often yielding better results than natural language), sensitivity to bias when both code and specifications are generated by the same model, and the need for diversity across LLM sources to enable cross-checking. The group strongly rejected the idea of using LLMs for verification itself, instead positioning them as generators, explainers, and collaborators rather than judges. Open questions remain about whether traditional specifications are still needed in an era of “vibe-coding,” how to effectively validate and select between LLM-generated alternatives, and optimal approaches for ensuring specification diversity while avoiding algorithmic bias.

This group tackled the fundamental challenge of constructing large, complex specifications from smaller components, examining issues of composition both within single formalisms and across heterogeneous languages and logics. Key problems included how to assemble proofs about different system elements into coherent whole-system arguments, how to facilitate specification reuse across systems and abstraction levels, and how to support incremental, modular changes while managing proof maintenance effort. The group also addressed methodological questions around distributing specification construction across engineering teams and developing specification product lines.

Critical scalability concerns extended beyond mere size to include verification time, incremental analysis capabilities, and the challenge of maintaining formal arguments as specifications evolve. The group discussed several technical approaches including contract-based decomposition, component-based architectures with information hiding (such as AADL with local component proofs), and the use of equivalence relations between abstraction levels. A recurring theme was the tension between code-level proofs of individual components and higher-level API abstractions, particularly when implementations may not perfectly refine their specifications, raising questions about how to compose partial correctness guarantees into system-level assurance arguments.

This focused group examined the critical but often neglected practice of domain modeling, distinguishing sharply between productive and counterproductive uses of LLMs in this space. The group identified a “bad idea” – encouraging non-experts to do domain modeling with LLM assistance, since non-experts cannot properly evaluate LLM outputs – and a “good idea” – domain experts using LLMs as collaborative tools to help create quality domain models. For experts, LLMs can write domain models in natural or formal languages, answer validation questions, help get started, encourage continuation, and stimulate thinking. The group illustrated their approach with a practical example of validating assumptions in safety-critical systems, showing how LLMs can identify edge cases and failure scenarios that experts might overlook.

Three key research directions emerged: training data (determining whether to use large public models or small specialized ones, whether to restrict training to authoritative or proprietary data, and whether including diverse sources like science fiction might be valuable), prompt engineering (teaching experts to write well-structured domain models and validate them successfully, recognizing that prompt size and quality are crucial, and devising methods that guide experts through appropriate steps while encouraging independent critical thinking), and “meta-prompt-engineering” (asking the LLM how to write good prompts for domain modeling tasks). The emphasis throughout was on LLMs as tools to augment expert judgment rather than replace it.

Due to the advent of small language models (SLMs) especially for agentic artificial intelligence (AI), we suggest a challenge to verify a realistic foundation model (or large language model [LLM]) like ChatGPT. Could we verify ChatGPT, what would we verify, and how could we do it? We review recent results in neural network verification and recent scalability as demonstrated in the Verification of Neural Networks Competition (VNN-COMP), along with the limitations and usefulness of these approaches, detailed more in [1]. The neural network verification problem is given a trained neural network and a specification often formalized as preconditions and postconditions represented by sets in the input and output spaces of the neural network – prove the network satisfies the specification, and amounts to showing the neural network maps any element of the precondition into the postcondition. More realistically, we suggest trying to verify a fully open SLM like Ai2’s OLMo2 series (open code, data, weights, etc.) like OLMo2 1B, and this guiding grand challenge to verify an SLM (or LLM) will illustrate areas of need in formal methods for specification and verification of transformer architecture models.