# Position: Vibe Coding Needs Vibe Reasoning: Improving Vibe Coding with Formal Verification

arXiv: https://arxiv.org/abs/2511.00202 · HTML: https://mlsanity.com/paper/2511.00202/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Reasoning for agents, planning and code, one of 17 directions in LLM reasoning.
- Builds on 18 of its 26 references that are in the map.
- First posted on arXiv 31 Oct 2025.

## Placed in

- LLM reasoning / [Reasoning for agents, planning and code](https://mlsanity.com/lr/reasoning-for-agents-planning-and-code/)

## Builds on (most cited first, 18 of 18)

- [Self-Challenging Language Model Agents](https://mlsanity.com/paper/2506.01716/) (2025)
- [Copiloting the Copilots: Fusing Large Language Models with Completion Engines for Automated Program Repair](https://mlsanity.com/paper/2309.00608/) (2023)
- [LLM Agents Making Agent Tools](https://mlsanity.com/paper/2502.11705/) (2025)
- [Flexible and Efficient Grammar-Constrained Decoding](https://mlsanity.com/paper/2502.05111/) (2025)
- [Vibe Coding vs. Agentic Coding: Fundamentals and Practical Implications of Agentic AI](https://mlsanity.com/paper/2505.19443/) (2025)
- [Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency](https://mlsanity.com/paper/2410.20936/) (2024)
- [Type-Constrained Code Generation with Language Models](https://mlsanity.com/paper/2504.09246/) (2025)
- [Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs](https://mlsanity.com/paper/2301.02195/) (2023)
- [Advancing Agentic Systems: Dynamic Task Decomposition, Tool Integration and Evaluation using Novel Metrics and Dataset](https://mlsanity.com/paper/2410.22457/) (2024)
- [VeriPlan: Integrating Formal Verification and LLMs into End-User Planning](https://mlsanity.com/paper/2502.17898/) (2025)
- [CodeFlowBench: A Multi-turn, Iterative Benchmark for Complex Code Generation](https://mlsanity.com/paper/2504.21751/) (2025)
- [LLM Security Guard for Code](https://mlsanity.com/paper/2405.01103/) (2024)
- [Training Language Models to Generate Quality Code with Program Analysis Feedback](https://mlsanity.com/paper/2505.22704/) (2025)
- [Unsupervised Elicitation of Language Models](https://mlsanity.com/paper/2506.10139/) (2025)
- [Probabilistic Consensus through Ensemble Validation: A Framework for LLM Reliability](https://mlsanity.com/paper/2411.06535/) (2024)
- [Dissecting the SWE-Bench Leaderboards: Profiling Submitters and Architectures of LLM- and Agent-Based Repair Systems](https://mlsanity.com/paper/2506.17208/) (2025)
- [Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models](https://mlsanity.com/paper/2412.10483/) (2024)
- [From Defects to Demands: A Unified, Iterative, and Heuristically Guided LLM-Based Framework for Automated Software Repair and Requirement Realization](https://mlsanity.com/paper/2412.05098/) (2024)

## Abstract (arXiv)

``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, developers 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 inadvertently failing to resolve contradictions because LLMs prioritize user commands over code consistency. Given LLMs' receptiveness to verification-based feedback, we argue that formal methods can mitigate these pitfalls, making vibe coding 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: (1) Autoformalizes specifications (2) Validates against targets, (3) Delivers actionable feedback to the LLM, and (4) Allows intuitive developer influence on specifications.