Vibe-Coding: Feedback-Based Automated Verification with no Human Code Inspection, a Feasibility Study

Franti\v{s}ek Pl\'a\v{s}il; Michal T\"opfer; Petr Hn\v{e}tynka; Tom\'a\v{s} Bure\v{s}

arxiv: 2604.14867 · v1 · submitted 2026-04-16 · 💻 cs.SE · cs.AI

Vibe-Coding: Feedback-Based Automated Verification with no Human Code Inspection, a Feasibility Study

Michal T\"opfer , Franti\v{s}ek Pl\'a\v{s}il , Tom\'a\v{s} Bure\v{s} , Petr Hn\v{e}tynka This is my paper

Pith reviewed 2026-05-10 11:14 UTC · model grok-4.3

classification 💻 cs.SE cs.AI

keywords vibe codingautomated verificationLLM code generationcollective adaptive systemsfeedback loopsadaptation managersruntime constraintsfunctional constraints logic

0 comments

The pith

Fine-grained runtime constraint violations let LLMs iteratively produce valid adaptation managers for collective adaptive systems without any human code review.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper tests whether vibe-coding—iterative LLM code refinement via feedback—can work for runtime-adaptive software in collective adaptive systems when no programmer ever inspects the generated code. It adds a feedback loop to the normal adaptation loop that checks output against generic architectural constraints plus functional constraints written in Functional Constraints Logic, a first-order temporal logic for finite traces. In the Dragon Hunt case study, detailed violation reports usually let the LLM reach a correct adaptation manager in a small number of rounds. Coarse performance metrics, by contrast, frequently cause the loop to stall. The authors conclude that feedback precision, rather than other variables, decides whether domain experts without programming skills can still obtain reliable systems.

Core claim

The paper shows that, in the Dragon Hunt CAS case study, fine-grained constraint violations provide actionable feedback that typically yields a valid adaptation manager within a few iterations, while simple coarse metric-based feedback often stalls. Feedback precision is the dominant factor for reliable vibe coding in systems designed by domain experts with no programming skills, thereby obviating the need for human code inspection.

What carries the argument

The integrated feedback loop that pairs the CAS adaptation loop with precise runtime checks against architectural constraints and Functional Constraints Logic (FCL) formulas, then feeds violation details back to the LLM for repair.

If this is right

Domain experts without programming skills can still obtain working runtime-adaptive managers.
Human code inspection is no longer required for verification in this setting.
Precision of feedback reports matters more than the choice of LLM or initial prompt for success.
The same loop can be applied to other collective adaptive systems whose constraints can be expressed in FCL.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The method might apply to LLM-generated code in non-adaptive domains if suitable constraint languages are developed.
If FCL-style specifications prove reusable across projects, the upfront cost of writing them could be amortized over many generated systems.
Scaling the approach to larger systems would require automated ways to maintain and update the constraint set as requirements evolve.

Load-bearing premise

That the chosen constraints and FCL formulas will catch every relevant runtime failure and that the LLM can always translate the violation reports into correct fixes without introducing new errors.

What would settle it

A trial in which the LLM receives repeated violation reports yet produces code that still fails at runtime or that introduces new failures the constraints do not detect.

Figures

Figures reproduced from arXiv: 2604.14867 by Franti\v{s}ek Pl\'a\v{s}il, Michal T\"opfer, Petr Hn\v{e}tynka, Tom\'a\v{s} Bure\v{s}.

**Figure 2.** Figure 2: Distributions of feedback-loop iterations needed to [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗

read the original abstract

Vibe coding inherently assumes iterative refinement of LLM-generated code through feedback loops. While effective for conventional software tasks, its reliability in runtime-adaptive systems is unclear -- especially when generated code is not manually inspected. This paper studies feedback-based automated verification of LLM-generated adaptation managers in Collective Adaptive Systems (CAS). We focus on the key challenges of verification in the loop: how to detect failures of generated code at runtime and how to report them precisely enough for an LLM to fix them. We combine the adaptation loop with a vibe-coding feedback loop where correctness is checked against (i) generic architectural constraints and (ii) functional constraints formalized in Functional Constraints Logic (FCL), a novel first-order temporal logic over potentially finite traces. Conducting the Dragon Hunt CAS case study, we show that fine-grained constraint violations provide actionable feedback that typically yields a valid adaptation manager within a few iterations, while simple coarse metric-based feedback often stalls. Our findings suggest that feedback precision is the dominant factor for reliable vibe coding in systems designed by domain experts with no programming skills, thereby obviating the need for human code inspection.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This feasibility study shows fine-grained FCL feedback can steer LLM fixes for a CAS adaptation manager without human code review in one example, but the single case and lack of completeness argument keep the broader claim preliminary.

read the letter

The main thing to know is that the authors introduce Functional Constraints Logic (FCL), a first-order temporal logic over finite traces, and use it to generate precise violation reports that an LLM can act on to repair its own generated adaptation manager code. In the Dragon Hunt case study, this fine-grained feedback typically produces a working manager in a few iterations, while coarse metric feedback stalls. The setup folds the verification step into the vibe-coding loop so no one inspects the code by hand. That combination of a new logic with automated feedback for collective adaptive systems is the clearest novelty relative to prior vibe-coding work. The paper does a clean job framing the two practical problems—how to detect runtime failures and how to report them precisely enough for the LLM—and then showing through the example that precision matters more than just having feedback at all. The architectural constraints plus FCL formulas give the loop something concrete to work with, which is a reasonable step for systems aimed at domain experts who do not code. The soft spots are mostly about scope and evidence. Everything rests on a single case study, and the write-up gives no iteration counts, success rates across runs, error bars, or statistical comparison. Without those numbers it is hard to judge how robust the difference really is. The larger concern is whether the chosen constraints and FCL formulas actually catch every failure mode that could appear in the generated code. The paper offers no completeness argument or exhaustive check, so an undetected problem would leave the loop unable to guarantee correctness and the “no human inspection” claim would not hold. The assumption that the LLM will reliably turn a violation report into a correct fix without introducing new errors is also shown only for this instance. This work is aimed at researchers in software engineering who study LLM-assisted development of self-adaptive systems or formal feedback loops for generated code. A reader working on verification for collective adaptive systems or on making generative tools usable by non-programmers would get a concrete idea to test. It deserves a serious referee because the core mechanism is new and the motivation is practical, even though the current evidence is limited to feasibility. I would send it out for review and ask for additional case studies, quantitative results, and some argument on constraint coverage.

Referee Report

2 major / 2 minor

Summary. The paper presents a feasibility study on vibe-coding for LLM-generated adaptation managers in Collective Adaptive Systems (CAS). It combines an adaptation loop with a feedback loop that checks correctness against generic architectural constraints and functional constraints expressed in a new first-order temporal logic called Functional Constraints Logic (FCL) over potentially finite traces. In the Dragon Hunt CAS case study, the authors report that fine-grained violation reports enable the LLM to produce valid managers within a few iterations, while coarse metric-based feedback often stalls. They conclude that feedback precision is the dominant factor, allowing domain experts without programming skills to create reliable systems without human code inspection.

Significance. If the empirical observations hold beyond the single case study, the work could reduce the human verification burden in developing runtime-adaptive systems and enable non-programmers to participate more directly. The introduction of FCL as a novel logic tailored to finite traces is a concrete technical contribution that may find use in other verification contexts. The paper is grounded in a concrete CAS example rather than purely abstract claims, which strengthens its practical relevance.

major comments (2)

[Dragon Hunt CAS case study] Dragon Hunt CAS case study: the central claim that fine-grained feedback 'obviates the need for human code inspection' rests on the unshown assumption that the chosen architectural constraints plus FCL formulas detect every relevant runtime failure mode. No completeness argument, exhaustive enumeration of failure modes, or proof sketch is provided that the selected constraints cover the full space of possible failures for this domain (or for CAS in general). If an undetected failure exists, the loop cannot guarantee correctness and the LLM may still emit unsafe code.
[Dragon Hunt CAS case study] Results presentation (case study section): iteration counts, success rates, exact FCL formulas used, number of runs, and any statistical measures (error bars, baselines, or variance) are not reported. Without these, it is impossible to judge whether the observed difference between fine-grained and coarse feedback is robust or reproducible, weakening the claim that precision is 'the dominant factor'.

minor comments (2)

[FCL definition] The definition and semantics of FCL (first-order temporal logic over finite traces) would benefit from an explicit grammar or small example derivation to clarify how violation reports are generated and fed back to the LLM.
[Related work] The manuscript would be strengthened by a short discussion of related work on runtime verification of adaptive systems and on LLM-based code repair loops, even if only to position the novelty of combining architectural constraints with FCL.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive and detailed comments on our feasibility study. We address each major comment below, clarifying the scope of our claims and committing to improvements in the revised manuscript.

read point-by-point responses

Referee: [Dragon Hunt CAS case study] Dragon Hunt CAS case study: the central claim that fine-grained feedback 'obviates the need for human code inspection' rests on the unshown assumption that the chosen architectural constraints plus FCL formulas detect every relevant runtime failure mode. No completeness argument, exhaustive enumeration of failure modes, or proof sketch is provided that the selected constraints cover the full space of possible failures for this domain (or for CAS in general). If an undetected failure exists, the loop cannot guarantee correctness and the LLM may still emit unsafe code.

Authors: We appreciate the referee's emphasis on this point. Our paper is framed as a feasibility study, not a general verification framework, and we do not claim or assume that the chosen constraints and FCL formulas detect every possible runtime failure mode. The central observation is that, for the specific Dragon Hunt CAS, these constraints provided sufficient feedback for the LLM to converge on a valid adaptation manager without human code inspection. We acknowledge that undetected failures could exist outside the covered constraints. In the revision we will add an explicit limitations subsection (likely in the case study or discussion) that states the assumptions about constraint coverage, notes the absence of a completeness argument, and moderates the language to indicate that human inspection is reduced rather than fully obviated when the constraints are adequate for the domain. revision: yes
Referee: [Dragon Hunt CAS case study] Results presentation (case study section): iteration counts, success rates, exact FCL formulas used, number of runs, and any statistical measures (error bars, baselines, or variance) are not reported. Without these, it is impossible to judge whether the observed difference between fine-grained and coarse feedback is robust or reproducible, weakening the claim that precision is 'the dominant factor'.

Authors: We agree that the current results section would benefit from greater transparency and detail to support reproducibility and assessment of robustness. The experiments consisted of multiple LLM runs comparing fine-grained versus coarse feedback. In the revised manuscript we will report the exact FCL formulas, per-run iteration counts, success rates (e.g., fraction of trials reaching a valid manager within a bounded number of iterations), number of runs performed, and observed variance. We will also include a brief discussion of experimental variability inherent to LLM sampling and note any simple baselines used. These additions will be presented in tables or enumerated lists within the case study section. revision: yes

Circularity Check

0 steps flagged

No circularity; empirical case-study observations with no self-referential derivations

full rationale

The paper is a feasibility study reporting empirical results from the Dragon Hunt CAS case study. Central claims concern the relative effectiveness of fine-grained constraint violations versus coarse metrics in enabling LLM fixes within the vibe-coding loop. These are presented as observations from running the combined adaptation+verification process, not as quantities derived from equations or parameters that reduce to the inputs by construction. No mathematical derivations, fitted inputs renamed as predictions, or self-citation chains appear in the abstract or provided text. The introduction of FCL is a definitional contribution rather than a circular one, and success is demonstrated experimentally on the chosen example rather than proven in a self-contained deductive chain. The study is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The approach depends on the sufficiency of the chosen constraints to capture correctness and on the LLM's ability to act on violation feedback; FCL is introduced as a new formalism without independent verification beyond the case study.

axioms (2)

domain assumption Architectural constraints plus FCL formulas are sufficient to detect all relevant failures of the generated adaptation managers.
Invoked as the basis for automated verification in the feedback loop.
domain assumption The LLM can interpret precise violation reports and produce corrected code that satisfies the constraints.
Required for the iterative refinement to succeed without human intervention.

invented entities (1)

Functional Constraints Logic (FCL) no independent evidence
purpose: Formalize functional constraints over potentially finite traces for precise violation reporting to the LLM.
Presented as novel; no external evidence of prior use or independent validation provided.

pith-pipeline@v0.9.0 · 5522 in / 1426 out tokens · 47498 ms · 2026-05-10T11:14:08.303017+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

14 extracted references · 14 canonical work pages

[1]

Tomas Bures, Ilias Gerostathopoulos, Petr Hnetynka, Jaroslav Keznikl, Michal Kit, and Frantisek Plasil. 2013. DEECo – an Ensemble-Based Component System. InProc. of CBSE’13. ACM, 81–90

work page 2013
[2]

Aaron Councilman, David Jiahao Fu, Aryan Gupta, Chengxiao Wang, David Grove, Yu-Xiong Wang, and Vikram Adve. 2025. Towards Formal Verification of LLM-Generated Code from Natural Language Prompts. arXiv:2507.13290 [cs.PL] https://arxiv.org/abs/2507.13290

work page arXiv 2025
[3]

Rocco De Nicola, Stefan Jähnichen, and Martin Wirsing. 2020. Rigorous engi- neering of collective adaptive systems: special section.International Journal on Software Tools for Technology Transfer22, 4 (2020), 389–397. doi:10.1007/s10009- 020-00565-0

work page doi:10.1007/s10009- 2020
[4]

Nicola Del Giudice, Michele Loreti, Michela Quadrini, and Aniqa Rehman. 2025. Monitoring Local and Global Properties of Collective Adaptive Systems. In Leveraging Applications of Formal Methods, Verification and Validation. Rigorous Engineering of Collective Adaptive Systems. Springer, 281–296

work page 2025
[5]

Yuyao Ge, Lingrui Mei, Zenghao Duan, Tianhao Li, Yujia Zheng, Yiwei Wang, Lexin Wang, Jiayu Yao, Tianyu Liu, Yujun Cai, Baolong Bi, Fangda Guo, Jiafeng Guo, Shenghua Liu, and Xueqi Cheng. 2025. A Survey of Vibe Coding with Large Language Models. arXiv:2510.12399 [cs.AI] https://arxiv.org/abs/2510.12399

work page arXiv 2025
[6]

Kovalyov and Erwin Pesch

Mikhail Y. Kovalyov and Erwin Pesch. 2010. A generic approach to proving NP-hardness of partition type problems.Discrete Applied Mathematics158, 17 (2010), 1908–1912. doi:10.1016/j.dam.2010.08.001

work page doi:10.1016/j.dam.2010.08.001 2010
[7]

Michele Loreti and Aniqa Rehman. [n. d.]. A Logical Framework for Reasoning About Local and Global Properties of Collective Systems. InProc. of QEST 2022, Warsaw, Poland. doi:10.1007/978-3-031-16336-4_7

work page doi:10.1007/978-3-031-16336-4_7 2022
[8]

Niels Mündler, Mark Niklas Müller, Jingxuan He, and Martin Vechev. 2025. SWT- Bench: Testing and Validating Real-World Bug-Fixes with Code Agents.arXiv preprint arXiv:2406.12952(2025)

work page arXiv 2025
[9]

Ana Nunez, Nafis Tanveer Islam, Sumit Kumar Jha, and Peyman Najafirad. 2024. AutoSafeCoder: A Multi-Agent Framework for Securing LLM Code Generation through Static Analysis and Fuzz Testing. arXiv:2409.10737 [cs.SE] https://arxiv. org/abs/2409.10737

work page arXiv 2024
[10]

Michal Töpfer, Tomáš Bureš, František Plášil, and Petr Hnětynka. 2025. On Limits of LLMs in Adaptation of Ensemble-Based Architectures. (2025). doi:10. 2139/ssrn.5357551

work page 2025
[11]

Michal Töpfer, František Plášil, Tomáš Bureš, and Petr Hnětynka. 2026. Feedback- based Automated Verification in Vibe Coding of CAS Adaptation Built on Con- straint Logic. arXiv:2602.18607 [cs.AI] https://arxiv.org/abs/2602.18607

work page arXiv 2026
[12]

Karthik Vaidhyanathan and Henry Muccini. 2026. Software Architecture in the Age of Agentic AI. InSoftware Architecture. ECSA 2025 Tracks and Work- shops. Springer Nature Switzerland, Cham, 41–49

work page 2026
[13]

Yedi Zhang, Sun Yi Emma, Annabelle Lee Jia En, and Jin Song Dong. 2025. RvLLM: LLM Runtime Verification with Domain Knowledge. arXiv:2505.18585 [cs.AI]

work page arXiv 2025
[14]

Li Zhong and Zilong Wang. 2024. Can LLM Replace Stack Overflow? A Study on Robustness and Reliability of Large Language Model Code Generation.Proceed- ings of the AAAI Conference on Artificial Intelligence38, 19 (2024), 21841–21849. doi:10.1609/aaai.v38i19.30185 5

work page doi:10.1609/aaai.v38i19.30185 2024

[1] [1]

Tomas Bures, Ilias Gerostathopoulos, Petr Hnetynka, Jaroslav Keznikl, Michal Kit, and Frantisek Plasil. 2013. DEECo – an Ensemble-Based Component System. InProc. of CBSE’13. ACM, 81–90

work page 2013

[2] [2]

Aaron Councilman, David Jiahao Fu, Aryan Gupta, Chengxiao Wang, David Grove, Yu-Xiong Wang, and Vikram Adve. 2025. Towards Formal Verification of LLM-Generated Code from Natural Language Prompts. arXiv:2507.13290 [cs.PL] https://arxiv.org/abs/2507.13290

work page arXiv 2025

[3] [3]

Rocco De Nicola, Stefan Jähnichen, and Martin Wirsing. 2020. Rigorous engi- neering of collective adaptive systems: special section.International Journal on Software Tools for Technology Transfer22, 4 (2020), 389–397. doi:10.1007/s10009- 020-00565-0

work page doi:10.1007/s10009- 2020

[4] [4]

Nicola Del Giudice, Michele Loreti, Michela Quadrini, and Aniqa Rehman. 2025. Monitoring Local and Global Properties of Collective Adaptive Systems. In Leveraging Applications of Formal Methods, Verification and Validation. Rigorous Engineering of Collective Adaptive Systems. Springer, 281–296

work page 2025

[5] [5]

Yuyao Ge, Lingrui Mei, Zenghao Duan, Tianhao Li, Yujia Zheng, Yiwei Wang, Lexin Wang, Jiayu Yao, Tianyu Liu, Yujun Cai, Baolong Bi, Fangda Guo, Jiafeng Guo, Shenghua Liu, and Xueqi Cheng. 2025. A Survey of Vibe Coding with Large Language Models. arXiv:2510.12399 [cs.AI] https://arxiv.org/abs/2510.12399

work page arXiv 2025

[6] [6]

Kovalyov and Erwin Pesch

Mikhail Y. Kovalyov and Erwin Pesch. 2010. A generic approach to proving NP-hardness of partition type problems.Discrete Applied Mathematics158, 17 (2010), 1908–1912. doi:10.1016/j.dam.2010.08.001

work page doi:10.1016/j.dam.2010.08.001 2010

[7] [7]

Michele Loreti and Aniqa Rehman. [n. d.]. A Logical Framework for Reasoning About Local and Global Properties of Collective Systems. InProc. of QEST 2022, Warsaw, Poland. doi:10.1007/978-3-031-16336-4_7

work page doi:10.1007/978-3-031-16336-4_7 2022

[8] [8]

Niels Mündler, Mark Niklas Müller, Jingxuan He, and Martin Vechev. 2025. SWT- Bench: Testing and Validating Real-World Bug-Fixes with Code Agents.arXiv preprint arXiv:2406.12952(2025)

work page arXiv 2025

[9] [9]

Ana Nunez, Nafis Tanveer Islam, Sumit Kumar Jha, and Peyman Najafirad. 2024. AutoSafeCoder: A Multi-Agent Framework for Securing LLM Code Generation through Static Analysis and Fuzz Testing. arXiv:2409.10737 [cs.SE] https://arxiv. org/abs/2409.10737

work page arXiv 2024

[10] [10]

Michal Töpfer, Tomáš Bureš, František Plášil, and Petr Hnětynka. 2025. On Limits of LLMs in Adaptation of Ensemble-Based Architectures. (2025). doi:10. 2139/ssrn.5357551

work page 2025

[11] [11]

Michal Töpfer, František Plášil, Tomáš Bureš, and Petr Hnětynka. 2026. Feedback- based Automated Verification in Vibe Coding of CAS Adaptation Built on Con- straint Logic. arXiv:2602.18607 [cs.AI] https://arxiv.org/abs/2602.18607

work page arXiv 2026

[12] [12]

Karthik Vaidhyanathan and Henry Muccini. 2026. Software Architecture in the Age of Agentic AI. InSoftware Architecture. ECSA 2025 Tracks and Work- shops. Springer Nature Switzerland, Cham, 41–49

work page 2026

[13] [13]

Yedi Zhang, Sun Yi Emma, Annabelle Lee Jia En, and Jin Song Dong. 2025. RvLLM: LLM Runtime Verification with Domain Knowledge. arXiv:2505.18585 [cs.AI]

work page arXiv 2025

[14] [14]

Li Zhong and Zilong Wang. 2024. Can LLM Replace Stack Overflow? A Study on Robustness and Reliability of Large Language Model Code Generation.Proceed- ings of the AAAI Conference on Artificial Intelligence38, 19 (2024), 21841–21849. doi:10.1609/aaai.v38i19.30185 5

work page doi:10.1609/aaai.v38i19.30185 2024