# AI for software engineering: from probable to provable

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 4 of its 9 references that are in the map.
- First posted on arXiv 28 Nov 2025.

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

- [Language Models for Code Completion: A Practical Evaluation](https://mlsanity.com/paper/2402.16197/) (2024)
- [A Short Survey on Formalising Software Requirements using Large Language Models](https://mlsanity.com/paper/2506.11874/) (2025)
- [Do AI models help produce verified bug fixes?](https://mlsanity.com/paper/2507.15822/) (2025)
- [Lessons from Formally Verified Deployed Software Systems (Extended version)](https://mlsanity.com/paper/2301.02206/) (2023)

## Abstract (arXiv)

Vibe coding, the much-touted use of AI techniques for programming, faces two overwhelming obstacles: the difficulty of specifying goals ("prompt engineering" is a form of requirements engineering, one of the toughest disciplines of software engineering); and the hallucination phenomenon. Programs are only useful if they are correct or very close to correct. The solution? Combine the creativity of artificial intelligence with the rigor of formal specification methods and the power of formal program verification, supported by modern proof tools.