FlowCheck: Helping End-Users Specify and Verify Intent in Vibe-Coded Web Apps

arXiv:2608.28880v1 [cs.SE] 28 Aug 2026

FlowCheck: Helping End-Users Specify and Verify Intent in Vibe-Coded Web Apps Reya Vir

Lydia Chilton

Columbia University New York, USA reyavir@cs.columbia.edu

Columbia University New York, USA chilton@cs.columbia.edu

Zhuo Zhang

Eugene Wu

Columbia University New York, USA zz3474@columbia.edu

Abstract Vibe-coded applications often contain silent behavioral failures in which the interface appears functional even though user-visible information does not flow to the expected state or output. We introduce FlowCheck, a constraint language to specify these user-visible information flows directly through the application interface, where constraints can also be displayed and inspected without reading code, and are structured enough for reliable LLM generation. FlowCheck translates the constraints into deterministic CodeQL analyses, and we evaluate it across four applications generated via Claude Code, and compare with three coding models as bug-finding baselines. We find that FlowCheck correctly translates and flags all 30 of our injected constraint violations with no false positives. In contrast, frontier models (Claude Opus 4.7, DeepSeek V3, and Gemini Pro) showed significantly lower accuracy when prompted to find bugs in the same code, with none achieving full accuracy. This approach lets vibe coders state intent in terms of the interface they understand, and checks it deterministically against the code they do not.

Columbia University New York, USA ewu@cs.columbia.edu October 4–9, 2026, Oakland, CA, USA. ACM, New York, NY, USA, 14 pages. https://doi.org/10.1145/3843750.3843844

1

Introduction

Large language model (LLM) coding agents have democratized software development. End users with little programming experience can now “Vibe code” complex applications and iterate on their features via natural language. These Vibe Coders evaluate progress primarily by interacting with the application rather than inspecting its implementation. This shifts the bottleneck from writing code to determining whether the generated application behaves as intended. Coding agents remain unreliable. They may misunderstand requests, omit necessary state updates, introduce incorrect data flows, or break previously working behavior. Prior work has documented incomplete implementations, regressions, and incorrect agent-generated code [7, 33]. Beyond code-level errors, large-scale analysis of real codingagent sessions shows that agents frequently break down on what users actually want [29]. These Silent Behavioral Failures—the application runs but its observable behavior CCS Concepts: • Software and its engineering → Softviolates user intents—are especially difficult to detect when ware verification and validation; Domain specific lanthe application compiles, renders normally, and produces guages; • Human-centered computing → Interactive sysplausible feedback. A button may report success even though tems and tools. no data was saved, or a displayed value may update without Keywords: Vibe Coding, LLM Code Generation, End-User reflecting the state it is supposed to represent. Programming, Static Analysis, Software Verification Existing debugging techniques like unit, integration, and ACM Reference Format: end-to-end testing can validate behavior, but require users Reya Vir, Lydia Chilton, Zhuo Zhang, and Eugene Wu. 2026. FlowCheck: to identify test cases and encode the expected result as an Helping End-Users Specify and Verify Intent in Vibe-Coded Web executable oracle. LLM-based testing and debugging reduce Apps. In Proceedings of the 2nd ACM SIGPLAN International Workthe authoring burden, but we find these are probabilistic shop on Language Models and Programming Languages (LMPL ’26), and limited in the types of failures they can identify. Traditional static analysis and program verification techniques are deterministic for predefined program properties, but are This work is licensed under a Creative Commons Attribution 4.0 Internadesigned for programmers rather than vibe coders. tional License. Vibe coders therefore need a way to express what they LMPL ’26, Oakland, CA, USA expect in terms of the interface they understand and to de© 2026 Copyright held by the owner/author(s). terministically check whether the implementation supports ACM ISBN 979-8-4007-2986-7/2026/10 https://doi.org/10.1145/3843750.3843844 that behavior. We focus on web applications, where user

LMPL ’26, October 4–9, 2026, Oakland, CA, USA

intents can be expressed as constraints over flows between user actions, interface-level updates, persistent state, and backend calls. For example, a user may expect that clicking a button should update a displayed total based on an input, or that submitting a form will persist its contents. We introduce FlowCheck, a system that expresses and checks data and control flow constraints over visible interface elements and application effects—for instance, that an action should not update a particular component, values should derive from specific inputs, state must persist across reloads, or an action must trigger an API call. We define a constraint language that users can express and visualize directly in the application interface, and that can be easily generated by LLMs. The constraints compile to static analysis queries (CodeQL) over the application’s event handlers, control and data flow, and interface and storage accesses. Example 1.1. The user asks an agent to add a promotionalcode feature to a vibe-coded shopping application. The agent creates a promo input and an “Apply” button. When the user enters a valid code, the interface displays “Discount applied!” even though the new total is neither persisted nor shown: function applyPromo() { const getById = id => document.getElementById(id); const code = getById('promo-input').value; if (code === 'SAVE20') { // read and update cart state let tot = parseFloat(localStorage.getItem('cartTotal')); tot *= 0.8; // Update success message in UI getById('promo-msg').innerText = 'Discount␣applied!'; // BUG: did not persist nor display updated total // localStorage.setItem('cartTotal', tot); // missing } }

Although the app runs and the message suggests the feature works, it violates the user’s expectation that applying the code changes the cart total, even on refresh. In FlowCheck, users can specify that clicking the button should cause the promo code to update the displayed and persisted total. The analysis identifies that the message is updated but the discounted value does not flow to either destination. Unlike LLM-as-judge approaches, FlowCheck returns the same result for identical code and constraints, without executing the app. Here, our focus is on properties that can be statically analyzed, as they are lightweight and can be used within agent loops. We find that constraints are useful targets for agents to generate to aid testing their code, and violations provide details of the failure and intended behavior, which guides debugging and avoids relying on vibe-coder guesses. Our paper makes the following contributions: 1. We develop a taxonomy of silent behavioral failures from a formative study spanning four applications, three coding

Reya Vir, Lydia Chilton, Zhuo Zhang, and Eugene Wu

models, and four iteration steps. From these, we identified 23 distinct failures, where nearly half (48%) can be expressed and checked fully using our static constraints. 2. We introduce a constraint language and interface through which end users express expected behavior using visible elements, actions, and effects. 3. We present a deterministic static-analysis system that translates these constraints into CodeQL queries and checks the required control-flow and data-flow relationships. 4. We evaluate FlowCheck on 30 injected failures across four web applications (14–21 constraints each), where it achieves 100% detection accuracy, compared to at most 26/30 (87%) for the best LLM baseline (Claude, best prompt). We further show that agents can author valid constraints in our language, and that using them to check code raises the agents’ bug-catch rate on a test app, an early sign the language is learnable and usable by LLMs.

2

Related Work

2.1

Evaluating LLM-Generated Applications

Coding agents struggle as requirements iteratively grow, across front-end development [31] and backend correctness constraints [7, 33]. We focus on silent behavioral failures: the application runs and presents plausible output, but uservisible information does not flow to the expected state or element. This differs from prior semantic failures [14, 15] by grounding correctness in end user’s expectations. LiveCodeBench and DebugBench evaluate self-contained problems with predefined input-output oracles [9, 30], while SWE-bench evaluates patches to existing repositories [10]. These benchmarks therefore do not capture expectations expressed through a newly generated application’s interface. Recent vibe-coding benchmarks evaluate complete applications using browser agents or LLM judgments [1, 31]. However, recent position work argues that vibe coding needs more deterministic checking [19]; our formative study characterizes failures, while FlowCheck lets users state and deterministically check the expected information flows. Automated test generation is another approach to check agent-generated code, but faces the oracle problem, where a test is dependent on knowing what the correct behavior should be [2]. Tools such as EvoSuite [8] are able to produce test sets and suggest assertions, but those assertions are based on what the current code does, rather than what it should do. The same issue occurs with LLM-based test generators like TestPilot [26] which generates JavaScript (JS) unit tests by prompting a model with the implementation of the function, so its oracles may reflect the existing code. If the code contains silent failures, the generated oracle may not be able to detect it. In our approach, our constraints supply the oracle from an outside user or agent, representing the user’s intended behavior separate from implementation.

FlowCheck: Helping End-Users Specify and Verify Intent in Vibe-Coded Web Apps

2.2

Specifications and LLM Debugging

SpecGen, AutoSpec, Clover, and PATAgent use LLMs to generate or formalize specifications and then apply verification tools [16, 27, 35, 37]. Their specifications describe code using formal abstractions that non-programmers cannot easily inspect. Our language is intentionally less expressive: it describes user-visible actions, elements, and information flows, can be authored and displayed within the application interface, and is simple enough for an LLM to generate. LLM-based debugging and repair instead ask a model to diagnose or correct the program. This has been done in various ways: by prompting it to explain and revise its own code [5], by using execution traces or semantic context [34], or more recently by treating the LLM as an autonomous agent that plans and invokes tools [3]. However, self-repair gives inconsistent gains, and models are limited by their ability to provide actionable feedback on why code fails [23]. Even where repair succeeds, it does not leave the user with a persistent, independently checkable statement of the intended behavior. Our constraints remain visible to the user, and their analysis is deterministic regardless of whether the user or an LLM authored them.

2.3

End-User Web Testing and Programming

Dynamic web-testing systems such as GUITAR, Crawljax, and Atusa execute interaction sequences and check resulting interface states or DOM invariants [17, 18, 20]. Quickstrom similarly checks user-facing behavior, but it uses a runtime approach, with specifications written in a temporal logic aimed at web programmers [22]. Our constraints similarly describe application-level behavior, but are checked statically as information-flow relationships without executing or crawling the application. This makes checks immediate and repeatable, but excludes runtime-only properties such as external API results or dynamically generated code. End-user programming systems already make the program and state visible to the user. Users can debug by directly asserting e.g., spreadsheet values, select interface artifacts, or ask questions about program behavior [4, 11, 25]. Triggeraction programming (TAP) further shows that if–then rules can be accessible to non-programmers [36]. Recent work shows that natural language is difficult for users and programmers to state their intent [24]. Vibe coders struggle with reading and evaluating correctness of LLMgenerated code [21]. Prior work frames this as an abstraction gap between user intent and generated code, and bridges this by making the generated code legible or visualized so the user can form an accurate mental model [13]. We instead start with the visible interface, and define data- and control-flow constraints from what users can directly express. Formally stating the intended behavior lets FlowCheck mechanically check and enforce them on behalf of the vibe coder.

3

LMPL ’26, October 4–9, 2026, Oakland, CA, USA

Formative Study: Vibe Coding Failures

We conducted a formative study to characterize failures that arise during iterative vibe coding. Across four applications and three coding systems, we observed 23 distinct failures. Every application and system exhibited at least one failure. 3.1

Methodology

We used a closed-weight model (Claude Opus 4.7), an openweight model (DeepSeek V3), and a commercial vibe-coding system (Lovable). For each system, we generated four applications with four scripted stages: initial generation, feature addition, refactoring, and feature modification. We fixed the prompts across systems, requested plain JavaScript without frameworks, saved the code after each stage, and manually checked it against expectations written before generation. The applications were a workshop speaker scheduler; a column-based task board refactored into a whiteboard with dependencies between tasks; a shopping application with promo codes and limited-edition items; and an image gallery with favorites, albums, navigation, and a public image API. 3.2

Observed Failures

We grouped the 23 failures into five recurring categories. Surface-level correctness. The visible output is disconnected from the data or action it claims to represent. In the image galleries produced by Claude, DeepSeek, and Lovable, clicking a thumbnail opened a different image; data should flow from the clicked thumbnail to the popup. In DeepSeek’s shopping app, the VIP20 promo code failed when the cart contained limited-edition items; the displayed total ignored the promo input and cart contents. Dropped constraints across iterations. A relationship established in one iteration, disappeared after a later modification. All three systems dropped the rule that a speaker could occupy only one slot after a subsequent prompt allowed multiple speakers per slot. Similarly, after task boards became whiteboards, Claude, DeepSeek, and Lovable allowed a task to move directly from “not started” to “finished,” despite an earlier rule forbidding that state update. In both cases, the interface remained functional, but an earlier restriction on which actions could update state was lost. Missing implied functionality. The interface advertises an action without connecting it to its corresponding effect. The Claude and DeepSeek task boards displayed an archive area labeled “Move a card here to set aside,” but dropping a card did not update the archive; only a separate button worked. DeepSeek’s shopping app presented Tinder-style cards, but swiping did not advance the displayed item and users had to fall back to buttons. These failures expose missing action-toeffect links, although gesture semantics such as dragging and swiping may need runtime support beyond static analysis. Breaking changes after modification. A new feature or refactoring severed a relationship that previously worked.

LMPL ’26, October 4–9, 2026, Oakland, CA, USA

Reya Vir, Lydia Chilton, Zhuo Zhang, and Eugene Wu

After the task board was converted to a whiteboard, cards from all three systems no longer displayed their status: the underlying task state no longer flowed to the visible card. In DeepSeek’s dependency editor, adding 𝐴 → 𝐵 and then 𝐴 → 𝐶 silently rewrote the graph as 𝐴 → 𝐶 → 𝐵, so the second action overwrote rather than preserved the relationship. Incomplete persistence. State was not saved, restored, or associated with the correct data. In the image gallery, favorites were stored by position rather than image identity, so reloading caused saved favorites to refer to different images (Claude, DeepSeek, Lovable). In Lovable’s speaker scheduler, neither the speaker list nor the schedule survived a reload, despite the prompt describing the generated people as “my speaker list.” The first failure persisted the wrong source; the second omitted the save-and-restore path entirely. Failures in the Wild. Beyond our study, we observed the same patterns in public vibe-coding transcripts1 : one agent generated search and history interfaces without creating the required database tables, while another left a game permanently displaying “loading” because an asynchronous result never reached the interface. 3.2.1 Summary of Findings. We find that 11 of the 23 failures share a common structure: missing or incorrect relationships between a user action and an observable effect. These included whether a component is updated, whether its value derives from the correct inputs, whether an update is prohibited under a condition, and whether state persists across reloads. Because these relationships span event handlers, control flow, DOM updates, and storage operations, they are non-local and difficult to reason about from code fragments, yet visible to the user. This motivates an interfacegrounded constraint language that makes such information flows explicit and mechanically checkable.

4

System Overview

Our system helps users verify and debug their vibe coded web applications. Instead of asking agents to debug, users author constraints by clicking through the behavior they expect, and FlowCheck verifies if the code aligns with that behavior. As shown in Figure 4, users select interface elements, actions, and storage state as nouns and specify the flows between them. Thus, the user interacts with the app as normal, without needing to learn or inspect code. The workflow has the following three steps: First, code is preprocessed to add element identifiers (Section 6.1). Second, users author constraints through an interface running their app, or an agent generates them (Sections 6.2 and 6.4). Third, constraints compile into static analysis queries that run against the code, and returns pass/fail results. (Section 5.5).

Figure 1. FlowCheck Core Engine. The app source code is preprocessed by CodeQL to support later static analysis queries. User- or LLM- authored constraints are compiled into CodeQL primitives, and run to find violations. Finally, we output the constraints that passed or failed. 2 CodeQL is a static code analysis engine3 that compiles source code into a relational database that models the abstract syntax tree, control-flow graph, and data-flow graph. We pre-process HTML separately in order to identify interface elements (Section 6.1). Thus, constraints reduce to queries over the database and pre-processed HTML; each query result is an instance of a match (e.g., a code path) that violates some expected behavior.

5

Constraint Language

5.1

Design Principles

Drawing from related work in end user programming, we made three design decisions: • Observability: The end-user’s mental model is the interface, and they reason about expectations in terms of visible UI states. For this reason, we restrict constraints to observable elements, or key components we make visible to the user (API, storage). • Action to behavior framing: every constraint is conditioned on a single user action, motivated by the triggeraction structure. Users reason about intent in terms of cause and effect (TAP), where an action leads to (or does not lead to) an expected effect [32]. • Static verifiability: We allow users to express only things we can check statically. Constraints that would require running the app (such as confirming an actual value from an API call, or detecting a race condition) are out of scope, as they require runtime tracing. Static analysis ensures it is deterministic and does not vary across traces. 5.2

Abstractions

We make the following abstractions to express constraints over the app’s behavior. These are designed to be easy for a user to understand, and also easy for an LLM to generate.

1 https://github.com/jennygzma/vibecoding-chatqa 2 Icons from https://www.flaticon.com.

3 https://codeql.github.com/

FlowCheck: Helping End-Users Specify and Verify Intent in Vibe-Coded Web Apps

Components: The components of these constraints are strictly things that can be read from or written to, such as UI elements, database tables, and APIs. Actions: User actions (e.g. clicking) and system actions (e.g API call, page load). Reads and Writes: 𝑟 (), 𝑤 () over components. A write 𝑤 (𝑐) means that there is a value written to component c; read 𝑟 (𝑐) means that a value is read from component c. Sources: The sources of data for a component. This allows us to express a set of sources that a write must read from. For example, 𝑤 (𝑐, 𝑟 (𝑎) + 1) requires c to be written with value 𝑟 (𝑎) + 1, and 𝑤 (𝑐, 𝑠𝑜𝑢𝑟𝑐𝑒𝑠 = {𝑟 (𝑎), 𝑟 (𝑏)}) requires c to be written with a value derived from exactly this set of reads. Each constraint is a logical statement about whether an event occurs or not given a condition. The event either must always occur (𝑃 = 1) as in all paths from the action must result in the expected event, while 𝑃 = 0 means this should never happen given the action. These map to our all paths and no paths checks over the code. 5.3

LMPL ’26, October 4–9, 2026, Oakland, CA, USA

constraint = "P(" lex "|" lex ")" "=" NUM EOF lex = lex (OR | AND | XOR) lex | NOT lex | atom atom = write | action | call | persist | guard write = "w(" id ["," expr] ")" | "w(" id "," "sources=" srcset ")" action = "A(" id ")" // user action call = "call(" id ")" persist = "persist(" id ")" guard = expr cmp expr | expr IN range srcset = "{" [srcitem {"," srcitem}] "}" srcitem = "r(" id ")" expr = expr ("+" | "-" | "*" | "/") expr | "r(" id ")" | lit

Figure 2. Constraint syntax in extended Backus–Naur form, a simplified subset of our grammar; see Appendix A.1 for the full grammar.

Grammar

Our grammar focuses on parsing probabilistic constraints of the form: 𝑃 (𝑒𝑣𝑒𝑛𝑡 | 𝑎𝑐𝑡𝑖𝑜𝑛) = 𝑝𝑟𝑜𝑏𝑎𝑏𝑖𝑙𝑖𝑡𝑦. The action is the user or system event that the constraint is conditioned on, while the event is our expected outcome (e.g. write to a component or API call). It supports nested logic expressions (and/or/not/xor), user and system actions, reads/writes to components, and expected probabilities. Example 5.1. For example, 𝑃 (𝑤 (𝑐𝑎𝑟𝑡𝐶𝑜𝑢𝑛𝑡) | 𝐴(𝑎𝑑𝑑𝐶ℎ𝑎𝑟𝑔𝑒𝑟 )) = 1, means: Every time the user takes action of clicking the add charger button, we expect that the cartCount component is written to every single time (𝑃 = 1). This means that all execution paths from the addCharger event handler must write to the cartCount component with a probability of 1. While most of the grammar are standard logical and arithmetic expressions, the types of state and atomic operations are worth mention. There are three types of state that serve as primitives that expressions are built on: UI elements that the user can see, storage entries for local or session storage, and APIs for external services including external storage. The grammar uses the id to reference every identifier position. During semantic analysis, each id is classified as a UI element, storage entry, or API from the mapping, which we use to ensure the constraint is valid. Each corresponds to one part of the authoring interface in Figure 4. There are four atomic operations over this state: A write w() means a value is written to a component. It has optional constraints on the value or its sources. A user action A() names an event the user takes (e.g button clicks). A system

event call() represents an API invocation. A persist event persist() represents state that survives across reloads. The grammar permits actions and guards in any atom position, but our semantic analysis (Section 6.3) validates constraints and rejects those that put a user action or bare guard on the event side, or multiple actions on the condition side. 5.4

Expressiveness

We enumerated the kinds of user-visible constraints a user might want to express about a web app, by drawing from our formative study (Section 3.2), common failure patterns from prior work, and through experience building and interacting with these apps. We grouped them into three main categories: UI, API, and database constraints, covering the failures in our formative study (Section 3.2) as well as more general web app expectations. We found that 29 of the 34 specific constraint cases can be checked with static methods: 21 are fully checkable, and 8 are checkable partially by structurally verifying control- and dataflow paths while deferring exact value checking to runtime. Constraints that involve exact value checking or runtime timing require heavier-weight dynamic analysis that we leave to future work. As discussed above, every constraint consists of an action, an event, and user elements. Actions can express any user action or browser event over a visible HTML element. The user simply selects an element, and specifies the action with an optional guard. Events are what occur in response to actions, and can be any write, action, API call, storage interaction, or composition of these. Table 1 summarizes the main constraint patterns we encountered and express.

LMPL ’26, October 4–9, 2026, Oakland, CA, USA

Reya Vir, Lydia Chilton, Zhuo Zhang, and Eugene Wu

Table 1. Core expressiveness patterns of the constraint language. Pattern Basic state updates Writes from source Compound events Persistence API call Disallowed events

5.5

Description Link a user action to a basic write event. Restricts a constraint to be written from a specific source. Combines multiple expected events using logic operators. Requires that a specific action results in saved state across page reloads. Requires an action to trigger an API call. Target event must not occur.

From Constraints to CodeQL Queries

We compile each constraint into a set of the primitive queries of Table 2, together with a rule for combining their pass/fail results. Figure 3 defines this compilation as five translation functions, read top-down: TJ·K translates the whole constraint, CJ·K translates its condition side, EJ·Kℎ and RJ·Kℎ translate its event side, and VJ·K translates the value expressions that appear inside events. Table 2. The CodeQL primitive queries. Primitive path_exists all_paths_write literal_value source_set self_increment api_result_taint no_other_handlers call_reaches call_with_source page_load_restores guarded_write

What it checks ≥ 1 code path from the handler writes to target. Every exit path through the handler writes the target. The write assigns the literal value named in the constraint. Dataflow sources to the write same as expected set. Written value derives from 𝑟 ( target ) + constant. The written value taint-flows from a fetch/axios response. Only the named action writes to target. The handler reaches an invocation of the named function. r(source) flows to an argument of the call. A page-load handler calls getItem(key) for the storage key. The write is structurally inside an if reading the guarded element.

Constraints (TJ·K). The probability decides how the event side is checked. A 𝑃=1 constraint requires the event on every path, so its event is translated by EJ·Kℎ , whose primitives check all paths. A 𝑃=0 constraint forbids the event on any path, so its event is translated by RJ·Kℎ , which only asks whether the event is reachable at all; the constraint passes when it is not. For persist, this means the action handler never writes the storage key. Conditions (CJ·K). The condition side is translated once into the handler context ℎ from which every primitive query begins. In the common case, ℎ is simply handler (𝑎). The function handler (·) is not part of the constraint language, but an auxiliary function used by the translation: given the id 𝑎 of an interface element, it returns the event-handler function that the app registers on that element. handler (𝑎) resolves the id to its code references, including calls such as getElementById("addBtn") and the variables to which they are assigned (e.g., isElementRef predicate in the Appendix). We then identify the function attached to the element’s events. Each query on the event side searches only code reachable from that function.

Example P(w(cartCount) | A(addBtn)) = 1 P(w(total, r(promoInput)) | A(applyPromoBtn)) = 1 P(w(cartCount) AND w(cartItems) | A(addBtn)) = 1 P(persist(cartStorage) | A(addBtn)) = 1 P(call(productsAPI) | A(pageLoad)) = 1 P(w(cartCount) | A(applyPromoBtn)) = 0

A guard keeps the handler but records the guard, written ⟨handler (𝑎), 𝑔⟩; under this context a write must additionally sit inside a conditional that reads the guarded element (guarded_write). A negated action instead changes the context to handler (𝑎), and writes are checked using no_other_handlers so that only 𝑎 can write the target. The distinction between the two forms of negation appears directly in the rules. The constraint 𝑃 (𝑤 (𝑐) | 𝐴(𝑎)) = 0 asks whether 𝑎’s own handler can reach the write and passes when it cannot. By contrast, 𝑃 (𝑤 (𝑐) | NOT 𝐴(𝑎)) = 1 checks exclusivity, passing when no other handler reaches the write. Events (EJ·Kℎ ) and values (VJ·K). EJ·Kℎ follows the structure of the event expression and covers the three checkable event atoms: writes, calls, and persists. User actions and guards instead belong to the condition side and are handled by CJ·K. A plain write w(𝑒) produces two primitives: path_exists, requiring the write to be reachable from ℎ, and all_paths_write, requiring the write to occur on every path through the handler. A write includes either an assignment to the element (e.g., .textContent, .value) or a DOM mutation on it. Additional details in the atom add primitives to this base—for instance, a literal value adds literal_value, a value expression adds source_set. A call atom checks that the handler reaches the named API. When the atom names a source value, call_with_source checks both that the call is reachable and that the source flows into it. A persist atom checks both parts of persistence: the handler must save to the storage key using path_exists, and a page-load handler must read the value back using page_load_restores. Compound events are translated one operand at a time, after which their pass/fail results are combined using the Boolean operator in the constraint: AND as ∧, OR as ∨, XOR as ⊕, and NOT as ¬. Each primitive corresponds to one CodeQL query executed from entry point ℎ. The query returns a set of rows, with each row representing one match in the code, and the primitive interprets those rows as pass/fail. For example, path_exists passes when the query finds at least one reachable write. By contrast, all_paths_write searches for counterexample paths that exit without writing, and passes only when none exist. Finally, VJ·K does not evaluate arithmetic. It only collects the components read by a value expression, so r(𝑎) + r(𝑏) becomes the source set $a,b$. The checker verifies where a value comes from, rather than what the expression computes.

FlowCheck: Helping End-Users Specify and Verify Intent in Vibe-Coded Web Apps

LMPL ’26, October 4–9, 2026, Oakland, CA, USA

Constraint Translation

TJ·K TJP(𝐸 | 𝐶) = 1K = EJ𝐸KCJ𝐶 K

Condition Translation

CJA(𝑎)K = handler (𝑎)

TJP(𝐸 | 𝐶) = 0K = ¬ RJ𝐸KCJ𝐶 K

CJA(𝑎) AND 𝑔K = ⟨handler (𝑎), 𝑔⟩

CJ·K

CJNOT A(𝑎)K = handler (𝑎)

Event Translation

EJ·Kℎ EJw(𝑒)Kℎ = path_exists(ℎ, 𝑒) ∧ all_paths_write(ℎ, 𝑒) EJw(𝑒, 𝑘)Kℎ = EJw(𝑒)Kℎ ∧ literal_value(ℎ, 𝑒, 𝑘) EJw(𝑒, 𝑣)Kℎ = EJw(𝑒)Kℎ ∧ source_set(ℎ, 𝑒, VJ𝑣K) EJw(𝑒, sources=𝑆)Kℎ = EJw(𝑒)Kℎ ∧ source_set(ℎ, 𝑒, VJ𝑆K) EJw(𝑒, r(𝑒) + 𝑘)Kℎ = EJw(𝑒, r(𝑒))Kℎ ∧ self_increment(ℎ, 𝑒, 𝑘) EJw(𝑒, r(api_result))Kℎ = EJw(𝑒)Kℎ ∧ api_result_taint(ℎ, 𝑒) EJcall(𝑐)Kℎ = call_reaches(ℎ, 𝑐) EJcall(𝑐, 𝑣)Kℎ = call_with_source(ℎ, 𝑐, VJ𝑣K) EJpersist(𝑠)Kℎ = path_exists(ℎ, 𝑠) ∧ page_load_restores(𝑠) EJ𝐸 1 OR 𝐸 2 Kℎ = EJ𝐸 1 Kℎ ∨ EJ𝐸 2 Kℎ

EJ𝐸 1 AND 𝐸 2 Kℎ = EJ𝐸 1 Kℎ ∧ EJ𝐸 2 Kℎ

EJ𝐸 1 XOR 𝐸 2 Kℎ = EJ𝐸 1 Kℎ ⊕ EJ𝐸 2 Kℎ

EJNOT 𝐸Kℎ = ¬ EJ𝐸Kℎ

EJw(𝑒)K ⟨ℎ, 𝑔⟩ = EJw(𝑒)Kℎ ∧ guarded_write(ℎ, 𝑒, 𝑔)

EJw(𝑒)Khandler (𝑎) = no_other_handlers(𝑎, 𝑒)

Reachability Translation (for 𝑃 = 0) RJw(𝑒, . . . )Kℎ = path_exists(ℎ, 𝑒)

RJ·Kℎ RJ𝐸 1 𝑜𝑝 𝐸 2 Kℎ = RJ𝐸 1 Kℎ 𝑜c 𝑝 RJ𝐸 2 Kℎ

RJcall(𝑐, . . . )Kℎ = call_reaches(ℎ, 𝑐)

RJNOT 𝐸Kℎ = ¬ RJ𝐸Kℎ

RJpersist(𝑠)Kℎ = path_exists(ℎ, 𝑠) Value Translation (expected sources) VJr(𝑥)K = {𝑥 } VJ𝑘K = ∅

VJ·K VJ𝑣 1 𝑜𝑝 𝑣 2 K = VJ𝑣 1 K ∪ VJ𝑣 2 K

VJ{𝑣 1 , . . . , 𝑣𝑛 }K = VJ𝑣 1 K ∪ · · · ∪ VJ𝑣𝑛 K

Figure 3. The translation semantics from constraints to CodeQL primitive queries. Primitives are the queries of Table 2, run with handler context ℎ as their entry point; the auxiliary function handler (𝑎) resolves element id 𝑎 to the event-handler function the app registers on it. Metavariables: 𝑎 ranges over action elements, 𝑒 over element ids, 𝑠 over storage keys, 𝑐 over APIs, 𝑘 over literals, 𝑣 over value expressions, 𝑆 over source sets, 𝑔 over guards, and 𝐸, 𝐶 over event and condition expressions. When several E rules overlap, the most specific applies. In V, 𝑜𝑝 ∈ {+, -, *, /}; in R, 𝑜𝑝 ∈ {AND, OR, XOR} and 𝑜c 𝑝 is the corresponding Boolean connective (∧, ∨, ⊕). Example 5.2. Let ℎ = handler (applyPromoBtn). The promocode constraint from the introduction compiles by the rules of Figure 3 as: TJP(w(total, r(promoInput))| A(applyPromoBtn)) = 1K = EJw(total, r(promoInput))Kℎ = path_exists(ℎ, total) ∧ all_paths_write(ℎ, total) ∧ source_set(ℎ, total, {promoInput})

In the broken app, the handler writes only the success message, so all_paths_write returns counterexample paths that never write total, and the constraint fails. 5.6

Why We Chose This Design

Other formalisms like Hoare logic or Linear Temporal Logic can be more expressive, but are less accessible to non-developers. Writing our promo example in Hoare logic as {𝑃 } applyPromo() {𝑄 }, requires the user to write out the DOM state before and after, as well as read the code for internal function names and

variables. A non-developer, or vibe-coder, would not know these, and learning this would take as long as debugging manually. By restricting constraints to user-visible behavior, users express their expectations easily over their own app.

6

Implementation

To go from the app to verified constraints, we follow three steps: (1) preprocess the code to add identifiers (Section 6.1), (2) run the app for authoring constraints (Section 6.2), and (3) parse, validate, and verify the constraint (Section 6.3). 6.1

Preprocessing

Vibe-coded apps often lack identifiers for elements [12]. This creates two issues: (1) when authoring a constraint, we have no id to uniquely reference each element; (2) the id links the HTML and JS, which both reference the same DOM elements. To address this, we automatically map elements across both languages by scanning the source code to locate all UI elements (e.g. buttons and inputs), and adding unique

LMPL ’26, October 4–9, 2026, Oakland, CA, USA

Reya Vir, Lydia Chilton, Zhuo Zhang, and Eugene Wu

identifiers (cv_nnnn) where they are missing. This ensures every element has a static reference across both languages. We use BeautifulSoup to parse each HTML file and traverse the elements the user could select. For JS, we use regular expressions to identify programmatically created elements (such as createElement()), and append missing IDs. 6.2

User Interface

Users provide FlowCheck with their web app’s path, which opens in a new tab. Users express constraints on this app via our overlay template: “When I take [action], these update: [component]” with optional AND, OR, XOR, NOT logic. Users select visible UI components by clicking directly on them, the same way they interact with their app. They can also pick from a detected list of APIs and storage. As a result, the user does not need to learn the language syntax, identify internal variables for elements, or write constraints by hand. FlowCheck records the user’s actions, converts them to our constraint language, and sends them to the parser.

Figure 4. User authoring a constraint via the overlay. The user selects the promo input as the action and discount as a write target, then adds a second target (cart total, highlighted in green), to form a compound constraint. Users select visible components, without having to learn code or syntax. 6.3

Analysis

Once the user selects their components through the UI, their selections are translated into our constraint language, and compiled to static CodeQL queries in 4 steps: 1. Parsing: Constraints are parsed using an ANTLR4-generated parser into an AST, using our grammar from Section 5. 2. Semantic analysis: We walk the AST to extract the key parts (the event, condition, probability, and identifiers) and verify semantic rules: every referenced identifier must match a valid DOM element, storage identifier, or API,

Figure 5. Reviewing authored constraints. The Review panel lists the constraints the user has built, and dashed lines trace each constraint’s flows from action to event.

the condition side must contain an action 𝐴(𝑒𝑖 ), the event side must contain a valid effect (𝑤 (), 𝑐𝑎𝑙𝑙 (), 𝑝𝑒𝑟𝑠𝑖𝑠𝑡 ()), the probability must be 0 or 1, and identifiers in action must map to the “action” type. If rule fails, the constraint is invalid and exits with a detailed message to the user. 3. Classification: From this AST, we determine which primitive queries to run based on the event type and condition (Section 5.5). For example, an event containing an API node resolves to an API call check, while a write carrying a value expression resolves to a dataflow check. 4. Verification: Once we know which primitives to run, FlowCheck executes each corresponding CodeQL query– written in a .ql file with placeholder tokens replaced by element identifiers–against the database (Section 4). It reviews the returned rows to return a Pass/Fail result, and reports which queries failed for the user to review.

6.4

Authoring Constraints

Constraints can be generated in 2 ways: 1. User: The user can author constraints through our overlay UI, which lets a user click on elements in their running app and pick from constraint templates. For this, they do not need to know the constraint syntax or understand the code, only simple logic expressions (AND/OR/XOR/NOT). 2. LLM or Agent: We describe the language as a skill for an agent or LLM, containing the grammar, constraint types, and examples. Given the code, the app description, and this context, a model can produce a comprehensive list of constraints, which can combine with the user’s set for broader coverage. In Section 7.2.3 we find that models can author valid constraints and use them to catch more bugs.

FlowCheck: Helping End-Users Specify and Verify Intent in Vibe-Coded Web Apps

LMPL ’26, October 4–9, 2026, Oakland, CA, USA

7

Amazon

Evaluation

In our evaluation, we focused on two questions: (1) does FlowCheck catch the constraint violations it is designed to catch, and (2) how does it compare to asking a frontier LLM to find the same bugs? 7.1

Experiment Setup

7.1.1 Test Applications. Test applications were generated using Claude Code. We built four web apps, each modeled after an existing app (Amazon, Twitter, Airbnb, Slack). We chose well-known apps because they are real-world use cases, and models understand the expected features and behavior due to extensive training data. We used JS with no frameworks to stay within scope of static analysis, ensured all elements had IDs, and used local storage. We iterated on each app, adding features to create opportunities to write constraints. For example, a local database of items for Amazon, or a fees calculator for Airbnb. 7.1.2 Ground Truth and Injected Violations. We established 14–21 constraints per app representing the expected behavior (e.g. applying a promo code updates the total). We copied each app to modified/ variant and guided an agent to introduce 7–8 subtle violations, breaking about half the constraints, to simulate real-world development mistakes. These were inspired by documented coding-agent failure patterns [6], taxonomies of LLM-generated bugs [28], our formative study (Section 3.2), and by manually breaking or disconnecting components. Bugs covered several types, including missing branch write (if x then { write } with no else), switch missing a default case, write-with-wrong-source, and disconnected components. For example, in the modified Twitter app, post-tweet-btn writes the posted-banner even for empty inputs, dropping the character count check. The apps ranged from roughly 300 to 900 lines of code (HTML and JS), each with 16–26 action elements, 17–23 event handlers, and 5–11 localStorage operations. This added 30 behavioral violations across the four applications. We evaluated whether FlowCheck could correctly flag these constraint violations, and compared it against the LLM baselines. 7.1.3 Methods. We compared FlowCheck against asking a frontier LLM to find bugs in the same broken code. We tested three models: Claude Opus 4.7, DeepSeek V3, and Gemini Pro, using three prompt variants, increasing in detail (using a single run per model-prompt cell). Prompt 1: “Here is a web app, similar to [well known app]. Are there any bugs?” Prompt 2: Lists the features the user requested, e.g. “the user requested an Amazon like app with these features: a product grid, a cart drawer. . . ” Prompt 3: Same feature list as Prompt 2 plus an explicit edge-case checklist: boundary values, all user states, all branches, cross-handler consistency.

P1 Claude P2 P3

5

6

4

6

4

7

P1 3 DeepSeek P2 3 P3 1

7

24 26

8

17

5 15

6 5

5

Slack

24

6 7

7

6 6

Airbnb

7

5

4

4 P1 2 3 4 Gemini P2 2 2 4 P3 3 2

0

Twitter

7

19

12

3

12

4 5

14

10 15 20 Failures caught

25

30

Figure 6. Bug catch rate of FlowCheck compared to the LLM baselines (Claude, DeepSeek, Gemini) across the three prompt variants. FlowCheck flags all injected violations, while the best model–prompt pair reaches 26/30. 7.2

Results

FlowCheck catches all constraint violations, while LLMs were slower and less accurate, with the best model-prompt pair (Claude P3) reaching 26/30 and most results far lower (Figure 6). The results suggest that models are better at spotting localized bugs, a wrong literal or a missing write inside one handler, but struggle once bugs span multiple branches or handlers. Providing more detail in the prompt does not necessarily help; the models may read more of the code but not always find more of the bugs. 7.2.1 What Models Catch. Models reliably caught bugs localized to a small code block, whose patterns are relatively easy to recognize. For example, assigning an incorrect literal, or failing to update the UI on one conditional branch. Models also caught writes from the wrong data source (e.g. applypromo saving the old value instead of the user’s input) and partial persistence (e.g. storing favorites but not loading them on refresh). This was common in the Airbnb app, whose bugs largely involve localized writes that were missing or wrote the wrong key. Identifying these bugs does not require any control flow analysis or handler interaction. 7.2.2 What Models Miss. We found two dominant classes of violations that LLMs did not reliably identify. The first are universal quantifier constraints, where a property must hold over all paths, such as P=1 writes. Verifying these requires checking all branches, but models sometimes miss the branch where the write is dropped. For example, an Airbnb booking handler that updates the total cost only when guests ≤ 4, but leaves the other branch silently broken. The second are cross-handler flows, where one handler’s correctness

LMPL ’26, October 4–9, 2026, Oakland, CA, USA

depends on state written by another. These are difficult to detect because the bug is not visible in either handler alone, only when they interact. For example, Amazon’s checkout reads cartSummary but applyPromo clears it to 0. Since the handlers never reference each other, models reason on them separately and don’t trace the data flow between them. We found that adding detail to the prompt does not always help; all three prompt versions did not reliably catch errors across models. With more detail, models read code more thoroughly, but grew more willing to trust it, justifying bugs instead. For example, Amazon’s laptop favorite handler silently skips its write for one user tier, but a model dismissed this as intentional: "USER_TIER is a const initialized to ’free’, so the enterprise branch is dead code, not a defect."

Reya Vir, Lydia Chilton, Zhuo Zhang, and Eugene Wu

value is never parsed further. As a workaround, users can write constraints at the static container level. Frameworks like React and Vue have the same issue since they build UIs at runtime from a virtual DOM. This usually leaves the static HTML empty and FlowCheck cannot fully check them. Drag-and-drop is similar: implementations vary across the HTML5 drag API, touch events, and mouse movement, with no single code pattern, making it difficult to detect statically. 8.2

Future Work

Runtime Analysis: Our language supports probability values within [0, 1], but our implementation focuses on P=1 and P=0. Handling exact values and timing bugs (e.g., race conditions, API status codes) requires runtime data. We plan to address this using a browser agent to collect runtime traces, 7.2.3 Agents and our Constraint Language. We used verify constraints, and record the interactions that led to the the Amazon app as a probe to understand whether LLMs error to help debugging. can benefit from FlowCheck. We studied two questions: (Q1) Runtime tracing introduces variance because results decan agents author constraints? (Q2) does providing our lanpend on browser agent paths, raising open questions about guage and asking the model to write constraints help find action selection and modeling users, which is why we fomore bugs? To do so, we performed three runs; in each, we cused on static analysis first. A promising direction is a hyprompted each model with the grammar, a description of the brid approach: using static analysis for structural checks, and operators, example constraints, a description of the Amausing runtime tracing only for value or timing related checks. zon app, and the Amazon code, and asked it to generate a For example, the constraint 𝑃 (𝑤 (𝑒 𝑗 , len(𝑟 (api_result))) | comprehensive set of constraints to find bugs. We consider call(api)) = 1 expresses that a component ej must display a constraint valid if it parses and passes our semantic rules. the length of an API result. The static checker confirms the Q1. Per run, Claude, DeepSeek, and Gemini each genervalue written to ej derives from the API response length, and ated 30-60, 50-86, and 15-20 constraints. Of these, 45-100% runtime traces verify the resulting length matches. were valid for Gemini, 34-44% for Claude, and 41-65% for User Evaluation: While our evaluation demonstrates DeepSeek. Although they nearly all made sense conceptually, that FlowCheck can accurately detect injected failures, we their errors were finer: hallucinated names (e.g. dbPut_favorites),plan to conduct a user study with vibe-coders to evaluate syntax errors (underscore instead of dash), or the wrong atom language usability, how users interpret analysis results, and for an event (call(x) instead of A(x)). Since they expressed how they integrate them into their coding workflow. reasonable expectations and failed on syntax or identifiers, Iterative Vibe Coding: FlowCheck evaluates constraints this could likely be improved via more prompt engineering. on single code versions, but vibe coding is an iterative proQ2. The constraints helped models catch more of the silent cess where constraints change as apps grow. A key next step failures: compared to using their best prompt, Claude inis tracking and evolving constraints alongside code versions, creased from 5 → 6, DeepSeek from 3 → 5, and Gemini allowing coding agents to continuously generate, check, and from 3 → 4 out of 7 gold bugs. DeepSeek likely improved refine constraints and code throughout development. the most because it generated the most constraints. Among the bugs the models identified, Claude and Gemini produced 9 Conclusion no false positives, while DeepSeek produced 2-3 per run. We introduced a constraint language enabling users to exClaude and DeepSeek also identified other bugs out of scope press expected web-app behavior simply by pointing at the of FlowCheck. While this is not conclusive evidence, it is a app itself. We also introduced FlowCheck, a tool that verifies promising signal that providing a compact constraint lanthese constraints against their code through static analysis. guage can help improve bug catch rates. We do so by parsing the constraint, classifying the type, and mapping to a set of CodeQL queries that we then execute. 8 Limitations and Future Work In our evaluation, FlowCheck caught all 30/30 injected vi8.1 Limitations olations, compared to at most 26/30 for the strongest LLM CodeQL is a static analyzer that reads the code without runbaseline and fewer for the rest. Combined with the authoring ning, so it cannot link JS to DOM elements created at runtime. interface, this lets users of any programming background For example, elements built through strings (container. express and verify expectations deterministically, without innerHTML="...") hide the ids inside the string, since the needing to read or understand the code.

FlowCheck: Helping End-Users Specify and Verify Intent in Vibe-Coded Web Apps

References [1] Srijan Bansal, Jiao Fangkai, Yilun Zhou, Austin Xu, Shafiq Joty, and Semih Yavuz. 2026. VIBEPASS: Can Vibe Coders Really Pass the Vibe Check? arXiv:2603.15921 [cs.SE] https://arxiv.org/abs/2603.15921 [2] Earl T. Barr, Mark Harman, Phil McMinn, Muzammil Shahbaz, and Shin Yoo. 2015. The Oracle Problem in Software Testing: A Survey. IEEE Transactions on Software Engineering 41, 5 (2015), 507–525. doi:10. 1109/TSE.2014.2372785 [3] Islem Bouzenia, Premkumar Devanbu, and Michael Pradel. 2025. RepairAgent: An Autonomous, LLM-Based Agent for Program Repair. In Proceedings of the IEEE/ACM 47th International Conference on Software Engineering (Ottawa, Ontario, Canada) (ICSE ’25). IEEE Press, 2188–2200. doi:10.1109/ICSE55347.2025.00157 [4] M. Burnett, C. Cook, O. Pendse, G. Rothermel, J. Summet, and C. Wallace. 2003. End-user software engineering with assertions in the spreadsheet paradigm. In 25th International Conference on Software Engineering, 2003. Proceedings. 93–103. doi:10.1109/ICSE.2003.1201191 [5] Xinyun Chen, Maxwell Lin, Nathanael Schärli, and Denny Zhou. 2023. Teaching Large Language Models to Self-Debug. arXiv:2304.05128 [cs.CL] https://arxiv.org/abs/2304.05128 [6] DAPLab, Columbia University. 2026. 9 Critical Failure Patterns of Coding Agents. https://daplab.cs.columbia.edu/general/2026/01/08/9critical-failure-patterns-of-coding-agents.html. Data, Agents, and Processes Lab, Columbia University. [7] Francesco Dente, Dario Satriani, and Paolo Papotti. 2026. Constraint Decay: The Fragility of LLM Agents in Backend Code Generation. arXiv:2605.06445 [cs.SE] https://arxiv.org/abs/2605.06445 [8] Gordon Fraser and Andrea Arcuri. 2011. EvoSuite: automatic test suite generation for object-oriented software. In Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering (Szeged, Hungary) (ESEC/FSE ’11). Association for Computing Machinery, New York, NY, USA, 416–419. doi:10.1145/2025113.2025179 [9] Naman Jain, King Han, Alex Gu, Wen-Ding Li, Fanjia Yan, Tianjun Zhang, Sida Wang, Armando Solar-Lezama, Koushik Sen, and Ion Stoica. 2024. LiveCodeBench: Holistic and Contamination Free Evaluation of Large Language Models for Code. arXiv:2403.07974 [cs.SE] https://arxiv.org/abs/2403.07974 [10] Carlos E. Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, and Karthik Narasimhan. 2024. SWE-bench: Can Language Models Resolve Real-World GitHub Issues? arXiv:2310.06770 [cs.CL] https://arxiv.org/abs/2310.06770 [11] Amy J. Ko and Brad A. Myers. 2004. Designing the whyline: a debugging interface for asking questions about program behavior. In Proceedings of the SIGCHI Conference on Human Factors in Computing Systems (Vienna, Austria) (CHI ’04). Association for Computing Machinery, New York, NY, USA, 151–158. doi:10.1145/985692.985712 [12] Maurizio Leotta, Andrea Stocco, Filippo Ricca, and Paolo Tonella. 2016. Robula+: an algorithm for generating robust XPath locators for web testing. Journal of Software: Evolution and Process 28, 3 (2016), 177– 204. arXiv:https://onlinelibrary.wiley.com/doi/pdf/10.1002/smr.1771 doi:10.1002/smr.1771 [13] Michael Xieyang Liu, Advait Sarkar, Carina Negreanu, Benjamin Zorn, Jack Williams, Neil Toronto, and Andrew D. Gordon. 2023. “What It Wants Me To Say”: Bridging the Abstraction Gap Between EndUser Programmers and Code-Generating Large Language Models. In Proceedings of the 2023 CHI Conference on Human Factors in Computing Systems (Hamburg, Germany) (CHI ’23). Association for Computing Machinery, New York, NY, USA, Article 598, 31 pages. doi:10.1145/ 3544548.3580817 [14] Chang Lou, Peng Huang, and Scott Smith. 2020. Understanding, Detecting and Localizing Partial Failures in Large System Software. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20). USENIX Association, Santa Clara, CA, 559–574.

LMPL ’26, October 4–9, 2026, Oakland, CA, USA

https://www.usenix.org/conference/nsdi20/presentation/lou [15] Chang Lou, Yuzhuo Jing, and Peng Huang. 2022. Demystifying and Checking Silent Semantic Violations in Large Distributed Systems. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22). USENIX Association, Carlsbad, CA, 91–107. https: //www.usenix.org/conference/osdi22/presentation/lou-demystifying [16] Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, and Lei Bu. 2025. SpecGen: Automated Generation of Formal Program Specifications via Large Language Models. arXiv:2401.08807 [cs.SE] https://arxiv.org/abs/2401. 08807 [17] Ali Mesbah, Arie van Deursen, and Stefan Lenselink. 2012. Crawling Ajax-Based Web Applications through Dynamic Analysis of User Interface State Changes. ACM Trans. Web 6, 1, Article 3 (March 2012), 30 pages. doi:10.1145/2109205.2109208 [18] Ali Mesbah, Arie van Deursen, and Danny Roest. 2012. Invariant-Based Automatic Testing of Modern Web Applications. IEEE Transactions on Software Engineering 38, 1 (2012), 35–53. doi:10.1109/TSE.2011.28 [19] Jacqueline Mitchell and Yasser Shaaban. 2025. Position: Vibe Coding Needs Vibe Reasoning: Improving Vibe Coding with Formal Verification. In Proceedings of the 1st ACM SIGPLAN International Workshop on Language Models and Programming Languages (Singapore, Singapore) (LMPL ’25). Association for Computing Machinery, New York, NY, USA, 84–90. doi:10.1145/3759425.3763390 [20] Bao N. Nguyen, Bryan Robbins, Ishan Banerjee, and Atif Memon. 2014. GUITAR: an innovative tool for automated testing of GUIdriven software. Automated Software Engg. 21, 1 (March 2014), 65–105. doi:10.1007/s10515-013-0128-9 [21] Sydney Nguyen, Hannah McLean Babe, Yangtian Zi, Arjun Guha, Carolyn Jane Anderson, and Molly Q Feldman. 2024. How Beginning Programmers and Code LLMs (Mis)read Each Other. In Proceedings of the 2024 CHI Conference on Human Factors in Computing Systems (Honolulu, HI, USA) (CHI ’24). Association for Computing Machinery, New York, NY, USA, Article 651, 26 pages. doi:10.1145/3613904.3642706 [22] Liam O’Connor and Oskar Wickström. 2022. Quickstrom: propertybased acceptance testing with LTL specifications. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (San Diego, CA, USA) (PLDI 2022). Association for Computing Machinery, New York, NY, USA, 1025–1038. doi:10.1145/3519939.3523728 [23] Theo X. Olausson, Jeevana Priya Inala, Chenglong Wang, Jianfeng Gao, and Armando Solar-Lezama. 2024. Is Self-Repair a Silver Bullet for Code Generation? arXiv:2306.09896 [cs.CL] https://arxiv.org/abs/ 2306.09896 [24] Madison Pickering, Helena Williams, Alison Gan, Weijia He, Hyojae Park, Francisco Piedrahita Velez, Michael L. Littman, and Blase Ur. 2025. How Humans Communicate Programming Tasks in Natural Language and Implications For End-User Programming with LLMs. In Proceedings of the 2025 CHI Conference on Human Factors in Computing Systems (CHI ’25). Association for Computing Machinery, New York, NY, USA, Article 875, 34 pages. doi:10.1145/3706598.3713271 [25] Gregg Rothermel, Lixin Li, Christopher DuPuis, and Margaret Burnett. 1998. What you see is what you test: a methodology for testing form-based visual programs. In Proceedings of the 20th International Conference on Software Engineering (Kyoto, Japan) (ICSE ’98). IEEE Computer Society, USA, 198–207. [26] Max Schäfer, Sarah Nadi, Aryaz Eghbali, and Frank Tip. 2023. An Empirical Evaluation of Using Large Language Models for Automated Unit Test Generation. arXiv:2302.06527 [cs.SE] https://arxiv.org/abs/ 2302.06527 [27] Chuyue Sun, Ying Sheng, Oded Padon, and Clark Barrett. 2024. Clover: Closed-Loop Verifiable Code Generation. arXiv:2310.17807 [cs.AI] https://arxiv.org/abs/2310.17807 [28] Florian Tambon, Arghavan Moradi-Dakhel, Amin Nikanjam, Foutse Khomh, Michel C. Desmarais, and Giuliano Antoniol. 2025. Bugs in

LMPL ’26, October 4–9, 2026, Oakland, CA, USA large language models generated code: an empirical study. Empirical Softw. Engg. 30, 3 (Feb. 2025), 48 pages. doi:10.1007/s10664-025-10614-4 [29] Ningzhi Tang, Chaoran Chen, Gelei Xu, Yiyu Shi, Yu Huang, Collin McMillan, Tao Dong, and Toby Jia-Jun Li. 2026. How Coding Agents Fail Their Users: A Large-Scale Analysis of Developer-Agent Misalignment in 20,574 Real-World Sessions. arXiv:2605.29442 [cs.SE] https://arxiv.org/abs/2605.29442 [30] Runchu Tian, Yining Ye, Yujia Qin, Xin Cong, Yankai Lin, Yinxu Pan, Yesai Wu, Haotian Hui, Weichuan Liu, Zhiyuan Liu, and Maosong Sun. 2024. DebugBench: Evaluating Debugging Capability of Large Language Models. arXiv:2401.04621 [cs.SE] https://arxiv.org/abs/2401. 04621 [31] Hung Tran, Langston Nashold, Rayan Krishnan, Antoine Bigeard, and Alex Gu. 2026. Vibe Code Bench: Evaluating AI Models on End-to-End Web Application Development. In Proceedings of the ACM Conference on AI and Agentic Systems (CAIS ’26). Association for Computing Machinery, New York, NY, USA, 514–536. doi:10.1145/3786335.3813180 [32] Blase Ur, Elyse McManus, Melwyn Pak Yong Ho, and Michael L. Littman. 2014. Practical trigger-action programming in the smart home. In Proceedings of the SIGCHI Conference on Human Factors in Computing Systems (Toronto, Ontario, Canada) (CHI ’14). Association for Computing Machinery, New York, NY, USA, 803–812. doi:10.1145/2556288.2557420 [33] Mark Vero, Niels Mündler, Victor Chibotaru, Veselin Raychev, Maximilian Baader, Nikola Jovanović, Jingxuan He, and Martin Vechev. 2025. BaxBench: Can LLMs Generate Correct and Secure Backends? arXiv:2502.11844 [cs.CR] https://arxiv.org/abs/2502.11844 [34] Jian Wang, Xiaofei Xie, Qiang Hu, Shangqing Liu, and Yi Li. 2025. Do Code Semantics Help? A Comprehensive Study on Execution Trace-Based Information for Code Large Language Models. arXiv:2509.11686 [cs.SE] https://arxiv.org/abs/2509.11686 [35] Cheng Wen, Jialun Cao, Jie Su, Zhiwu Xu, Shengchao Qin, Mengda He, Haokun Li, Shing-Chi Cheung, and Cong Tian. 2024. Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification. arXiv:2404.00762 [cs.SE] https://arxiv.org/abs/2404.00762 [36] Valerie Zhao, Lefan Zhang, Bo Wang, Michael L. Littman, Shan Lu, and Blase Ur. 2021. Understanding Trigger-Action Programs Through Novel Visualizations of Program Differences. In Proceedings of the 2021 CHI Conference on Human Factors in Computing Systems (Yokohama, Japan) (CHI ’21). Association for Computing Machinery, New York, NY, USA, Article 312, 17 pages. doi:10.1145/3411764.3445567 [37] Xinyue Zuo, Yifan Zhang, Hongshu Wang, Yufan Cai, Zhe Hou, Jing Sun, and Jin Song Dong. 2025. PAT-Agent: Autoformalization for Model Checking. arXiv:2509.23675 [cs.SE] https://arxiv.org/abs/2509.23675

Acknowledgments We thank Zhou Yu for her guidance and Haonan Wang for helpful discussions. This research received funding from NSF 2103794, 2312991, 2551201 as well as DAPLab corporate support in the form of funding and/or compute from Amazon, IntellectAI, Infosys, Tidalwave, Veris, shopify, Microsoft, Thinking Machines, Dandy, Perplexity, and Daytona. The views and conclusions presented here are those of the authors and should not be interpreted as representing the official positions of the funding organizations.

A

Appendix

A.1

Constraint.g4 File

grammar Constraint;

Reya Vir, Lydia Chilton, Zhuo Zhang, and Eugene Wu

//

entry point

constraint : prob_constraint EOF ; prob_constraint : 'P(' logic_expr '|' logic_expr ')' probability_expr ; probability_expr : '=' NUMBER ; //

boolean logic

logic_expr : logic_expr OR logic_xor | logic_xor ; logic_xor : logic_xor XOR logic_term | logic_term ; logic_term : logic_term AND logic_factor | logic_factor ; logic_factor : NOT logic_factor | '(' logic_expr ')' | atom ; // atom

atoms : write_event | user_action | system_event | persist_event | guard | literal_bool ;

// Three w() forms: // w(t) — existence only // w(t, expr) — value from expr // w(t, sources={. . . }) — value from exact set write_event : 'w(' identifier ')' | 'w(' identifier ',' expr ')' | 'w(' identifier ',' 'sources=' source_set ')'

FlowCheck: Helping End-Users Specify and Verify Intent in Vibe-Coded Web Apps

; source_set : '{' source_item (',' source_item)* '}' | '{' '}' ; source_item : 'r(' identifier ')' | 'r(' 'api_result' ')' ; user_action : 'A(' identifier ')' ; system_event : 'call(' identifier ')' | 'call(' identifier ',' expr ')' ; persist_event : 'persist(' identifier ')' ; //

expressions

guard : expr comparator expr | expr IN range ; expr

term

: expr ('+' | '-') term | term ; : term ('*' | '/') factor | factor ;

factor : '(' expr ')' | atom_expr ; atom_expr : 'r(' identifier ')' | 'r(' 'api_result' ')' | 'len(' 'r(' identifier ')' ')' | 'len(' 'r(' 'api_result' ')' ')' | 'status(' identifier ')' | 'f(' expr ')' | literal ; //

terminals

LMPL ’26, October 4–9, 2026, Oakland, CA, USA

identifier : IDENTIFIER ; comparator : '=' | '!=' | '<' | '>' | '<=' | '>=' ; range : '[' NUMBER ',' NUMBER ']' | 'D' ; literal : NUMBER | STRING | 'null' ; literal_bool : TRUE | FALSE ; //

lexer rules

NOT : '¬' | '!' | 'NOT' ; AND : '∧' | '&&' | 'AND' ; OR : '∨' | '||' | 'OR' ; XOR : 'XOR' ; IN : 'in' ; TRUE : 'true' ; FALSE : 'false' ; // IDENTIFIER also accepts a leading '.' so class // selectors like `.wishlist-heart` parse as a // single token. Downstream layers // (semantic check, dispatcher) treat the // leading-dot form as a CSS class selector to // bind against dynamic per-instance elements. IDENTIFIER : '.'? [a-zA-Z][a-zA-Z0-9_-]* ; NUMBER : [0-9]+ ('.' [0-9]+)? ; STRING : '"' (~["\r\n])* '"' ; WS : [ \t\r\n]+ -> skip ;

A.2

Parts of CodeQL Primitives

Full CodeQL queries are on Github at: https://github.com/ reyavir/flowcheck isElementRef: This predicate is used to identify elements with the specified id, that are initialized in code using document.getElementById(id) or are referenced future uses. predicate isElementRef(string id, Expr ref) { // Direct: `document.getElementById(id)` exists(MethodCallExpr mc | mc = ref | mc.getMethodName() = "getElementById" and mc.getArgument(0).getStringValue() = id ) or // Cached: `const x = document.getElementById(id); exists(VariableDeclarator decl, MethodCallExpr getEl, Variable v | getEl = decl.getInit() and getEl.getMethodName() = "getElementById" and getEl.getArgument(0).getStringValue() = id and v = decl.getBindingPattern().(VarRef).getVariable() and ref.(VarRef).getVariable() = v ) }

Writes A write to the element is any property assignment on it, or a call to one of a small set of DOM-mutation methods, classList methods, or style methods. predicate writesElement(string id, AssignExpr write) { exists(PropAccess lhs | lhs = write.getLhs() and isElementRef(id, lhs.getBase()) ) } predicate writesElementVia(string id, MethodCallExpr call) { call.getMethodName() = [ "appendChild", "append", "prepend", "insertBefore", "replaceChild", "replaceChildren", "insertAdjacentElement", "removeChild", "remove", "setAttribute"

LMPL ’26, October 4–9, 2026, Oakland, CA, USA

}

] and isElementRef(id, call.getReceiver()) or // element.classList.{add,remove,toggle,replace}(...) exists(PropAccess classList | classList = call.getReceiver() and classList.getPropertyName() = "classList" and isElementRef(id, classList.getBase()) and call.getMethodName() = ["add", "remove", "toggle", "replace"] ) // (style.setProperty/removeProperty — omitted for space)

Reya Vir, Lydia Chilton, Zhuo Zhang, and Eugene Wu

A.3

LLM Rationalizations of Injected Bugs

With the most detailed prompt (P3), models often located an injected bug, but then dismissed it by reasoning, rather than flagging it. Examples from the Amazon app 1. "qty is clamped to ≥ 1, so the qty=0 path is unreachable; not a bug." 2. "the qty=99 cap is product-specific per the comment, so missing on other products is likely intentional"; and 3. "USER_TIER is a const initialized to ’free’, so the enterprise branch is dead code, not a defect." Received 2026-07-11; accepted 2026-08-14

Related documents

• FlowCheck: Helping End-Users Specify and Verify Intent in Vibe-Coded Web Apps#793115
• FlowCheck: Helping End-Users Specify and Verify Intent in Vibe-Coded Web Apps#789111
• From Prompting to Verification: How Experience Shapes Vibe Coding Practices#229597
• Vibe Coding in Product Teams: Reconfiguring AI-Assisted Workflows, Prototyping, and Collaboration#189345
• Beyond Coding: How Vibe Coding Reconfigures Software Development Work and the Professional Identity of Software Developers#1000534