Abductive Vibe Coding (Extended Abstract)

TL;DR

This paper proposes a semi-formal framework for validating AI-generated software artifacts by extracting rationales that specify conditions for their adequacy, addressing the challenge of formal verification in vibe coding.

Contribution

It introduces an approach to generate semi-formal rationales for AI-generated code, enabling validation without full formal proofs.

Findings

Initial framework implementation underway

Conditions for code adequacy are being formalized

Potential for improved validation of AI-generated artifacts

Abstract

When software artifacts are generated by AI models ("vibe coding"), human engineers assume responsibility for validating them. Ideally, this validation would be done through the creation of a formal proof of correctness. However, this is infeasible for many real-world vibe coding scenarios, especially when requirements for the AI-generated artifacts resist formalization. This extended abstract describes ongoing work towards the extraction of analyzable, semi-formal rationales for the adequacy of vibe-coded artifacts. Rather than deciding correctness directly, our framework produces a set of conditions under which the generated code can be considered adequate. We describe current efforts towards implementing our framework and anticipated research opportunities.