Latest / 1 More Paper / Position: Vibe Coding Needs Vibe Reasoning: Improving Vibe Coding with Formal Verification — Mitchell & Shaaban (2025)
Transcript
- You’re listening to “Position: Vibe Coding Needs Vibe Reasoning: Improving Vibe Coding with Formal Verification,” by Jacqueline Mitchell and Yasser Shaaban. Published in Proceedings of the 1st ACM SIGPLAN International Workshop on Language Models and Programming Languages on October 9, 2025. Abstract. “Vibe coding” — the practice of developing software through iteratively conversing with a large language model (LLM) — has exploded in popularity within the last year. However, de- velopers report key limitations including the accumulation of technical debt, security issues, and code churn to achieve satisfactory results. We argue that these pitfalls result from LLMs’ inability to reconcile accumulating human-imposed constraints during vibe coding, with developers inadver- tently failing to resolve contradictions because LLMs pri- oritize user commands over code consistency. Given LLMs’ receptiveness to verification-based feedback, we argue that formal methods can mitigate these pitfalls, making vibe cod- ing more reliable. However, we posit that integrating formal methods must transcend existing approaches that combine formal methods and LLMs. We advocate for a side-car system throughout the vibe coding process which: Autoformal- izes specifications Validates against targets, Delivers actionable feedback to the LLM, and Allows intuitive developer influence on specifications. CCS Concepts: • Software and its engineering → Soft- ware creation and management; • Theory of computa- tion → Logic and verification; • Computing methodolo- gies → Machine learning. Introduction. Modern LLMs have made vibe coding — writing software by conversing with an LLM — an appealing new workflow, granting developers the ability to rapidly prototype and re-fine code by prompting an LLM. In the context of soft-ware development (and developing a mature codebase), vibe coding is a long-range iterative venture, guided by human feedback. Over time, the user’s requirements accumulate as natural language constraints on the system. These con-straints may be inconsistent (e.g., conflicting design goals) due to human error, evolving goals, or contradictory instruc-tions from the user. In fact, developers have reported dealing with accumulated technical debt (and security issues) that compound over time. In extreme cases, developers report falling into the so-called “pit of despair,” a state where starting over is easier than untangling inconsistencies in the code. LLM-generated code may also contain security flaws: a recent repository-level evaluation of 318 benchmark programs shows that the strongest model generates secure and correct code at a rate of only 28%. Formal verification is increasingly used to check security properties in LLM-generated code. It can au-tomatically assess safety and intended behavior, making it attractive for vibe coding. However, the ability to verify spec-ifications against LLM-generated code is only one part of the battle. The burden of writing and maintaining application-specific specifications (i.e., beyond simple checks, such as making sure the code type-checks) falls upon developers and grows more burdensome with rapid iteration on the code. Furthermore, even prior to vibe coding, industry re-ports show that it is difficult to get developers to adopt static analysis in their workflows. This paper argues that formal methods can improve vibe-coded software, provided the integration is developer-first. We propose Vibe Reasoning: a system that autoformalizes application-specific verification targets, verifies them with the lightest effective techniques, provides feedback that leads to actionable fixes, and keeps developers in control in a way where human involvement is collaborative, instead of an overhead. Unlike typical autoformalization or full-program verification, it iteratively and automatically checks only crit-ical invariants. 2 Challenges in Vibe Coding This section outlines the vibe coding process in more detail, emphasizing the key challenges. Figure 1 depicts a possible vibe coding workflow. While vibe coding, developers typi-cally: request new features or revisions (e.g., refactoring) or when they find bugs or misalignment with their intent, either ask the LLM to fix them or revert to a prior version and continue. The user’s demands accumulate in the form of natural language constraints (φ0,φ1,...). Over time, these constraints may drift or conflict, leaving the code in an in-consistent, buggy, and complex state, as reported by develop-ers. Common complications include: Constraint Inconsistency, where a new feature silently contradicts existing behavior; Partial-propagation Bugs, where a change (e.g., in a schema or input-sanitization) is applied in one module, but not others, leading to errors (e.g., crashes or data-corruption); State-machine Divergence. For example, when a UI or protocol logic acquires new states or transitions in one part of the codebase, but the transitions are not globally updated, leading to crashes or illegal states; Duplication Debt, where multiple LLM-generated variants of a routine evolve separately, ballooning technical debt. These patterns mirror technical debt patterns in machine learning-based coding systems, including entanglement (changing any input affects all outputs), hidden feedback loops, undeclared consumers (components that silently de-pend on changed behavior), and correction cascades (multi-ple versions of similar code evolve independently), described by Sculley et al.. In vibe coding, these patterns are am-plified by the rapid development style and the developer’s limited visibility of the generated code’s interdependencies. Vibe coding also compresses the development cycle: projects that once required teams can now be done solo, removing review-driven guardrails and other implicit constraints. The solo developer must choose when and how to refactor (e.g., apply Single Responsibility Principle) while managing grow-ing branches that hide latent conflicts and hard-to-fix bugs. Balancing developer intent, evolving constraints, and code-base consistency demands systematic planning and reconcil-iation, capabilities which LLMs currently lack. Kambhampati et al. argue that LLMs optimize for local plausibility (pat-tern completion) rather than combinatorial planning needed for global consistency, so they struggle to reconcile evolving constraints over long horizons. This results in constraint-reconciliation decay: as sessions lengthen and dependen-cies accumulate, success rates fall. This is supported by sev-eral studies: Multi-turn coding benchmarks show that per-formance steeply declines compared to single-turn tasks, dominated by failures to globalize changes across helpers and state. Repository-level evaluations reveal similar cross-file integration and dependency breaks. Success of agentic systems on static benchmarks (SWE-bench Verified) do not carry over to dynamic, evolving tasks (SWE-bench-Live). Further, relying on expanded “memory” is also insufficient; benchmarks show that long-term recall is unreliable and degrades under complexity, accu-mulating contradictions rather than ensuring consistency. 3 Why Formal Methods in Vibe Coding? Despite the difficulties LLMs face with planning, they readily incorporate explicit, well-structured human feedback. In Figure 1, at each iteration, the user provides feedback in the form of natural language. Generally, the LLM adjusts accordingly (possibly in an ad-hoc manner) to immediate feedback. The task of generating this feedback falls upon the user, who must manually test or inspect the code, and triage what to test and when, which becomes cumbersome. Offloading the burden to LLM-written tests is not ideal either. Test suites must evolve with the code, and the developer must ensure that the tests reflect their intent and are consistent with the codebase. Achieving high coverage often requires many tests whose maintenance can be more complex than that of the codebase itself. Running the tests can take a long time, and even a high pass rate cannot guarantee the absence of important classes of bugs. Formal methods can guarantee the absence of bugs, for-malize design constraints, and model and verify system-wide invariants and dependencies. This makes their integration into vibe coding compelling, especially given the systemic nature of ML technical debt. Many existing works com-bine LLMs and formal methods, highlighting the ability of LLMs to effectively incorporate feedback from a verification engine. The next subsection classifies these approaches and argues for the need for a developer-first integration that transcends existing systems. 3.1 Type I and Type II Systems Work at the intersection of formal methods and LLMs for synthesis can largely be classified into two types. Type I systems (Figure 2, left) use formal methods to filter out solu-tions that do not satisfy a certain specification, and provide feedback (e.g., a counterexample) to the LLM, iterating until a valid solution is reached (e.g., loop-invariant synthesis with formal tools in the loop, static analysis-guided repair ). Type II systems (Figure 2, right) use formal methods to post-process LLM outputs so that it satis-fies specifications by construction (e.g., constrained decoding, program completion ). Both systems rely on humans to supply formal methods components (e.g., specifications). In a vibe coding workflow, verification targets may need to evolve over time; developers must decide how to convey the feedback to the LLM (Type I) or integrate post-processed results into the codebase (Type II). Then, the user must ensure that the code remains in a consistent state, which may be very burdensome. Thus, we advocate for a system (Type III), which incorporates formal methods in a way such that human involvement becomes collaborative, rather than an overhead cost. 4 The Type III Vibe Reasoning Trifecta We specify an autonomous (agentic ) system centered on developer ease and collaboration. Figure 3a shows the high-level Vibe Reasoning loop, where the system runs alongside vibe coding (abstracted from Figure 1). Figure 3b describes the Type III side-car, which manages verification, autofor-malization, and user-feedback integration. Each block in Figure 3b denotes an event (e.g., requesting user feedback on a verification target or autoformalizing a specification). Red arrows represent failures (e.g., failure to verify), and com-municate that information to various parts of the system. The structure of this section follows the core components of the side-car: Autoformalizing Specifications, Continuous Verification, and Integration (of human and verifier feedback). 4.1 Autoformalizing Specifications The goal is to convert developer intent and good coding prac-tices (e.g., maintainability and security) into formally veri-fiable specifications. Some specifications are universal and tool-discoverable, including exhaustive variant handling (e.g., TypeScript’s assertNever, Kotlin sealed classes), Effect-Dependency soundness (e.g., React’s exhaustive-deps lin-ter), and Parameterized SQL Enforcement (e.g., CodeQL, which detects unescaped concatenation). The system should be able to apply these checks as needed. Two key challenges in autoformalization are Creating high-quality application-specific verification targets aligned with explicit (e.g., a specification that guarantees the absence of a discovered bug) and implicit (e.g., inventory in an e-commerce system is never negative) developer intent to limit technical debt and security risks. Managing the constraints accumulated over time: new specifications may contradict earlier ones, or the number of specifications may be unwieldy. Promising Directions: LLM-based autoformalization for verification shows promise, across a variety of application domains. In the context of vibe coding, the goal is to map explicit and implicit intent (in the form of natural language) into formally verifiable or checkable specifica-tions. Recent works suggest possible directions for achieving high-quality autoformalizations with LLMs. Internal Coher-ence Maximization is an unsupervised search technique that selects mutually predictable and logically self-consistent LLM responses. Another work uses probabilistic consensus for response selection and argues that unanimous consen-sus amongst several independent LLMs can serve as proxies for ground truth. Zhou et al. demonstrate that an LLM can generate high-quality tasks via Code-as-Task bundles which pair natural language goals with an executable verifier function that can automatically validate task completion and provide feedback to improve model performance. For Type III, future work should explore if ensembles of LLMs can propose and select formal verification targets beyond test suites and if they can maintain the verification environ-ment over time (e.g., deciding to keep or retire specifications) and consider feedback from failed builds (Figure 3a). Human Collaboration: Of course, LLM-generated speci-fications may not fully align with developer intent. Thus, we advocate for a human-in-the-loop component. Prior work shows improved trust in users when they participate in veri-fication. VeriPlan lets end-users approve logical rules (in natural language) and choose which to enforce as hard or soft constraints. For vibe coding, the system could present specifications in natural language with an explanation of their impact on the codebase and trade-offs, then let users approve, reject, or request changes. This could address the second challenge: users can resolve conflicting design re-quirements by selecting specifications that meet their needs. 4.2 Continuous Verification Once selected, specifications are used as verification targets throughout the vibe coding process, to be validated by appro-priate tools (chosen by the system). The system must decide which tools to use to verify the specifications. Challenge: A key challenge in continuous verification is that the scale at which verification is used must match development pace. Verification techniques that are too slow may be undesirable. The system must make trade-offs by fo-cusing on core components, preferring lightweight analyses when possible, and prioritizing the most important targets. Promising Directions: Agentic techniques have been shown to be effective at external tool selection. The system could leverage these techniques, use knowledge about the trade-offs of different verification techniques, or rewrite components of code to be more verification-friendly. Human Collaboration: Users may wish to weigh in on the cost-benefit of verifying specific targets. The system could explain benefits in natural language and allow users to continue or stop verification (e.g., when the runtime is too high) and to request alternative specifications when the verification conflicts with their pace. 4.3 Integration The last tenet is effectively integrating feedback from a ver-ifier to the LLM. Typically, this is done by providing the feedback to the LLM using prompts, which has been shown to be generally effective in Type I systems. If the LLM is unable to fix the code to satisfy a certain specification, Type II techniques may be invoked; when applicable, the system could select and apply a Type II technique to ensure that the generated component satisfies the specification. Challenge: Incremental modifications to the codebase are not guaranteed to be fool-proof. Edits made to satisfy one specification may regress another. Promising Directions: The side-car could incrementally incorporate verifier feedback as part of the compile/build process (Figure 3b), ensuring accumulated constraints (the specifications) are enforced. Human Collaboration: To involve the developer, the sys-tem could present proposed changes, with natural-language explanations, for approval or rejection. If integration to sat-isfy a specification takes too long, the user may relax it to a soft constraint, to steer development without enforcing a strict requirement. 5 A Proof-of-Concept Type III We describe a simple Type III side-car that mitigates common TypeScript vibe coding errors that can cause state-machine divergence and error propagation as code evolves over time. The side-car integrates with a coding agent, triggering in-cremental analysis that proposes the introduction of new formalizations, currently focused on syntactic checks for a few patterns which can flag future bugs, that get checked via compiler. The goal is to incrementally steer development such that as many bugs are detected at compile time as pos-sible. To illustrate the bugs we aim to prevent, consider the toy example in Listing 1, ignoring the red code for now. Suppose that ‘shipped’ and ‘cancelled’ (and the asso-ciated code in blue) were added via LLM edits. Assum-ing that updateOrderUI calls OrderBadge, the LLM edits silently lead to two bugs: OrderBadge lacks a case for ‘shipped’, so shipped orders are not reflected in the UI. processOrder lacks a ‘cancelled’ action, so the UI could indicate that an order has been cancelled, while no cancella-tion occurs. // orderProcessor.ts function processOrder(order: Order){ updateOrderUI(order.status); switch(order.status) { case 'pending': return sendPaymentReminder(order); case 'paid': return scheduleShipping(order); case 'shipped': return sendNotification(order); // side-car: exhaustive guard default: return assertNever(order.status); } } // orderUI.tsx function OrderBadge({ status }: { status: OrderStatus }) { switch (status) { case 'pending': return <Badge color="Y">Pending</Badge>; case 'paid': return <Badge color="G">Paid</Badge>; case 'cancelled': return <Badge color="Gr">Cancelled</Badge>; case 'shipped': return <Badge color="B">Shipped</Badge> } } Listing 1. Toy function with exhaustive handling We now outline the component for Autoformalization (Figure 3b), specialized for these kinds of TypeScript bugs. Autoformalization uses LLM-generated specifications follow-ing predefined templates. Verification is lightweight, relying on syntactic checks and successful compilation. The specifi-cations can also act as “soft” constraints, used as suggestions provided to the LLM to steer engineering practices, in hopes of revealing future bugs at compile time. We focus on four autoformalization targets, which take the form of templates that are generated by an LLM. The templates are composed of two pieces: the Scope and the Spec. The Spec describes the desired properties, while the Scope describes which parts of the code are being considered as part of the Spec. The four targets are as follows: Exhaustive Switch: The Scope is a switch statement S, described by its location in the code, union type UnionName being switched over, and which cases are covered, Cases. The Spec states that either Cases = Members(UnionName) or S has a default containing assertNever and compilation succeeds. assertNever (shown below) turns “exhaustive handling” into a compile-time check. If control reaches it with anything other than never, the TypeScript compiler errors immediately. export function assertNever(x: never): never { throw new Error(Unexpected case: ${JSON.stringify(x)}); } The goal of Exhaustive Switch is to prevent silent failures when union types are extended, to enforce exhaustive han-dling of union types across the codebase, and ensure that future buggy variants fail quickly. This spec is capable of detecting the bugs in the code of Listing 1. Discriminated Union: The Scope is an area of control flow characterized by comparisons on a string-valued vari-able t belonging to an object type and the observed values of t. The Spec states that a union type UT should be created with the observed values of t and that the string comparisons should be replaced with a switch statement over UT. For ex-ample, in Listing 2, t is action.type and the observed values are ‘ADDTODO’, ‘REMOVETODO’, and ‘TOGGLETODO’. interface Action { type: string; payload?: any; } function reducer(state: State, action: Action) { if (action.type === 'ADDTODO') { return {...} }; else if (action.type === 'REMOVETODO') { return {... } }; else if (action.type === 'TOGGLETODO') { return {... }; } return state; } Listing 2. Toy function with stringly comparisons The goal of Discriminated Union is to formalize string-based state/type discrimination, preventing semantic drift and technical debt. Union Alias: The Scope refers to locations in the code with semantically-related families of strings. The Spec states that a union type containing the set of strings should exist. Further, sites that produce/consume the strings must be an-notated with the type and not rely on hard-coded strings. For example, in ‘stringly-typed’ APIs, promote a union (e.g., type MessageType = ’info’ | ’warning’ | ’error’) and con-strain call sites (e.g., processMessage(type: MessageType, data: any)). The goal of Union Alias is to centralize semantically-related literals used in similar contexts into a union type to prevent future semantic drift and duplication. satisfies Guard: The Scope refers to an object literal M intended as a total mapping from a finite set of keys (K) to values (V) (e.g., HTTP methods → handlers). The Spec states that the object M has satisfies Record<K, V> and compiles successfully. The goal of satisfies Guard is to ensure that finite-key objects have complete key coverage and correct values at runtime. Experiments We created a small proof-of-concept im-plementation written in TypeScript of the Type III side-car architecture (Figure 3a), with our previously outlined Type III component. The autoformalization component uses LLM-based analysis to instantiate templates - as concrete specifications. Currently, the Verification/Testing compo-nent of the side-car (Figure 3b) uses lightweight syntactic checks and compilation success. Future implementations will use more sophisticated code provenance for patterns that cannot be syntactically verified. To implement the Type III system (Figure 3a), we integrated our proposed side-car with Claude Code, a popular vibe coding LLM agent, via hooks that run on code changes. Results were promising; for example, the prototype system can emit the lines in red in Listing 1, flagging and fixing both bugs. 6 Conclusion Vibe coding is inherently fragile. Prompt-by-prompt LLM ed-its inevitably collide with accumulating design constraints, leading to constraint-reconciliation decay, technical debt, and security failures. In this position paper, we advocate for Vibe Reasoning (Type III systems): a developer-first in-tegration of formal methods to address these fundamental limitations. We invite the formal methods community to treat vibe coding’s current pain points as fertile ground for developing the next generation of developer-centric verifi-cation techniques, and we hope our paper shines a light on the challenges and opportunities.