Paper deep dive

Feedback-based Automated Verification in Vibe Coding of CAS Adaptation Built on Constraint Logic

Michal Töpfer, František Plášil, Tomáš Bureš, Petr Hnětynka

Year: 2026Venue: arXiv preprintArea: cs.AIType: PreprintEmbeddings: 63

Intelligence

Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 91%

Last extracted: 7/20/2026, 9:42:25 PM

Summary

This paper proposes a method for generating Adaptation Managers (AM) for Collective Adaptive Systems (CAS) using 'vibe coding' with Large Language Models (LLMs). The approach combines iterative LLM code generation with runtime verification using a novel temporal logic called Functional Constraints Logic (FCL). FCL allows for precise specification of functional and generic constraints on system traces. The system uses feedback loops where constraint violations detected during runtime verification are reported back to the LLM to refine the generated AM code, achieving high correctness with few iterations.

Entities (8)

Adaptation Manager · software-component · 98%Functional Constraints Logic · formal-logic · 97%Vibe-Coding · methodology · 95%Constraint Verifier · software-component · 93%Collective Adaptive Systems · system-type · 92%Dragon Hunt · case-study · 90%ADSL · domain-specific-language · 88%FCDSL · domain-specific-language · 88%

Relation Signals (6)

Vibe-Coding → uses → Large Language Models

confidence 95% · With the advances of generative LLMs, generating AM code based on system specification... is a tempting opportunity. The recent introduction of vibe coding suggests a way to target the problem... by iterative testing and vibe coding feedback loops

Functional Constraints Logic → isusedfor → Runtime Verification

confidence 94% · Furthermore, we show that by combining the adaptation and vibe coding feedback loops where the FCL constraints are evaluated for the current system state, we achieved good results

Adaptation Manager → isgeneratedby → Vibe-Coding

confidence 92% · In this paper, we show that generating an AM via vibe coding feedback loops is a viable option

Vibe-Coding → providesfeedbackvia → Constraint Violation Report

confidence 91% · If any constraints are violated, they are adequately recorded in the constraint violation report... the feedback loop is activated... The constraint violation report is made a part of the new prompt

Constraint Verifier → verifies → Functional Constraints Logic

confidence 90% · The constraint verifier that checks whether predefined constraints are not violated... Functional constraints are described in more detail in Sec. III-C and Sec. IV.

Dragon Hunt → isexampleof → Collective Adaptive Systems

confidence 85% · As a running example, we use a simple made-up “Dragon Hunt” game... To model the running example as a CAS, we employ an ensemble-based software architecture

Cypher Suggestions (0)

No Cypher suggestions yet.

Abstract

Abstract:In CAS adaptation, a challenge is to define the dynamic architecture of the system and changes in its behavior. Implementation-wise, this is projected into an adaptation mechanism, typically realized as an Adaptation Manager (AM). With the advances of generative LLMs, generating AM code based on system specification and desired AM behavior (partially in natural language) is a tempting opportunity. The recent introduction of vibe coding suggests a way to target the problem of the correctness of generated code by iterative testing and vibe coding feedback loops instead of direct code inspection. In this paper, we show that generating an AM via vibe coding feedback loops is a viable option when the verification of the generated AM is based on a very precise formulation of the functional requirements. We specify these as constraints in a novel temporal logic FCL that allows us to express the behavior of traces with much finer granularity than classical LTL enables. Furthermore, we show that by combining the adaptation and vibe coding feedback loops where the FCL constraints are evaluated for the current system state, we achieved good results in the experiments with generating AMs for two example systems from the CAS domain. Typically, just a few feedback loop iterations were necessary, each feeding the LLM with reports describing detailed violations of the constraints. This AM testing was combined with high run path coverage achieved by different initial settings.

PDF

Open source PDF →Open local PDF →

Trouble viewing inline? Open PDF directly →

Full Text

61,478 characters extracted from source content.

Expand or collapse full text

Feedback-based Automated Verification in Vibe Coding of CAS Adaptation Built on Constraint Logic Michal Töpfer, František Plášil, Tomáš Bureš, Petr Hn ˇ etynka Charles University, Czech Republic Email: michal.topfer, frantisek.plasil, tomas.bures, petr.hnetynka@matfyz.cuni.cz Abstract—In CAS adaptation, a challenge is to define the dynamic architecture of the system and changes in its behavior. Implementation-wise, this is projected into an adaptation mecha- nism, typically realized as an Adaptation Manager (AM). With the advances of generative LLMs, generating AM code based on system specification and desired AM behavior (partially in natural language) is a tempting opportunity. The recent introduction of vibe coding suggests a way to target the problem of the correctness of generated code by iterative testing and vibe coding feedback loops instead of direct code inspection. In this paper, we show that generating an AM via vibe coding feedback loops is a viable option when the verification of the generated AM is based on a very precise formulation of the functional requirements. We specify these as constraints in a novel temporal logic FCL that allows us to express the behavior of traces with much finer granularity than classical LTL enables. Furthermore, we show that by combining the adaptation and vibe coding feedback loops where the FCL constraints are evaluated for the current system state, we achieved good results in the experiments with generating AMs for two example systems from the CAS domain. Typically, just a few feedback loop iterations were necessary, each feeding the LLM with reports describing detailed violations of the constraints. This AM testing was combined with high run path coverage achieved by different initial settings. Index Terms—Adaptive systems, Large language models, Soft- ware architecture, Collective adaptive systems, Vibe coding, Runtime verification, Temporal logic I. INTRODUCTION Collective Adaptive Systems (CAS) feature cooperating entities (frequently called agents) collaborating in groups (ensembles) towards a common goal. As the name suggests, adaptation is an integral feature of CAS. Adaptation concerns the dynamic presence of agents, their flexible grouping, and emerging changes in the environment. This inherently means dynamic modification and adaptation of the system architecture. Obviously, a challenge is to define the dynamic system architecture and changes in the behavior of the system. To this end, [1] provides an overview of a number of different approaches covering, e.g., goal-oriented design, adaptation feedback loops, logic-based modeling and analysis, and at- tribute and aggregate programming techniques. Overall, CAS adaptation is a challenging task where the particular domain can play a substantial role so that its realization has to reflect the application specifics. Implementation-wise, this has to be projected in the adaptation mechanism (typically realized as a software block Adaptation Manager – AM later on). With the advances of generative LLMs and the vision of employing generative AI in software architecture [2], the option to generate code based on providing a prompt containing the system specification (even partially in natural language) is a tempting opportunity for generating an AM. As for every code generated this way, the correctness of the result is a key issue, so human code inspection originally appeared as a necessity. For example, [3] reports underwhelming results when experimenting with generation of AM code per se, i.e., without any feedback to LLM. Nevertheless, the recent introduction of vibe coding suggests a way around the problem (a comprehensive survey is, e.g., in [4]). Instead of direct code inspection, vibe coding proposes its checking in iterative feedback loops and asking the LLM for its improvement by prompt adjustments. Such prompt modification may potentially include human interventions as well (for instance, to enhance/correct the system specification). Code checking can be based on a wide range of methods [4]; for example, in [5] it ranges from handling compilation errors, running predefined tests, static analysis, employing LLM- generated tests, to injecting flaws into the code to assess the quality of the tests. In this paper, we aim at targeting the challenge of to which extent to combine a formal way of system specification and its description in a natural language to achieve a viable result in vibe coding an AM. Instead of considering the whole spectrum of code assess- ment methods, we further particularly focus on testing the AM code for violation of a set of architectural constraints. These include generic constraints that ensure compliance with general architectural rules (e.g., each component is assigned to exactly one ensemble, i.e., a collaborating group of components), and functional constraints that ensure that each architectural adaptation step will preserve the desired functionality of the particular application. We propose an adaptation specification in a DSL that combines a description of the high-level adaptation strategy in natural language and a formalization of the detailed constraints that the AM should follow and comply with. To this end, we designed and formalized a novel temporal logic – Functional Constraints Logic (FCL), allowing the definition of adaptation steps’ constraints in both a detailed and an easy-to- reflect-in-DSL way. In this context, we focus on the following research questions. RQ1:How to automatically guide generative AI in designing and implementing CAS adaptation as an AM based on arXiv:2602.18607v1 [cs.AI] 20 Feb 2026 system specification via vibe coding? RQ2:How to ensure that vibe coding produces AM yielding valid adaptations (i.e., conforming to the generic and functional constraints)? RQ3:How efficient is the method of combining the vibe coding feedback loop and the adaptation loop? The contributions of this paper include •design of a DSL for specifying the system and its architecture (ADSL), •design of a novel temporal logic FCL as a base for the specification of functional constraints in a dedicated DSL (FCDSL), • a tool for runtime verification of an AM, including evaluation of the functional constraints, •an experimentation framework for generating LLM prompts from architectural specification, querying the LLMs via an API, and providing feedback to the LLM based on runtime verification, • evaluation on two example cases. The implementation of the framework, experimental setup, and raw results are available in the replication package 1 . The structure of the paper is as follows. In Sec. I, we introduce the running example and show how to model it as CAS. Sec. I describes the approach of combining vibe coding with runtime verification feedback to implement an AM, while Sec. IV gives more details on FCL and defining functional constraints. In Sec. V, we evaluate our approach and provide the results of the experiments. Sec. VI discusses related work and Sec. VII concludes the paper. I. BACKGROUND AND RUNNING EXAMPLE A. Running example As a running example, we use a simple made-up “Dragon Hunt” game, adopted from [3]. This example is intentionally fictional, so that the LLM could not have been trained on its exact rules. A Dragon lives in a Cave near a Village. The goal of the game is to kill the Dragon. The player of the game can control the villagers by assigning them tasks (in each of his/her turns). Villagers can either stay in the Village and produce wheat, that allows them to spawn more villagers, or move to the Cave to attack the Dragon. The Dragon attacks back, possibly killing some of the villagers. There is a limit of 30 turns (steps), after which the player loses if the Dragon remains alive. The rules of the game define what tasks can be assigned to the villagers. Villagers in the Village can 1) farm (produce wheat), 2) spawn a new villager, 3) go to the Cave. Villagers in the Cave can 1) attack the Dragon, 2) stay idle in the Cave, 3) go back to the Village. There are two roles of villagers in the game: farmers (more efficient at farming wheat) and warriors (capable of more damage to the Dragon). 1 https://github.com/smartarch/llm-adaptation/tree/icsa B. Modeling the running example as a CAS To model the running example as a CAS, we employ an ensemble-based software architecture based on the concepts from the DEECo model [6], [7]. The villages are the components of the system. Each component has several attributes representing the component’s state (location, health points, role, etc.). Furthermore, there are beyond-control components that cannot be controlled by the AM, but their attributes can be observed, such as the current amount of wheat in a silo in the Village. The system is adapted in discrete time steps (turns of the game). In each step, the AM performs ensemble resolution – it divides the components into groups (called ensembles). This updates the architecture of the system (the composition of components) and assigns tasks to components. For example, all the components assigned to the ensembleFarmwill work on the farm to produce wheat. To make the assignment of tasks to components simpler, we require that during ensemble resolution each component is assigned to exactly one ensemble. The rules of the game also constrain the architecture, e.g., only the components located in the Village can be assigned to the Farm ensemble. From a broader perspective, the division of components into ensembles is an instance of the grouping problem, being NP-hard in general [8]. Therefore, a viable way around such complexity is to find a suitable heuristic – an opportunity to ask LLM to propose one and find a way to check that what it does propose meets the specification of the problem in question. From the perspective of the MAPE-K loop [9] commonly used as a model of the adaptation process, the AM observes the state of the system (Monitor), decides on the ensemble res- olution (Analyze + Plan), and assigns tasks to the components based on their membership in a particular ensemble (Execute). I. VIBE CODING AND FEEDBACK VERIFICATION A. Combining adaptation and feedback loops To answer RQ1, we propose combining vibe coding with an automated feedback loop to the LLM based on the results of runtime verification done as part of the adaptation loop. It consists of two main stages executed in these loops: 1) Prompting an LLM to generate the code of the AM (Sec. I-B), 2)Runtime verification of the generated AM (Sec.I-C) that potentially yields feedback to code generation. This idea is graphically expressed in Fig. 1 and is further elaborated in this section. At design time, the architect specifies the goals of the system and constraints on the desired architecture of the components and ensembles and their state. From this specification, a prompt is automatically generated (“1.” in Fig. 1) and presented to the LLM. The task of the LLM is to design and implement an AM for the system – it should output it as a block of Python code (“2.”). The system is run, and the generated AM periodically adapts the system architecture (red loop in Fig. 1): It reads the Initial state Initial state 3. Domain description Architecture specification (in ADSL) I. monitor system state Managed system Prompt AM code generation I. propose architecture update Adaptation manager (AM) 2. LLM Run-time verification Constraints (in FCDSL) 5. retry Prompt generation 1. I. execute architecture update Constraint verifier 4. constraint violation Constraint violations report state Initial state Fig. 1: Combining adaptation and feedback loops. monitored system state (“I.”) and proposes an update to the system architecture (“I.”). The architecture update is executed on the system (“I.”) and the system runs until the next adaptation (“I.” again). At the same time, run-time verification of the functionality of AM takes place (“3.”). Its important part is the constraint verifier that checks whether predefined constraints are not violated, in particular: • Generic constraints ensure that the AM code complies with key specification requirements imposed for the adapta- tion loop environment, and that the proposed architecture updates meet the generic rules of the component and ensemble cooperation. More details on these constraints are given in Sec. I-C. •Functional constraints ensure that the AM follows the adaptation strategy specified in ADLS (Listing 2). These constraints are described in more detail in Sec.I-Cand Sec. IV. If any constraints are violated, they are adequately recorded in the constraint violation report (“4.”), the system run is stopped and the feedback loop is activated – black loop in Fig. 1. In particular, the LLM is asked to generate the AM again to fix these violations (“5.”). The constraint violation report is made a part of the new prompt (the original prompt and the LLM response are kept in the context). This closes the feedback loop. The updated AM is again verified and the loop is repeated until an AM passing all the constraints is generated (a safety mechanism can also be employed to stop the feedback loop after a predefined number of unsuccessful iterations). B. Prompt generation The prompt to the LLM is automatically generated from a domain description (Sec.I-B1) and an architecture specifi- cation (in the domain specific language ADSL; Sec.I-B2). Sec. I-B3 overviews how the prompt is generated. 1) Domain description: The domain description defines the system scenario in natural language. It describes the rules of the system, specifies its entities, behavior requirements, etc. Domain description of the running example is illustrated in Listing 1. Listing 1: Domain description for the Dragon Hunt. You play a computer game. The goal is to kill a Dragon as fast as possible. The Dragon lives in a Cave near a Village. The player controls villagers. The villagers can either be in the Village and work on a farm (and produce wheat) or they can go to the Cave, where they can attack the Dragon. There are two types of villagers − farmers and warriors. Farmers produce more wheat when they work on a farm, and warriors deal more damage to the Dragon. Farmers start with 4 HP, produce 5 wheat when farming, and deal 1 damage when attacking. Warriors start with 6 HP, produce 2 wheat when farming, and deal 3 damage when attacking. To spawn a new villager, at least two villagers must be in the "spawn" group and some wheat is consumed (12 for warriors, 10 for farmers). When the Dragon is attacked, it can attack back. With 40% probability, it will cause 1 damage to every villager in the Cave, and with 20% probability, it will eat one random villager in the Cave. Dead villagers are removed from the game. If all the villagers die, you lose the game. The Dragon starts with 50 HP and you win the game when it dies. If you don’t kill the Dragon within 30 steps, you lose the game. 2) Architecture specification: The architecture specification serves to formally define the components and ensembles in the system, the architecture of the system (permitted assignments of components into ensembles – ensemble resolution), and to express the desired adaptation strategy in ensemble resolution. It is written in ADSL that mixes formal constructs and natural language formulation snippets, as highlighted by color coding in Listing 2: BLUE denotes keywords, BLACK identifiers and expressions, and GREEN natural language snippets. Listing 2: Dragon Hunt architecture specification in ADSL (a fragment). # component definitions component Dragon attribute hp name "Health" component Villager name name attribute role name "role" description "’Farmer’ or ’Warrior’" ... # ensemble definitions ensemble Farm name "farm" description "Stay in the Village and work on the farm" ensemble GoToCave name "cave" description: "Go to the Cave" ... # observable−only environment state beyond−control Dragon dragon "The Dragon" ... # ensemble resolution periodically assign Villager[] "Villagers in the Village" if location == ’Village’ into ensembles Farm, GoToCave, ... as assign_in_village periodically assign Villager[] "Villagers in the Cave" if location == ’Cave’ into ensembles ... as assign_in_cave strategy: "All Warriors should go to the Cave, and then attack the Dragon. All Farmers should stay in Village and farm or spawn new villagers (both Farmers and Warriors are necessary)." # adaptation manager interface am_interface SmartAdaptation(dragon.DragonHuntAdaptation) 3) Prompt content: An example of a generated prompt is shown in Listing 3, where the VIOLET text indicates the information obtained from the ADSL architecture specification and the domain description, and the BLACK text is part of the template used to generate the prompt. The prompt starts with the domain description that includes the overall goal of the system. Next, the LLM task is articulated: Design and implement an adaptation manager that assigns components to groups 2 . The generic constraint that assigned to exactly one group” is explicitly mentioned. For the generated AM to be practically useful by being plugged into the system, technical requirements are mentioned, such as implementing the AM in Python and deriving it from a given abstract class. The abstract class is automatically generated from the ensemble assignment definitions (one method per assignment) specified in the ADSL. Then, more details on each ensemble assignment are given. The available ensembles with their descriptions are listed to provide the LLM with the possible tasks for the components. We also instruct the LLM on what attributes of the compo- nents are relevant to the adaptation and how to access them (via their identifier). As this prompt is generated at design time, it is not possible to include the attribute values for the components, so we rather instruct the LLM on how these values can be obtained in the generated AM. In a similar vein, beyond-control components and their attributes are listed after the ensemble assignments. Lastly, the desired strategy that the generated AM follows and a list of functional constraints (termed “requirements” in the prompt) is included in the prompt. Functional constraints are expressed in natural language; their formal specification in FCL is then used for verification (Sec. I-C). Listing 3: Example of a generated prompt. You play a computer game. ... If you don’t kill the Dragon within 30 steps, you lose the game. Suggest an adaptation manager. The goal is to assign the components into groups. Note that each component must be assigned to exactly one group. If a component is supposed to remain in the same group (continue performing the same action), it must always be explicitly re−assigned to that group. The adaptation manager must be written in Python and it must be a class named `SmartAdaptation` derived from this base class (can be imported from `dragon`): 2 In the prompts, we use the term “group” instead of “ensemble”, assuming this is less ambiguous for the LLM. ``` class DragonHuntAdaptation(abc.ABC): @abc.abstractmethod def assign_in_village(self, components, environment, group_ids, step): pass @abc.abstractmethod def assign_in_cave(self, components, environment, group_ids, step): pass ``` To perform the group assignments, use the ` environment.assign_group(component, group_id)` method. The ` group_id` must be exactly as listed below. − In `assign_in_village`, your goal is to divide the Villagers in the Village (`components`) into the following groups: − A group named "farm": Stay in the Village and work on the farm − A group named "cave": Go to the Cave − A group named "spawn farmer": For every two villagers assigned to this group and 10 wheat, a new Farmer is spawned. − A group named "spawn warrior": For every two villagers assigned to this group and 12 wheat, a new Warrior is spawned. The `group_ids` argument is a list of all valid group names. For each component, the following attributes are available (note that the attributes are read−only and they do not update when a component is assigned to a group): − `role`: Role (’Farmer’ or ’Warrior’) − `hp`: Health − In `assign_in_cave`, your goal is to divide the Villagers in the Cave (`components`) into the following groups: − A group named "attack": Attack the Dragon − A group named "cave": Stay in the Cave − A group named "village": Go to the Village The `group_ids` argument is a list of all valid group names. For each component, the following attributes are available (note that the attributes are read−only and they do not update when a component is assigned to a group): − `role`: Role (’Farmer’ or ’Warrior’) − `hp`: Health − Further, you can access the following beyond−control components, which are only observable and cannot be assigned to groups. The Dragon (accessible via `environment.dragon`) with the following attributes (note that the attributes are read−only and they do not update when a component is assigned to a group): − `hp`: Health The Farm (accessible via `environment.farm`) with the following attributes (note that the attributes are read−only and they do not update when a component is assigned to a group): − `wheat`: Current wheat amount − All Warriors should go to the Cave, and then attack the Dragon. All Farmers should stay in the Village and farm or spawn new villagers (both Farmers and Warriors are necessary). The adaptation strategy must adhere to the following functional requirements: −The Dragon should be attacked at least once in the first 15 steps of the game. − All farmers should stay in the Village. Think step by step. First, reason about the task and analyze the problem. Then, describe the adaptation manager. After that, write the Python code for the adaptation manager. C. Verification of the AM in system runs Verification of the AM is performed by running a series of automated tests, each targeting the violation of a specific type of constraint. In our approach, a test consists of running the system (the adaptation loop) and checking that the trace corresponding to the system run complies with the constraints. In the running test, the Constraint Verifier (CV) checks each of the proposed architecture updates produced by the AM. If the CV detects a constraint violation, it records it in the constraint violation report. After all tests are completed, if there are any constraints violated, the feedback loop is activated, and the report is sent to the LLM. To achieve a better trace coverage in the verification (i.e., cover the behavior of AM in more possible system states), the tests are parameterized by initial states (Listing 4). Each executed test is thus a new run of the system starting from a given initial state (e.g., the Dragon Hunt game is played from “No Warriors” state (Listing 4)). Listing 4: Initial states for verification in Dragon Hunt (fragment) initial state "Farmers and Warriors" random_seed: 42 # to guarantee repeatable experiments farmer_count: 2 warrior_count: 1 initial state "No Warriors" random_seed: 123 farmer_count: 2 warrior_count: 0 The generic constraints (domain-independent) ensure that the produced AM and its current output (architecture up- date/ensemble resolution) are sound in accordance with the specification expressed in the prompt. This includes testing that • the LLM response includes a block of Python code which is executable and can be imported into the system (e.g., the AM class is named correctly and derived from the abstract base class specified in the prompt), • no exceptions have been thrown at runtime, •only the appropriate ensembles mentioned in the ar- chitecture specification are used, e.g., inassign_in_cave, the appropriate ensembles areAttack,StayInCave, and GoToVillage), • each component is assigned to exactly one ensemble. Furthermore, functional constraints (domain-specific) are checked to ensure that the assignment of components into ensembles corresponds to the strategy drawn by the architect in ADSL. Although the strategy (specified in natural language) is given to the LLM in the initial prompt, there is no guarantee that the LLM will follow it in the generated AM. The functional constraints thus allow one to formalize the requirements on the behavior of the AM, and check, in an automatized way, whether they are met. The functional constraints are specified in the Functional Constraints DSL (FCDSL), which combines formally express- ing the constraints in the temporal logic FCL and articulating their essence in natural language, as illustrated in Listing 5. The former serves as input to the CV, the latter as the base for forming an entry in the constraint violation report (feedback to the LLM). Details on FCL and examples of functional constraints in FCL are given in Sec. IV. Listing 5: Functional constraints specification for the Dragon Hunt (a fragment in FCDSL). constraint "The Dragon should be attacked at least once in the first 15 steps of the game." ♢ 1 15 |Attack|≥ 1 constraint "All farmers should stay in the village." Farmers =v ∈ Villagers | v.role = ‘Farmer’ ∀f ∈ Farmers :♢ MAX MAX f .location = ‘Village’ IV. FUNCTIONAL CONSTRAINTS LOGIC (FCL) As already stated in the previous sections, the system architect can specify the desired behavior of the adaptation manager produced by vibe coding. The strategy is written in natural language, and it is presented to the LLM when generating the AM. Although current LLMs are trained to follow instructions, there is no guarantee that the LLM will correctly interpret the strategy and implement the AM according to it. To this end, our approach includes functional constraints as a way to formalize the behavior of the AM. The constraints allow us to formally specify expectations on the behavior via logical formulas that should hold for the system. The syntax and semantics of Functional constraints logic (FCL) are described in Sec. IV-A and examples are given in Sec. IV-B. The functional constraints are used for runtime verification of the generated AM and providing feedback to vibe coding, as already described in Sec.I-C. To ensure that the generated AM follows the desired strategy, the functional constraints have to be aligned with the strategy (both are defined by the architect). Apart from the runtime verification, FCL could also be used to guide future adaptations of the system, which we discuss in Sec. V-E5. A. FCL syntax and semantics FCL is based on first-order temporal logic and is inspired by TLA+ [10] and [11]. We assume that the system runs in discrete time steps and allow for both finite and infinite traces. The core of FCL is the temporal operator (called within)♢ n t φ, expressing that the formulaφholds at leastntimes within the nextt > 0steps or at leastntimes in the previous−tsteps fort < 0. As to the relationship oft(time window) andn, we define the semantics of ♢ n t φ for n >|t| as false . When considering finite runs of the system (finite traces), a special valueMAXis used to denote the number of time steps from the current step to the end of the trace. Likewise, BEGdenotes the number of time steps from the beginning of the trace to the current step. Thus,BEGandMAXserve as endcounts, since their value is determined by the current time step. Apart from the temporal operator within, the standard logical operators (∧,∨,=⇒,¬), constantstrueandfalse, quantifiers (∀,∃), and sets with standard operations (similar to TLA+) are employed in FCL. Thus, considering a system composed of components and ensembles, its state is represented by sets updated in each adaptation step (FCL time step). For example, all instances of theVillagercomponent are available as members of the Villagersset. The set corresponding to an ensemble is updated in each adaptation step to contain the components assigned to the ensemble, e.g.,Farmis the set of all components assigned to theFarmensemble in the current adaptation step. The attributes of the components are accessed via the dot notation (similarly to Python). Working with finite traces requires handling the semantics of tandnwhen colliding with the window boundaries:♢ n t φfor t > MAX ∧ n≤ MAXbecomes semantically♢ n MAX φ (and similarly♢ n t φfort < 0,|t| > BEGandn≤ BEGbecomes semantically ♢ n BEG φ). As an aside, using the♢ n t operator andINFdenoting infinity, the common LTL operators can be expressed as follows: • next (φ holds in the next time step): ⃝φ≜♢ 1 1 φ, •future (φholds at least once in the future):♢φ≜♢ 1 INF φ, • globally (φ holds in each future step): □φ≜♢ INF INF φ By general, the semantics of within applied to the LTL until operator and the nesting of within can be inductively defined by the concept of horizon (basically the maximal time window for which a composed formula has to hold) as in [11]. Given the main focus of this text and its space constraints, we do not elaborate on such formal definitions further. B. Examples of functional constraints for Dragon Hunt in FCL In the examples below, the following sets represent the system’s components:Dragons,Villagers; and ensembles: Farm,GoToCave,SpawnFarmer,SpawnWarrior,Attack, StayInCave , GoToVillage . 1) The game is won: The game is won when the Dragon is killed, i.e., when its health points reach zero. The setDragons contains all components of typeDragon(only one in this case). We use the within operator to express that the Dragon’s health reaches zero at some point of the game (technically, at least once). ∀d∈ Dragons :♢ 1 MAX d.hp≤ 0 2) The Dragon is attacked at least once within the first 15 steps of the game: To express that the Dragon is attacked at least once during the first 15 steps of the run of the system, we check that theAttackensemble has at least one member (its cardinality is ≥ 1). ♢ 1 15 |Attack|≥ 1 3) All farmers should stay in the Village: Our strategy desires that all farmers stay in the village. First, we define a set of all farmers by selecting some of theVillagercomponents based on their role. Farmers =v ∈ Villagers | v.role = “Farmer” Then, we use♢ MAX MAX to express that it should always hold (in every time step) that the farmer’s location is the village. ∀f ∈ Farmers :♢ MAX MAX f .location = “Village” 4) All warriors should go to the Cave: Each warrior should be in theGoToCaveensemble (i.e., go from the Village to the Cave) at least once. Warriors =v ∈ Villagers | v.role = “Warrior” ∀w ∈ Warriors :♢ 1 MAX w ∈ GoToCave 5) Spawn at least a few new warriors: To effectively kill the dragon, we want at least three warriors to be spawned during the run of the system. The rules of the game define that two villagers are necessary to spawn a new one. TheSpawnWarrior ensemble should therefore have at least two members at least three times. ♢ 3 MAX |SpawnWarrior|≥ 2 6) Spawn at least a few new farmers: (similar to above) ♢ 3 MAX |SpawnFarmer|≥ 2 7) After a villager gets to the cave, it should attack the dragon: An implication can be used to express a sequence of actions. If a component is a member of theGoToCave ensemble, it moves from the Village to the Cave. We want such components to attack the Dragon at some point in the future (i.e., at least once be a member of theAttackensemble). ∀v ∈ Villagers : v ∈ GoToCave =⇒ ♢ 1 MAX v ∈ Attack However, it can happen that a villager moves to the Cave in the last step of the trace, which leaves no more steps for them to attack the Dragon, leading to constraint violation. To prevent this, we update the implication to not enforce it in the last step (i.e., when MAX = 0). (v ∈ GoToCave∧ MAX > 0) =⇒ ♢ 1 MAX v ∈ Attack 8) Warriors should be mostly in the cave: We also want the warriors to spend most of the time in the Cave, but the fact that they are spawned in the Village and first need to go to the cave prevents us from using the “always” operator (♢ MAX MAX ). We thus formulate the constraint as follows: at least 80% of the time (i.e.,0.8times the number of remaining steps), at least half of the warriors are in the Cave. Warriors =v ∈ Villagers | v.role = “Warrior” InCave =v ∈ Villagers | v.location = “Cave” ♢ 0.8·MAX MAX |Warriors ∩ InCave|≥ 0.5·|Warriors| 9) Spawn a new warrior every 10 steps: 3 To express this constraint, we reformulate it as follows. If no warrior was spawned in the previous 10 steps, spawn a warrior. We uset =−10andn = 10to express that theSpawnWarrior ensemble had less than 2 members in each of the previous 10 steps. ♢ 10 −10 |SpawnWarrior| < 2 =⇒ |SpawnWarrior|≥ 2 3 In the end, this constraint turned out to be too strong and was not imposed in the Dragon Hunt later on. V. EVALUATION A. Tools and experiment setup The main aim of our evaluation was to show that vibe coding with feedback verification is a viable approach. To this end, we implemented a framework that realizes all the conceptual components depicted in Fig. 1 and allows us to control the verification process described in Sec.I-C. Thus, it constructs the prompts (Sec.I-B3), provides input to the LLM through an API 4 , runs the system adaptation loop with constraint verification, and activates the feedback loop by presenting feedback to the LLM with a constraint violation report. The main criterion observed in each experiment is the number of feedback loop iterations needed to obtain a valid AM (one that does not violate any of the constraints imposed). Since it is not guaranteed that the LLM will ever produce a valid AM, we also abort an experiment after 10 unsuccessful iterations. For the evaluation of the Dragon Hunt example, the framework was used as follows: First, in a series of initial experiments, we tuned up the functional constraints (their final form is in Sec.IV-B) so that if the AM loses the game, there should be a constraint violation explaining why this has happened (more on the tuning process is in the replication package 1 ). Second, we run a series of experiments aiming at comparing different forms of feedback to LLM, i.e., the content of the constraint violation report: 1) generic and functional constraint violations, 2) generic constraint violations only, 3)baseline: instead of constraint violations, the feedback contained system domain metrics (for Dragon Hunt the win rate and the number of steps to win the game). The variants differ only in the feedback presented to LLM; for verification (i.e., determining if AM is valid), all generic and functional constraints are always used. Moreover, we used two versions of the initial prompt: a)functional constraints already in the initial prompt (as shown in Sec. I-B3), b) no functional constraints mentioned in the initial prompt, Each form of feedback was combined with each initial prompt, leading to six experiment variants in total. Here, since the Dragon Hunt example is relatively simple, we opted for the “GPT-5 nano” LLM (version gpt−5−nano−2025−08−07), supposedly a less capable LLM likely needing more than one iteration to produce a valid AM. Finally, to take into account the stochasticity of LLM responses, we repeated each experiment 10 times. The distribution of the results collected from these 10 experiments for the 6 experiment variants is shown in Fig. 2; the results are discussed in Sec.V-C. The implementation of the framework, as well as the experiment setup and the raw results are available in the replication package 1 . 4 openai.com/api B. FCL implementation As part of the Constraint Verifier, we implemented a subset of FCL that was sufficient to express all the functional constraints specified in Sec.IV-B. It is a simplified FCL version allowing only one implication in a constraint and prohibiting nested within operators (recall that the meaning of the within temporal operator♢ n t φis that the formulaφmust be true at leastn times within the nexttsteps). Furthermore, in a constraint, the within operator witht > 0can be either the top-level syntactical construct or in the consequent of a syntactically top-level implication. Fort < 0, the within operator can be in the antecedent of such an implication. The evaluation of FCL constraints is done online while the system runs. As for the within operator♢ n t φwitht < 0, a history of the previous−tsteps is recorded to evaluate it in the current step. Fort > 0, the within operator cannot be evaluated immediately, since the needed future values are not yet known. This is implemented by creating a temporal obligation anytime the within operator is to be evaluated (i.e., typically at the beginning of the run if it is syntactically a top-level construct, or when the antecedent of an implication is true). In each step,φis evaluated and the result is recorded. The temporal obligation keeps track of the number of time steps in whichφ was true. At the end of the time window (aftertsteps) or if it is already possible to determine the result, e.g.φwas already truentimes or♢ n t φ cannot be true (i.e.,φis false more than t− n times), the evaluation of the obligation ends. C. Results Figure 2 shows a series of histograms of the number of iterations of the vibe-coding feedback loop necessary to produce a valid AM for three variants of feedback to LLM (rows) and two variants of the initial prompt (colors). The more the histogram is concentrated toward the left, the better. The results indicate that combining vibe coding with con- straint verification is an effective form of generating an AM for the system. In most of the experiment runs, the LLM managed to produce a correctly working AM behaving according to the desired strategy (a valid AM) in just a few iterations of the feedback loop. However, for this approach to be useful, it is necessary to align functional constraints with the goals of the system, as we discuss more in Sec.V-E2. In this case, we managed to design the constraints in such a way that all generated AMs meeting the constraints won the game. Regarding different forms of feedback, in the Dragon Hunt example, there does not seem to be much difference when the functional constraints are listed in the initial prompt. When the list is removed, reporting violations of both generic and functional constraints performs the best, as for the other two methods, there were at least a few experiment runs that did not produce a valid AM (those were aborted after 10 iterations of the feedback loop). This was expected as the constraints were also used to determine the validity of the generated AM. However, this also indicates that “insufficient” feedback might cause the feedback loop to get stuck in a dead end (Sec.V-E3). 0 2 4 6 Count Generic and functional constraints in feedback with func. constr. in init. prompt w/o func. constr. in init. prompt 0 2 4 6 Count Generic constraints in feedback 123456789Aborted Number of feedback loop iterations to obtain a valid AM 0 2 4 6 Count Metrics from running the system in feedback Fig. 2: Distributions of the number of feedback-loop iterations needed to obtain a valid AM in Dragon Hunt example. Bars show counts over 10 experiments for each variant. D. Validation on a second example: Smart Farm Apart from running the experiments with the Dragoon Hunt example, we also evaluated our approach for a second example: the Smart Farm. Its scenario comes from one of our recently finished ECSEL JU project AFarCloud 5 and focuses on protecting crop fields on a farm from feeding birds by groups of autonomous drones. As birds fly from one field to another, the drones need to be coordinated and redistributed among the fields to ensure protection of the most-threatened fields. If a field is not adequately protected, the birds cause damage to the field. The overall goal is to minimize the damage rate (in % of the field area). This example is more complex than the Dragon Hunt, as it is necessary to take into account the positions of the drones when redistributing them (i.e., the villagers with the same role were interchangeable, but the drones are not). Also, there are several instances of a protecting ensemble (one for each field) compared to only singleton ensembles in the Dragon Hunt. As GPT-5 nano often failed to produce a valid AM in this harder example, we also experimented with a more capable LLM “GPT-5 mini” (version gpt−5−mini−2025−08−07). Similarly to the Dragon Hunt example, we designed a set of functional constraints (and refined them after initial experiments) for the AM to follow in order to ensure adequate protection of the fields. We used 6 constraints and they are listed in the replication package 1 . The results, summarized in Fig. 3, show a pattern similar to that in the Dragon Hunt example. Providing generic and functional constraint violations as feedback to the LLM mostly 5 http://w.afarcloud.eu/ leads to a valid AM in a few iterations. The other forms of feedback perform worse. Without functional constraints listed in the initial prompt or given as feedback to the LLM, the GPT-5 nano frequently fails to generate a valid AM. 0 2 4 6 8 Count Generic and functional constraints in feedback 0 2 4 6 8 Count Generic constraints in feedback 123456789Aborted Number of feedback loop iterations to obtain a valid AM 0 2 4 6 8 Count Metrics from running the system in feedback LLM and Prompt GPT-5 nano, with func. constr. in init. prompt GPT-5 nano, w/o func. constr. in init. prompt GPT-5 mini, with func. constr. in init. prompt GPT-5 mini, w/o func. constr. in init. prompt Fig. 3: Distributions of the number of feedback-loop iterations needed to obtain a valid AM in Smart Farm example. Bars show counts over 10 independent experiments for each variant. Regarding the efficiency of the generated AMs in protecting the fields, they perform almost as well as our previously hand- written AM: The median of damage rate for valid generated AMs was 6.9%, while for the hand-written AM it was 7.0%. E. Discussion In this section, we discuss several lessons learned from setting up the vibe coding feedback loop and expressing constraints in FCL. 1) Results summary: When the functional constraints are listed in the initial prompt, the LLMs seem to be very capable in producing a valid AM. However, especially with less capable LLMs, it is still worth verifying the AM and checking whether the requirements are met. Regarding the different forms of feedback to the LLM we experimented with, giving the LLM detailed feedback (violations of generic and functional constraints) performs the best as the other two forms of feedback did not give the LLM enough information on what should be improved to produce a valid AM. 2) Functional constraints as precise as possible: Several times in our initial experiments, the LLM designed an AM that met all the constraints, but did not win the game. By further inspecting the behavior of the AM, we noticed that the game had been lost only by a small margin (the dragon survived with only a few health points). In particular, the AM did not spawn warriors often enough to win the game; however, it managed to spawn 3 of them during the run, thus fulfilling the constraint. To mitigate this issue, we updated the set of functional constraints and initial states, adding “The dragon is attacked at least once within the first 15 steps of the game” constraint and “No Warriors” initial state. After that, the issue was solved. The takeaway here is that it might be necessary in the feedback loop to re-formulate the constraints in alignment with the desired strategy and update appropriate run path coverage (human involvement in the feedback loop might be necessary as also reported in [4]). 3) Feedback loop reaching a dead end: We encountered several times that the vibe-coding feedback loop reached a dead end, so that the AM did not improve anymore. This often happened when there was insufficient feedback. For instance, when the feedback is in the form of metrics from running the system, the only information given to the LLM is that it lost (“win rate is 0%”). As this feedback repeated multiple times in a row, the LLM tended to produce a very similar AM. It might have been slightly modified in terms of exact implementation, but it actually behaved the same. This is illustrated in Fig. 4. 12345678910 Feedback loop iteration 10 15 20 25 0 10 20 30 40 50 Steps to win the game (if the game is won) Remaining Dragon HP (if the game is lost) Successful run Dead end Fig. 4: Two runs of an experiment – one successful (valid AM after 3 iterations) and one reaching a dead end and not improving anymore. The key takeaway here is that the feedback to the LLM needs to be precise enough. If we only said “win rate is 0%”, the LLM could not identify the reason for the loss and, consequently, how to find a solution to such AM malfunction. In such situations, we found it might be better to break the feedback loop and start over, since with a fresh start, the LLM is not confused by the conversation history with the previous unsuccessful attempts into producing a similar code. 4) Importance of fine-grained constraints thanks to FCL: As mentioned in the discussion above, specific and detailed- enough feedback in the feedback loop is crucial for a successful vibe coding employment. In this respect, FCL appeared to be very useful in allowing expression of the desired properties/- constraints at the level of multiple individual adaptation steps in a time window. This is in contrast with the expressive power of constraint granularity in, e.g. classical temporal logics such as LTL (considering only next, future, globally, until) and in TLA+ modeling the advance of execution at the level of just neighboring states (the current and the “primed” (new) state). It should be emphasized that the runtime implementation of FCL constraints based on the concept of temporal obligation turned out to be relatively easy. As an aside, the idea of end- counts (MAXandBEG) necessary to model the relationship of multiple steps in finite traces was also implemented in this way. 5) AM could cooperate with FCL interpreter: Another potential use for FCL, apart from constraint verification, is to prioritize AM adaptation decisions based on the access of the AM to the temporal obligations in the FCL interpreter of Constraint Verifier. Take, for example, the constraint♢ 1 MAX |Attack| ≥ 1. Consider the very last step of the run, and this constraint still not being satisfied – this means that theAttackensemble must not be empty in this step, since otherwise the constraint would be violated. Assuming AM had access to the temporal obligation associated with the constraint, it could assign some components to theAttackensemble to make the constraint satisfied in this last-minute opportunity. Furthermore, if the AM was sufficiently sophisticated, it could have anticipated this and sent some more villagers to the Cave in the previous steps since only the villagers in the Cave can be assigned to the Attack ensemble. Fine-grained adaptation rules such as these can be dynam- ically inferred from the FCL temporal obligations to guide the AM by narrowing potential adaptation options towards efficiently meeting the statically specified strategy in ADSL. For now, this is left as a potential direction for future work. F. Limitations and Threats to Validity We structure threats to validity according to [12]: 1) Construct validity: Although our results indicate that the approach presented in this paper is viable for the two simple examples with which we experimented, we did not perform any experiments with real-world CAS. In theory, the behavior of a more complex system could be described with more elaborate FCL constraints, but designing such constraints might be demanding, as it is necessary to describe the system in enough detail and align the constraints with the goals of the system. Another potential threat arises from our definition of a valid AM in the experiment. We used the functional constraints to determine whether the generated AM follows the desired strategy we specified in the prompt in natural language. Although we did our best to formulate the constraints according to the strategy and validated them using initial experiments, we did not inspect the LLM-generated code in detail. It is theoretically possible that the LLM generated a code that does not behave exactly according to the desired strategy, but still passes the constraints. Nevertheless, we also observed the results of running the examples with the generated AMs and found out that all the AMs approved as valid by the runtime verification performed well in terms of metrics of the system (e.g., managed to win the game by killing the Dragon). Lastly, the experiments in this paper included only a small subset of available LLMs, so that other LLMs might perform differently. However, the main contribution of this paper is the approach that combines vibe coding and FCL-based runtime verification, and that does not depend on a specific LLM (the LLM used can be simply swapped by a slight modification of the API calls). 2) Internal validity: The main threat in this area is the stochasticity of both the LLM responses and our use case implementation. We tried to mitigate this by repeating the experiments several times and by observing the trends among the aggregated results. 3) External validity: We tried to design the approach to be general enough and applicable to other use cases by working on top of the abstractions of the DEECo model, which has already proven to be suitable for modeling CAS, and our novel temporal logic FCL. The approach uses a DSL to specify the domain-specific details of the use case, and the LLMs prompts are automatically generated from them, making it relatively easy to apply them in other domains. In line with this objective, we used two different use case examples for the evaluation of our approach. 4) Reliability: Reliability threats arise from the fact that LLMs can be sensitive to exact formulations of instructions in the prompts. Thus, altering the wording of the instructions and the way the prompts are constructed might change the results. VI. RELATED WORK Several related works survey vibe coding techniques [4] and list different forms of feedback to the LLM. Common options are to perform static analysis of the code and run unit tests. Liang et al. [13] iteratively refine the generated code while also generating the tests with an LLM. Nunez et al. [14] suggest a multi-agent framework, where three LLM- based agents are employed: one for generating the code, one for static analysis, and one for fuzzy testing. Ravi et al. [5] suggest five automatic feedback loops addressing compilation errors, static analysis, hand-written unit tests, and generated unit tests with mutation analysis. Kavian et al. [15] combine LLMs with static code analysis engines to improve the security of the generated code. In addition, checking for architectural smells by LLMs proposed by Pandini et al. [16] can be used to improve the code. Similarly to our approach, several other works propose some form of runtime verification in vibe coding. Councilman et al. [17] propose a high-level formal query language, which expresses the user’s intent in structured natural language, and a verifier. In contrast, we use temporal logic for the user’s intent. Zhang et al. [18] design a general specification language based on predicate logic that enables automatic checking whether LLM-generated responses adhere to domain-specific properties. However, their focus is not on vibe-coding, they verify the LLMs responses in natural language. Due to that, their proposed language does not need to consider the temporal dimension, which we do need in our approach for describing CAS. Several works employ logic for expressing and checking properties of CAS (an an overview of different approaches to specifying and modeling CAS can be found in [1]). Since they use logic as means to specify the behavior of such a system as a whole, they use modal logic that employs dynamic, spatial, and temporal concepts, such as dL [19] and SSTL [20]. Of these, the most related to our approach is the GLoTL logic [11], [21] introduced to specify the spatial and temporal properties of cooperating CAS agents at both the local and global levels. In particular, the authors introduce the concept of horizon, setting the interval[k,l]of time steps in which φin the temporal formulaψU [k,l] φhas to hold a number of times. In comparison, our within operator features, in addition to a similar time window, the option to explicitly specify the number of steps in whichφhas to hold and allows for working with finite traces thanks to the endcounts MAX and BEG . Regarding the use of LLMs for adaptation, several works focus on enhancing the MAPE-K loop with LLM-driven reasoning [22], [23] or revising the MAPE-K phases in the context of learning-enabled components [24]. Töpfer et al. [3] show how to employ LLM for ensemble resolution, but their focus (similarly to the previously mentioned works) is mainly on employing LLMs directly as part of the AM (the LLM is queried in every adaptation step). In contrast, our approach uses the LLM to generate the code for the AM before the system is run, and the LLM is not used during the adaptation. A hybrid approach is proposed by Adnan et al. [25], where the LLM is used in the context of an IoT system to select a service or implement a new one based on user-defined goals. In general, combining ML techniques with software ar- chitecture improves the adaptability and reliability of ML- based systems [24], [26], [27]. These works emphasize runtime validation and adaptation of ML components. We similarly employ runtime validation to ensure that the architecture adheres to the predefined constraints. VII. CONCLUSION We conclude the paper by summarizing the way we answered the research questions articulated in Sec. I. RQ1: We have shown that generating an AM via vibe coding is a viable option, provided that a sophisticated feedback loop is used to verify AM functionality. The verification is to be based on a very precise formulation of the behavior requirements/constraints. To this end, we designed FCL, a temporal logic that allows us to specify the behavior of traces with the granularity much finer than the classical LTL logic offers. RQ2: The key idea employed to address RQ2 presented in the paper is to integrate the checking of constraints, both generic and, in particular, functional, into the adaptation loop, so that each architectural adaptation proposed by the AM is first checked for being free of constraint violations. RQ3: The idea of combining the adaptation and feedback loops has shown to be viable in the experiments with the two examples of CAS. In particular, the feedback specifying detailed violation of fine-grained constraints articulated in FCL did not require more than a few feedback loop iterations, provided that such testing is combined with the aim of high run path coverage achieved by different initial settings of system runs. REFERENCES [1]R. De Nicola, S. Jähnichen, and M. Wirsing, “Rigorous engineering of collective adaptive systems: special section,” International Journal on Software Tools for Technology Transfer, vol. 22, no. 4, p. 389–397, May 2020. [Online]. Available: http://dx.doi.org/10.1007/s10009-020-00565-0 [2]K. Vaidhyanathan and H. Muccini, “Software architecture in the age of agentic ai,” in Software Architecture. ECSA 2025 Tracks and Workshops, D. Bianculli, H. Sartaj, V. Andrikopoulos, C. Pautasso, T. Mikkonen, J. Perez, T. Bureš, M. De Sanctis, H. Muccini, E. Navarro, M. Soliman, and U. Zdun, Eds. Cham: Springer Nature Switzerland, 2026, p. 41–49. [3]M. Töpfer, T. Bureš, F. Plášil, and P. Hn ˇ etynka, “On limits of LLMs in adaptation of ensemble-based architectures,” 2025. [Online]. Available: http://dx.doi.org/10.2139/ssrn.5357551 [4] Y. Ge, L. Mei, Z. Duan, T. Li, Y. Zheng, Y. Wang, L. Wang, J. Yao, T. Liu, Y. Cai, B. Bi, F. Guo, J. Guo, S. Liu, and X. Cheng, “A survey of vibe coding with large language models,” 2025. [Online]. Available: https://arxiv.org/abs/2510.12399 [5] R. Ravi, D. Bradshaw, S. Ruberto, G. Jahangirova, and V. Terragni, “Llmloop: Improving llm-generated code and tests through automated iterative feedback loops,” in Proceedings of ICSME 2025, 07 2025. [6]T. Bures, I. Gerostathopoulos, P. Hnetynka, J. Keznikl, M. Kit, and F. Plasil, “DEECo – an Ensemble-Based Component System,” in Proc. of CBSE’13. ACM, 2013, p. 81–90. [7]T. Bures, I. Gerostathopoulos, P. Hnetynka, F. Plasil, F. Krijt, J. Vinarek, and J. Kofron, “A language and framework for dynamic component ensembles in smart systems,” Int. Journ. on Software Tools for Technology Transfer, vol. 22, no. 4, 2020. [8]M. Y. Kovalyov and E. Pesch, “A generic approach to proving np-hardness of partition type problems,” Discrete Applied Mathematics, vol. 158, no. 17, p. 1908–1912, 2010. [Online]. Available: https://w.sciencedirect.com/science/article/pii/S0166218X10002647 [9]IBM, “An architectural blueprint for autonomic computing,” Autonomic Computing White Paper, 2005. [10]L.Lamport,SpecifyingSystems:TheTLA+Language andToolsforHardwareandSoftwareEngineers. Addison-Wesley,June2002.[Online].Available:https: //w.microsoft.com/en-us/research/publication/specifying-systems- the-tla-language-and-tools-for-hardware-and-software-engineers/ [11] M. Loreti and A. Rehman, “A logical framework for reasoning about local and global properties of collective systems,” in Quantitative Evaluation of Systems: 19th International Conference, QEST 2022, Warsaw, Poland, September 12–16, 2022, Proceedings.Berlin, Heidelberg: Springer-Verlag, 2022, p. 133–149. [Online]. Available: https://doi.org/10.1007/978-3-031-16336-4_7 [12]P. Runeson and M. Höst, “Guidelines for conducting and reporting case study research in software engineering,” Empirical Software Engineering, vol. 14, no. 2, p. 131–164, Dec. 2008. [Online]. Available: http://dx.doi.org/10.1007/s10664-008-9102-8 [13] Y. Liang, R. Ying, T. Taniguchi, C. Gan, and Z. Cui, RECODE: Leveraging Reliable Self-generated Tests and Fine-Grained Execution Feedback to Enhance LLM-Based Code Generation.Springer Nature Singapore, 2025, p. 510–521. [Online]. Available: http: //dx.doi.org/10.1007/978-981-95-0014-7_43 [14]A. Nunez, N. T. Islam, S. K. Jha, and P. Najafirad, “Autosafecoder: A multi-agent framework for securing llm code generation through static analysis and fuzz testing,” 2024. [Online]. Available: https: //arxiv.org/abs/2409.10737 [15] A. Kavian, M. M. Pourhashem Kallehbasti, S. Kazemi, E. Firouzi, and M. Ghafari, “Llm security guard for code,” in Proceedings of the 28th International Conference on Evaluation and Assessment in Software Engineering, ser. EASE 2024.ACM, Jun. 2024, p. 600–603. [Online]. Available: http://dx.doi.org/10.1145/3661167.3661263 [16]G. Pandini, A. Martini, A. N. Videsjorden, and F. A. Fontana, “An exploratory study on architectural smell refactoring using large languages models,” in 2025 IEEE 22nd International Conference on Software Architecture Companion (ICSA-C), 2025, p. 462–471. [17]A. Councilman, D. J. Fu, A. Gupta, C. Wang, D. Grove, Y.-X. Wang, and V. Adve, “Towards formal verification of llm-generated code from natural language prompts,” 2025. [Online]. Available: https://arxiv.org/abs/2507.13290 [18]Y. Zhang, S. Y. Emma, A. L. J. En, and J. S. Dong, “Rvllm: Llm runtime verification with domain knowledge,” 2025. [Online]. Available: https://arxiv.org/abs/2505.18585 [19]A. Platzer, “Overview of logical foundations of cyber-physical systems,” 10 2019. [Online]. Available: https://arxiv.org/abs/1910.11232v1 [20] V. Ciancia, S. Gilmore, G. Grilletti, D. Latella, M. Loreti, and M. Massink, “Spatio-temporal model checking of vehicular movement in public transport systems,” Int. J. Softw. Tools Technol. Transf., vol. 20, no. 3, p. 289–311, Jun. 2018. [Online]. Available: https://doi.org/10.1007/s10009-018-0483-8 [21] N. Del Giudice, M. Loreti, M. Quadrini, and A. Rehman, “Monitoring local and global properties of collective adaptive systems,” in Leveraging Applications of Formal Methods, Verification and Validation. Rigorous Engineering of Collective Adaptive Systems, T. Margaria and B. Steffen, Eds. Cham: Springer Nature Switzerland, 2025, p. 281–296. [22]J. Li, M. Zhang, N. Li, D. Weyns, Z. Jin, and K. Tei, “Exploring the potential of large language models in self-adaptive systems,” in Proc. of SEAMS 2024, Lisbon, Portugal, 2024, p. 77–83. [23]R. Donakanti, P. Jain, S. Kulkarni, and K. Vaidhyanathan, “ Reimagining Self-Adaptation in the Age of Large Language Models ,” in Companion Proceedings of ICSA 2024. IEEE CS, 2024, p. 171–174. [24]M. Casimiro, P. Romano, D. Garlan, G. A. Moreno, E. Kang, and M. Klein, Self-adaptive Machine Learning Systems: Research Challenges and Opportunities. Springer, 2022, p. 133–155. [25]B. Adnan, S. Miryala, A. Sambu, K. Vaidhyanathan, M. D. Sanctis, and R. Spalazzese, “Leveraging llms for dynamic iot systems generation through mixed-initiative interaction,” 2025. [Online]. Available: https://arxiv.org/abs/2502.00689 [26]G. A. Lewis, H. Muccini, I. Ozkaya, K. Vaidhyanathan, R. Weiss, and L. Zhu, “Software Architecture and Machine Learning (Dagstuhl Seminar 23302),” Dagstuhl Reports, vol. 13, no. 7, p. 166–188, 2024. [27]T. Bureš, “Self-adaptation 2.0,” in 2021 International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS), 2021, p. 262–263.

Instant research discovery