Dissect-and-Restore: AI-based Code Verification with Transient Refactoring

TL;DR

This paper introduces Prometheus, an AI-assisted system that enhances formal code verification by decomposing complex programs into verifiable parts, significantly improving verification success rates especially for complex specifications.

Contribution

The paper presents a novel AI-assisted verification workflow using transient modular refactoring to decompose and recompose code, improving verification effectiveness for complex programs.

Findings

Successfully verified 86% of tasks, outperforming baseline at 68%.

Verification success increased from 30% to 69% with complex specifications.

Proof outline integration boosted verification from 25% to 87%.

Abstract

Formal verification is increasingly recognized as a critical foundation for building reliable software systems. However, the need for specialized expertise to write precise specifications, navigate complex proof obligations, and learn annotations often makes verification an order of magnitude more expensive than implementation. While modern AI systems can recognize patterns in mathematical proofs and interpret natural language, effectively integrating them into the formal verification process remains an open challenge. We present Prometheus, a novel AI-assisted system that facilitates automated code verification with current AI capabilities in conjunction with modular software engineering principles (e.g., modular refactoring). Our approach begins by decomposing complex program logic, such as nested loops, into smaller, verifiable components. Once verified, these components are recomposed to construct a proof of the original program. This decomposition-recomposition workflow is non-trivial. Prometheus addresses this by guiding the proof search through structured decomposition of complex lemmas into smaller, verifiable sub-lemmas. When automated tools are insufficient, users can provide lightweight natural language guidance to steer the proof process effectively. Our evaluation demonstrates that transiently applying modular restructuring to the code substantially improves the AI's effectiveness in verifying individual components. This approach successfully verifies 86% of tasks in our curated dataset, compared to 68% for the baseline. Gains are more pronounced with increasing specification complexity, improving from 30% to 69%, and when integrating proof outlines for complex programs, from 25% to 87%.