Latest / 1 More Paper / FlowCheck: Helping End-Users Specify and Verify Intent in Vibe-Coded Web Apps — Vir et al. (2026)

Transcript

FlowCheck: Helping End-Users Specify and Verify Intent in Vibe-Coded Web Apps — Vir et al. (2026) · 1 More Paper

• You’re listening to “FlowCheck: Helping End-Users Specify and Verify Intent in Vibe-Coded Web Apps,” by Reya Vir and colleagues. Published in arXiv on August 28, 2026. Abstract. Vibe-coded applications often contain silent behavioral fail- ures 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 dis- played and inspected without reading code, and are struc- tured enough for reliable LLM generation. FlowCheck trans- lates 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. Introduction. Large language model (LLM) coding agents have democra-tized software development. End users with little program-ming 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 misunder-stand requests, omit necessary state updates, introduce in-correct data flows, or break previously working behavior. Prior work has documented incomplete implementations, regressions, and incorrect agent-generated code. Be-yond code-level errors, large-scale analysis of real coding-agent sessions shows that agents frequently break down on what users actually want. These Silent Behavioral Failures—the application runs but its observable behavior violates user intents—are especially difficult to detect when the application compiles, renders normally, and produces plausible feedback. A button may report success even though no data was saved, or a displayed value may update without reflecting the state it is supposed to represent. Existing debugging techniques like unit, integration, and end-to-end testing can validate behavior, but require users to identify test cases and encode the expected result as an executable oracle. LLM-based testing and debugging reduce the authoring burden, but we find these are probabilistic and limited in the types of failures they can identify. Tra-ditional static analysis and program verification techniques are deterministic for predefined program properties, but are designed for programmers rather than vibe coders. Vibe coders therefore need a way to express what they expect in terms of the interface they understand and to de-terministically check whether the implementation supports that behavior. We focus on web applications, where user 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 inter-face 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 analy-sis 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 promotional-code 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 ap-plying 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 ex-ecuting 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 vi-olations 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 models, and four iteration steps. From these, we identi-fied 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 and backend correctness constraints. We focus on silent behavioral failures: the application runs and presents plausible output, but user-visible information does not flow to the expected state or element. This differs from prior semantic failures by grounding correctness in end user’s expectations. LiveCodeBench and DebugBench evaluate self-contained problems with predefined input-output oracles, while SWE-bench evaluates patches to existing repositories. These benchmarks therefore do not capture expectations expressed through a newly generated application’s interface. Recent vibe-coding benchmarks evaluate complete applica-tions using browser agents or LLM judgments. How-ever, recent position work argues that vibe coding needs more deterministic checking; our formative study char-acterizes failures, while FlowCheck lets users state and de-terministically 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. Tools such as EvoSuite are able to pro-duce 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 gener-ators like TestPilot 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. 2.2 Specifications and LLM Debugging SpecGen, AutoSpec, Clover, and PATAgent use LLMs to gen-erate or formalize specifications and then apply verification tools. Their specifications describe code us-ing formal abstractions that non-programmers cannot easily inspect. Our language is intentionally less expressive: it de-scribes user-visible actions, elements, and information flows, can be authored and displayed within the application inter-face, 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 var-ious ways: by prompting it to explain and revise its own code, by using execution traces or semantic context, or more recently by treating the LLM as an autonomous agent that plans and invokes tools. However, self-repair gives inconsistent gains, and models are limited by their ability to provide actionable feedback on why code fails. Even where repair succeeds, it does not leave the user with a persistent, independently checkable statement of the in-tended 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. Quickstrom similarly checks user-facing behavior, but it uses a runtime approach, with specifications written in a temporal logic aimed at web programmers. Our constraints similarly describe application-level behavior, but are checked stati-cally 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 pro-gram 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. Trigger-action programming (TAP) further shows that if–then rules can be accessible to non-programmers. Recent work shows that natural language is difficult for users and programmers to state their intent. Vibe coders struggle with reading and evaluating correctness of LLM-generated code. 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. 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 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 open-weight model (DeepSeek V3), and a commercial vibe-coding system (Lovable). For each system, we generated four appli-cations 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 discon-nected 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 es-tablished in one iteration, disappeared after a later modifica-tion. All three systems dropped the rule that a speaker could occupy only one slot after a subsequent prompt allowed mul-tiple 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-to-effect 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. 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 A → B and then A → C silently rewrote the graph as A → C → B, 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, fa-vorites 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 perma-nently 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 re-lationships 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 han-dlers, 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 interface-grounded 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). CodeQL is a static code analysis engine3 that compiles source code into a relational database that models the ab-stract syntax tree, control-flow graph, and data-flow graph. We pre-process HTML separately in order to identify in-terface 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 in-terface, 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 condi-tioned on a single user action, motivated by the trigger-action 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. • 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. 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: r, w over components. A write w (c) means that there is a value written to component c; read r (c) 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, w (c,r (a) + 1) requires c to be written with value r (a) + 1, and w (c,sources = {r (a),r (b)}) 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 (P = 1) as in all paths from the action must result in the expected event, while P = 0 means this should never happen given the action. These map to our all paths and no paths checks over the code. 5.3 Grammar Our grammar focuses on parsing probabilistic constraints of the form: P (event | action) = probability. 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, P (w (cartCount) | A (addCharger)) = 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 (P = 1). This means that all exe-cution 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 arith-metic 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 po-sition. 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. 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 in-teracting 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 struc-turally verifying control- and dataflow paths while deferring exact value checking to runtime. Constraints that involve ex-act 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 com-position of these. Table 1 summarizes the main constraint patterns we encountered and express. 5.5 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 con-straint, CJ·K translates its condition side, EJ·Kh and RJ·Kh translate its event side, and VJ·K translates the value expres-sions that appear inside events. Constraints (TJ·K). The probability decides how the event side is checked. A P =1 constraint requires the event on every path, so its event is translated by EJ·Kh, whose primitives check all paths. A P =0 constraint forbids the event on any path, so its event is translated by RJ·Kh, 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 h from which every primitive query begins. In the common case, h is simply handler (a). The function handler (·) is not part of the constraint language, but an auxiliary function used by the translation: given the id a of an interface element, it returns the event-handler function that the app registers on that element. handler (a) 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. A guard keeps the handler but records the guard, writ-ten ⟨handler (a),g⟩; under this context a write must addi-tionally sit inside a conditional that reads the guarded ele-ment (guardedwrite). A negated action instead changes the context to handler (a), and writes are checked using nootherhandlers so that only a can write the target. The distinction between the two forms of negation appears directly in the rules. The constraint P (w (c) | A (a)) = 0 asks whether a’s own handler can reach the write and passes when it cannot. By contrast, P (w (c) | NOT A (a)) = 1 checks exclusivity, passing when no other handler reaches the write. Events (EJ·Kh) and values (VJ·K). EJ·Kh follows the struc-ture 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 han-dled by CJ·K. A plain write w(e) produces two primitives: pathexists, requiring the write to be reachable from h, and allpathswrite, 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 mu-tation on it. Additional details in the atom add primitives to this base—for instance, a literal value adds literalvalue, a value expression adds sourceset. A call atom checks that the handler reaches the named API. When the atom names a source value, callwithsource checks both that the call is reachable and that the source flows into it. A persist atom checks both parts of per-sistence: the handler must save to the storage key using pathexists, and a page-load handler must read the value back using pageloadrestores. Compound events are trans-lated 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 h. 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, pathexists passes when the query finds at least one reachable write. By contrast, allpathswrite 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(a) + r(b) becomes the source set $a,b$. The checker verifies where a value comes from, rather than what the expression computes. Constraint Translation TJ·K TJP(E | C) = 1K = EJEKCJCK TJP(E | C) = 0K = ¬ RJEKCJCK Condition Translation CJ·K CJA(a)K = handler (a) CJA(a) AND gK = ⟨handler (a), g⟩ CJNOT A(a)K = handler (a) Event Translation EJ·Kh EJw(e)Kh = pathexists(h,e) ∧ allpathswrite(h,e) EJw(e, k)Kh = EJw(e)Kh ∧ literalvalue(h,e,k) EJw(e, v)Kh = EJw(e)Kh ∧ sourceset(h,e, VJv K) EJw(e, sources=S)Kh = EJw(e)Kh ∧ sourceset(h,e, VJS K) EJw(e, r(e) + k)Kh = EJw(e, r(e))Kh ∧ selfincrement(h,e,k) EJw(e, r(apiresult))Kh = EJw(e)Kh ∧ apiresulttaint(h,e) EJcall(c)Kh = callreaches(h,c) EJcall(c, v)Kh = callwithsource(h,c, VJv K) EJpersist(s)Kh = pathexists(h,s) ∧ pageloadrestores(s) EJE1 AND E2Kh = EJE1Kh ∧ EJE2Kh EJE1 OR E2Kh = EJE1Kh ∨ EJE2Kh EJE1 XOR E2Kh = EJE1Kh ⊕ EJE2Kh EJNOT EKh = ¬ EJEKh EJw(e)K⟨h,g⟩ = EJw(e)Kh ∧ guardedwrite(h,e,g) EJw(e)Khandler (a) = nootherhandlers(a,e) Reachability Translation (for P = 0) RJ·Kh RJw(e...)Kh = pathexists(h,e) RJE1 opE2Kh = RJE1Kh c op RJE2Kh RJcall(c...)Kh = callreaches(h,c) RJNOT EKh = ¬ RJEKh RJpersist(s)Kh = pathexists(h,s) Value Translation (expected sources) VJ·K VJr(x)K = {x } VJ{v1..., vn }K = VJv1K ∪· · · ∪ VJvn K VJk K = ∅ VJv1 opv2K = VJv1K ∪ VJv2K Example 5.2. Let h = handler (applyPromoBtn). The promo-code constraint from the introduction compiles by the rules of Figure 3 as: TJP(w(total, r(promoInput))| A(applyPromoBtn)) = 1K = EJw(total, r(promoInput))Kh = pathexists(h, total) ∧ allpathswrite(h, total) ∧ sourceset(h, total, {promoInput}) In the broken app, the handler writes only the success mes-sage, so allpathswrite 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 {P } applyPromo {Q }, 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: preprocess the code to add identifiers (Section 6.1), run the app for authoring constraints (Section 6.2), and parse, validate, and verify the constraint (Section 6.3). 6.1 Preprocessing Vibe-coded apps often lack identifiers for elements. This creates two issues: when authoring a constraint, we have no id to uniquely reference each element; 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 identifiers (cvnnnn) 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. 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, the condition side must contain an action A (ei), the event side must contain a valid effect (w, call, persist ), 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 prim-. itive 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. 7 Evaluation In our evaluation, we focused on two questions: does FlowCheck catch the constraint violations it is designed to catch, and 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 gener-ated using Claude Code. We built four web apps, each mod-eled 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 be-havior 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 Ama-zon, 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, taxonomies of LLM-generated bugs, our formative study (Section 3.2), and by manually breaking or disconnecting components. Bugs covered several types, in-cluding 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. Methods. We compared FlowCheck against asking a 7.1.3 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. 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 spot-ting 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. apply-promo 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 re-quires 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 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 al-ways 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: "USERTIER is a const initialized to ’free’, so the enterprise branch is dead code, not a defect." 7.2.3 Agents and our Constraint Language. We used the Amazon app as a probe to understand whether LLMs can benefit from FlowCheck. We studied two questions: (Q1) can agents author constraints? (Q2) does providing our lan-guage and asking the model to write constraints help find more bugs? To do so, we performed three runs; in each, we prompted each model with the grammar, a description of the operators, example constraints, a description of the Ama-zon app, and the Amazon code, and asked it to generate a comprehensive set of constraints to find bugs. We consider a constraint valid if it parses and passes our semantic rules. Q1. Per run, Claude, DeepSeek, and Gemini each gener-ated 30-60, 50-86, and 15-20 constraints. Of these, 45-100% were valid for Gemini, 34-44% for Claude, and 41-65% for DeepSeek. Although they nearly all made sense conceptually, their errors were finer: hallucinated names (e.g. dbPutfavorites), syntax errors (underscore instead of dash), or the wrong atom for an event (call(x) instead of A(x)). Since they expressed reasonable expectations and failed on syntax or identifiers, this could likely be improved via more prompt engineering. User Evaluation: While our evaluation demonstrates that FlowCheck can accurately detect injected failures, we plan to conduct a user study with vibe-coders to evaluate language usability, how users interpret analysis results, and how they integrate them into their coding workflow. Q2. The constraints helped models catch more of the silent failures: compared to using their best prompt, Claude in-creased from 5 → 6, DeepSeek from 3 → 5, and Gemini from 3 → 4 out of 7 gold bugs. DeepSeek likely improved the most because it generated the most constraints. Among the bugs the models identified, Claude and Gemini produced no false positives, while DeepSeek produced 2-3 per run. Claude and DeepSeek also identified other bugs out of scope of FlowCheck. While this is not conclusive evidence, it is a promising signal that providing a compact constraint lan-guage can help improve bug catch rates. 8 Limitations and Future Work 8.1 Limitations CodeQL is a static analyzer that reads the code without run-ning, so it cannot link JS to DOM elements created at runtime. For example, elements built through strings (container. innerHTML="...") hide the ids inside the string, since the 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 val-ues within, but our implementation focuses on P=1 and P=0. Handling exact values and timing bugs (e.g., race con-ditions, API status codes) requires runtime data. We plan to address this using a browser agent to collect runtime traces, verify constraints, and record the interactions that led to the error to help debugging. Runtime tracing introduces variance because results de-pend on browser agent paths, raising open questions about action selection and modeling users, which is why we fo-cused on static analysis first. A promising direction is a hy-brid approach: using static analysis for structural checks, and using runtime tracing only for value or timing related checks. For example, the constraint P (w (e j, len(r (apiresult))) | call(api)) = 1 expresses that a component ej must display the length of an API result. The static checker confirms the value written to ej derives from the API response length, and runtime traces verify the resulting length matches. Iterative Vibe Coding: FlowCheck evaluates constraints on single code versions, but vibe coding is an iterative pro-cess where constraints change as apps grow. A key next step is tracking and evolving constraints alongside code versions, allowing coding agents to continuously generate, check, and refine constraints and code throughout development. 9 Conclusion We introduced a constraint language enabling users to ex-press expected web-app behavior simply by pointing at the app itself. We also introduced FlowCheck, a tool that verifies these constraints against their code through static analysis. We do so by parsing the constraint, classifying the type, and mapping to a set of CodeQL queries that we then execute. In our evaluation, FlowCheck caught all 30/30 injected vi-olations, compared to at most 26/30 for the strongest LLM baseline and fewer for the rest. Combined with the authoring interface, this lets users of any programming background express and verify expectations deterministically, without needing to read or understand the code. 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 corpo-rate support in the form of funding and/or compute from Amazon, IntellectAI, Infosys, Tidalwave, Veris, shopify, Mi-crosoft, 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; // entry point constraint: probconstraint EOF; probconstraint: 'P(' logicexpr '|' logicexpr ')' probabilityexpr; probabilityexpr : '=' NUMBER; // boolean logic logicexpr : logicexpr OR logicxor | logicxor; logicxor : logicxor XOR logicterm | logicterm; logicterm : logicterm AND logicfactor | logicfactor; logicfactor : NOT logicfactor | '(' logicexpr ')' | atom; // atoms atom : writeevent | useraction // Three w forms: // w(t) — existence only // w(t, expr) — value from expr // w(t, sources={... }) — value from exact set writeevent: 'w(' identifier ')' | 'w(' identifier ',' expr ')' | 'w(' identifier ',' 'sources=' sourceset ')' // lexer rules // 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: + ('.' +)?; STRING: '"' (~["\r\n]) '"'; WS: [ \t\r\n]+ -> skip; A.2 Parts of CodeQL Primitives Full CodeQL queries are on Github at: the linked source reyavir/flowcheck isElementRef: This predicate is used to identify elements with the specified id, that are initialized in code using docu-ment.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.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.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" ] 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) } 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. "USERTIER is a const initialized to ’free’, so the enterprise branch is dead code, not a defect."