VeCoGen: Automating Generation of Formally Verified C Code with Large Language Models

TL;DR

VECOGEN leverages large language models and formal verification to automatically generate and verify correct C programs from specifications, demonstrating success on competitive programming problems.

Contribution

This paper introduces VECOGEN, a novel tool that combines LLMs with formal verification to generate formally verified C code from specifications.

Findings

VECOGEN successfully solves 13 out of 15 Codeforces problems.

The tool effectively combines candidate generation and iterative improvement.

Formal verification ensures the correctness of generated programs.

Abstract

Large language models have demonstrated impressive capabilities in generating code, yet they often produce programs with flaws or deviations from intended behavior, limiting their suitability for safety-critical applications. To address this limitation, this paper introduces VECOGEN, a novel tool that combines large language models with formal verification to automate the generation of formally verified C programs. VECOGEN takes a formal specification in ANSI/ISO C Specification Language, a natural language specification, and a set of test cases to attempt to generate a verified program. This program-generation process consists of two steps. First, VECOGEN generates an initial set of candidate programs. Secondly, the tool iteratively improves on previously generated candidates. If a candidate program meets the formal specification, then we are sure the program is correct. We evaluate VECOGEN on 15 problems presented in Codeforces competitions. On these problems, VECOGEN solves 13 problems. This work shows the potential of combining large language models with formal verification to automate program generation.