Position: Vibe Coding Needs Vibe Reasoning: Improving Vibe Coding with Formal Verification — Mitchell & Shaaban (2025)

“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: (1) Autoformal- izes specifications (2) Validates against targets, (3) Delivers actionable feedback to the LLM, and (4) 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. This Full Reading presents the paper's text as an audio edition. Abstract source: pdf-extraction Authors: Jacqueline Mitchell, Yasser Shaaban Published in: Proceedings of the 1st ACM SIGPLAN International Workshop on Language Models and Programming Languages Publication date: 2025-10-09 Read the paper Source license: Creative Commons Attribution 4.0 International Narration: Read verbatim by an AI-generated voice. The authors and publisher do not sponsor or endorse this recording. Brief episode