Source-linked AI summary
FlowCheck: Helping End-Users Specify and Verify Intent in Vibe-Coded Web Apps
Reya Vir, Lydia Chilton, Zhuo Zhang, Eugene Wu
TL;DR
Vibe-coded applications can appear functional while user-visible information fails to reach the intended state or output. FlowCheck lets users specify those interface-level flows and compiles them into deterministic CodeQL checks. It detected all 30 injected violations, while the strongest LLM baseline detected at most 26/30.
Problem
Vibe-coded applications can run and present plausible feedback while silently violating user intent, and end users need interface-level ways to specify and verify expected behavior.
Method
FlowCheck lets users or LLMs author constraints over visible actions, elements, and effects, then translates them into static CodeQL analyses of control and data flow.
Results
100% detection accuracy was achieved on 30 injected failures, compared with at most 26/30 (87%) for the best LLM baseline.
Takeaways & Limitations
Users can state and inspect application intent through the interface and verify it deterministically against code without reading or understanding that code.
Takeaways & Limitations
CodeQL cannot link JavaScript to DOM elements created dynamically through strings, limiting analysis of such runtime-generated elements.
Abstract
from arXiv · showhide
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.
1 Introduction
Vibe-coded applications can appear functional while violating users’ intended information flows, creating failures that conventional approaches do not make easy for end users to specify and verify. FlowCheck addresses this gap with interface-grounded constraints compiled into deterministic static analyses.
- Motivation: Vibe-coded applications can run and display plausible feedback while observable behavior violates user intent.Examples include success messages without saved data and displayed values disconnected from underlying state.
- Motivation: Existing testing requires users to encode expected results as executable oracles, while LLM-based debugging is probabilistic and traditional static analysis targets programmers.These approaches either impose specification burdens or do not fit vibe coders’ interface-centered reasoning.
- Approach: FlowCheck lets users express constraints over visible elements, actions, interface updates, persistent state, and backend calls.The constraints can require, prohibit, or relate user-visible effects and information flows.
- Approach: FlowCheck compiles user- or LLM-authored constraints into CodeQL queries that check control-flow and data-flow relationships.The system reports which constraints pass or fail without executing the application.
- Evaluation: 100% detection accuracy was achieved on 30 injected failures, compared with at most 26/30 (87%) for the best LLM baseline.The evaluation covered four web applications, with 14–21 constraints per application.
2 Related Work
Prior work addresses generated-code correctness through benchmarks, testing, runtime interaction, formal specifications, and LLM debugging, but these approaches often rely on predefined oracles, programmer-oriented abstractions, probabilistic judgments, or execution. FlowCheck instead grounds specifications in user-visible interface flows and checks them statically.
- Benchmarks and testing: Existing coding benchmarks use predefined input-output oracles or repository patches and do not capture expectations expressed through newly generated application interfaces.Vibe-coding benchmarks use browser agents or LLM judgments, while recent work calls for more deterministic checking.
- Benchmarks and testing: Automated and LLM-based test generation can inherit the current implementation’s behavior rather than encode what the application should do.This is the oracle problem: generated assertions may reflect existing code instead of intended behavior.
- Specification systems: Formal specification systems use abstractions that non-programmers may not easily inspect, whereas FlowCheck describes visible actions, elements, and information flows.FlowCheck deliberately sacrifices expressiveness for interface authorability, displayability, and LLM generation.
- LLM debugging: LLM-based debugging and repair can provide inconsistent gains because models may struggle to produce actionable explanations of why code fails.FlowCheck’s deterministic violation reports are aimed at making intended behavior and failure locations inspectable.
- Runtime testing: Runtime web-testing systems check interaction sequences or DOM states by executing applications, while FlowCheck checks information-flow relationships statically without crawling or running them.The distinction concerns runtime interaction versus structural static analysis.
3 Formative Study: Vibe Coding Failures
A formative study of vibe-coded applications found recurring silent failures in visible behavior, persistence, and state relationships across models and iterative development stages. Eleven of 23 failures shared non-local action-to-effect relationship errors, motivating interface-grounded, mechanically checkable constraints.
- 3 Formative Study: Vibe Coding Failures: 23 distinct failures were observed across four applications and three coding systems, with every application and system exhibiting at least one failure.The study used four scripted stages: initial generation, feature addition, refactoring, and feature modification.
- 3.1 Methodology: The study covered a speaker scheduler, task-board whiteboard, shopping application, and image gallery generated under fixed prompts using plain JavaScript.The applications were manually checked against expectations recorded before generation.
- 3.2 Observed Failures: Surface-level correctness failures disconnected visible outputs from the data or action they claimed to represent.Examples included incorrect image openings and promo totals that ignored the input or cart contents.
- 3.2 Observed Failures: Task-board conversions caused cards to lose visible status, while a dependency editor overwrote an existing relationship instead of preserving it.Adding A→B and then A→C silently rewrote the graph as A→C→B.
- 3.2 Observed Failures: Incomplete persistence caused favorites to be associated with positions rather than image identities and caused speaker data to disappear after reload.The failures respectively persisted the wrong source and omitted the save-and-restore path.
- 3.2 Observed Failures: The same patterns appeared in public vibe-coding transcripts, including missing database tables and an interface stuck at “loading.”These observations extended the study’s failure patterns beyond its generated applications.
- 3.2.1 Summary of Findings: 11 of 23 failures involved missing or incorrect relationships between a user action and an observable effect.These relationships spanned event handlers, control flow, DOM updates, and storage operations, making them non-local in code but visible to users.
4 System Overview
FlowCheck lets users author expected behavior through the running application and checks the resulting constraints against source code. Its workflow preprocesses code, compiles constraints into CodeQL analyses, and returns pass/fail results.
- Authoring: Users author constraints by selecting interface elements, actions, and storage state, then specifying the expected flows between them.This interaction uses the application interface rather than requiring users to inspect code.
- Workflow: The workflow preprocesses application code, supports user or agent constraint authoring, and compiles constraints into static analyses that return pass/fail results.These are the system’s three stated workflow steps.
- Static analysis: The core engine compiles authored constraints into CodeQL primitives, runs them to find violations, and outputs passed or failed constraints.This pipeline connects interface-level specifications to deterministic source-code analysis.
- Static analysis: CodeQL preprocesses source code into a relational database modeling syntax, control flow, and data flow for later queries.HTML is separately preprocessed to identify interface elements.
5 Constraint Language
FlowCheck expresses user-visible behavior as constraints over actions, events, components, and data sources, then compiles those constraints into deterministic CodeQL checks. Its probability semantics distinguish events required on every path from events forbidden on any path.
- Design principles: FlowCheck constrains observable UI elements, storage, and APIs so users can specify expected behavior in interface terms.The design emphasizes observability and supports constraints that are also intended to be easy for LLMs to generate.
- Constraint model: Each constraint conditions an expected event on one user or system action, with support for reads, writes, persistence, API calls, guards, and logical composition.Events may combine writes, actions, API calls, storage interactions, or compositions of these.
- Constraint semantics: P=1 requires the event on every execution path, whereas P=0 requires that the event be unreachable.These cases map to all-paths and no-paths checks over the application code.
- Expressiveness: The language covers UI, API, and database constraints, with 29 of 34 identified cases statically checkable, including 21 fully and 8 partially.The categories were derived from formative-study failures, prior work, and experience with web applications.
- Translation to CodeQL: FlowCheck compiles constraints into primitive CodeQL queries that check reachability, all-path writes, literals, dataflow sources, API taint, exclusivity, and calls.The translation uses condition, event, and value functions, with queries evaluated from the action handler context.
- Example: In the broken promotional app, all_paths_write found paths that wrote only the success message and never updated the total, so the constraint failed.This demonstrates how a visible information-flow expectation becomes a counterexample-producing static check.
6 Implementation
FlowCheck preprocesses applications, lets users author constraints through an overlay, and validates and compiles those constraints into CodeQL analyses. The interface supports direct selection of visible elements while also allowing constraints to be generated by LLMs or agents.
- Pipeline: The implementation pipeline preprocesses code, runs the app for constraint authoring, then parses, validates, and verifies each constraint.These are the three high-level steps from the application to verified constraints.
- Preprocessing: Preprocessing adds unique identifiers to HTML and programmatically created elements so interface elements can be referenced consistently across HTML and JavaScript.This addresses missing identifiers and links DOM elements to their code references.
- User interface: The overlay lets users select visible UI components directly and choose detected APIs or storage without learning syntax, internal variables, or code.FlowCheck records those selections and converts them into the constraint language.
- Analysis: The analysis pipeline parses constraints into an AST, checks identifiers and semantic rules, classifies the required primitive queries, and compiles them for verification.Invalid constraints produce detailed user-facing messages rather than proceeding to analysis.
- Constraint generation: Constraints can be authored through the overlay or generated by an LLM or agent using the grammar, constraint types, and examples as a skill description.The two generation routes can be combined with user-authored constraints.
7 Evaluation
FlowCheck was evaluated on four modified web applications containing injected behavioral violations and compared with three frontier LLMs across three prompt variants. FlowCheck caught every constraint violation, while model performance varied substantially and was weakest on violations requiring broader control- or data-flow reasoning.
- Evaluation Setup: The evaluation tested whether FlowCheck catches designed violations and how it compares with frontier LLM bug finding.The study used four web applications, injected violations, and three models with three prompt variants.
- Overall Results: FlowCheck flagged all injected violations, while the best model–prompt pair reached 26/30.The comparison covered Claude, DeepSeek, and Gemini across three prompt variants.
- What Models Catch: Models more reliably caught localized bugs involving incorrect literals, missing branch writes, wrong data sources, or partial persistence.These failures generally did not require control-flow analysis or interaction between handlers.
- What Models Miss: Models often missed universal-quantifier violations because checking all branches is required to verify properties such as P=1 writes.One example updates booking cost only when guests ≤4, leaving another branch silently broken.
- What Models Miss: Models also struggled with cross-handler flows because the relevant bug appears only when state written by one handler is consumed by another.In the Amazon example, checkout reads cartSummary after applyPromo clears it to 0.
- Prompt Variants: Adding prompt detail did not reliably improve bug finding across models.More detailed prompts led models to inspect more code but sometimes trust or rationalize defective behavior instead.
8 Limitations and Future Work
The paper identifies limitations in FlowCheck’s static analysis and evaluation scope, and outlines future work for user studies and evolving constraints across iterations.
- 8.1 Limitations: CodeQL cannot link JavaScript to DOM elements created at runtime, limiting analysis of dynamically constructed interfaces.Elements created through strings such as innerHTML can hide element identifiers from static analysis.
- 8.1 Limitations: A future user study will evaluate language usability, interpretation of analysis results, and integration into vibe-coding workflows.
- 8.1 Limitations: FlowCheck currently evaluates constraints on single code versions, while iterative vibe coding changes both applications and constraints over time.Future work proposes tracking and evolving constraints alongside code versions.
9 Conclusion
FlowCheck lets users express expected web-application behavior through the interface and verify it against code using static analysis. In evaluation, it caught all injected violations, outperforming the strongest LLM baseline reported.
- FlowCheck parses constraints, classifies their types, maps them to CodeQL queries, and executes those queries against the code.
- 30/30 injected violations were caught by FlowCheck, compared with at most 26/30 for the strongest LLM baseline.
- The interface and static verification allow users of any programming background to express and verify expectations without reading or understanding code.
A.1 Constraint.g4 File
The Constraint.g4 file defines the grammar for FlowCheck constraints, including logical expressions, events, reads, writes, persistence, comparisons, literals, identifiers, and whitespace.
- The grammar supports OR, XOR, AND, and NOT composition for logical expressions, including parenthesized expressions and boolean literals.
- The grammar represents user actions, system events, persistence events, guards, and boolean literals as atomic constraint elements.
- Write events support existence checks, values derived from expressions, and values constrained to an exact source set.
- Identifiers, comparators, ranges, literals, and logical operators are explicitly tokenized, with identifiers optionally accepting a leading dot for CSS class selectors.
- Whitespace is skipped during parsing.
A.2 Parts of CodeQL Primitives
The CodeQL primitives define how FlowCheck identifies interface elements and recognizes writes or DOM mutations in application code.
- FlowCheck provides the full CodeQL queries through its GitHub repository.
- The isElementRef predicate identifies elements by direct getElementById calls or cached references derived from them.
- An element write includes property assignments and selected DOM-mutation, classList, and style-method operations.
- A.3 LLM Rationalizations of Injected Bugs: Models sometimes located injected bugs but dismissed them through reasoning instead of flagging them.Examples treated unreachable branches, product-specific behavior, or dead code as intentional rather than defective.