Leveraging Large Language Models for Automated Proof Synthesis in Rust

TL;DR

This paper combines Large Language Models and static analysis to automate proof synthesis in Rust, significantly reducing human effort in formal verification tasks.

Contribution

It introduces a novel approach that integrates GPT-4 with static analysis for automated proof generation in Rust-based verification.

Findings

LLMs can generate postconditions and invariants for short code snippets

The prototype reduces human effort in proof coding

Iterative querying and static analysis improve proof synthesis

Abstract

Formal verification can provably guarantee the correctness of critical system software, but the high proof burden has long hindered its wide adoption. Recently, Large Language Models (LLMs) have shown success in code analysis and synthesis. In this paper, we present a combination of LLMs and static analysis to synthesize invariants, assertions, and other proof structures for a Rust-based formal verification framework called Verus. In a few-shot setting, LLMs demonstrate impressive logical ability in generating postconditions and loop invariants, especially when analyzing short code snippets. However, LLMs lack the ability to retain and propagate context information, a strength of traditional static analysis. Based on these observations, we developed a prototype based on OpenAI's GPT-4 model. Our prototype decomposes the verification task into multiple smaller ones, iteratively queries GPT-4, and combines its output with lightweight static analysis. We evaluated the prototype with a developer in the automation loop on 20 vector-manipulating programs. The results demonstrate that it significantly reduces human effort in writing entry-level proof code.