AI for software engineering: from probable to provable

TL;DR

This paper proposes integrating AI with formal specification and verification methods to improve program correctness and address challenges like goal specification and hallucination in AI-assisted coding.

Contribution

It introduces a novel approach combining AI creativity with formal verification to enhance software correctness and reliability.

Findings

Combining AI with formal methods can improve program correctness.

Formal verification supports AI-generated code to reduce hallucinations.

The approach addresses goal specification challenges in AI programming.

Abstract

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.