Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2511.00202 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917053592502272 |
|---|---|
| author | Mitchell, Jacqueline Shaaban, Yasser |
| author_facet | Mitchell, Jacqueline Shaaban, Yasser |
| contents | ``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) \emph{Autoformalizes} specifications (2) Validates against targets, (3) Delivers \emph{actionable} feedback to the LLM, and (4) Allows intuitive developer influence on specifications. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_00202 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Position: Vibe Coding Needs Vibe Reasoning: Improving Vibe Coding with Formal Verification Mitchell, Jacqueline Shaaban, Yasser Software Engineering Machine Learning Logic in Computer Science F.3.1; I.2.5 ``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) \emph{Autoformalizes} specifications (2) Validates against targets, (3) Delivers \emph{actionable} feedback to the LLM, and (4) Allows intuitive developer influence on specifications. |
| title | Position: Vibe Coding Needs Vibe Reasoning: Improving Vibe Coding with Formal Verification |
| topic | Software Engineering Machine Learning Logic in Computer Science F.3.1; I.2.5 |
| url | https://arxiv.org/abs/2511.00202 |