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.

基于大型语言模型（LLMs）和静态分析相结合，开发了一个基于 Rust 的形式验证框架 Verus 的原型。通过将验证任务分解为多个较小的任务，迭代地查询 GPT-4，并将其输出与轻量级静态分析相结合，这个原型显著减少了编写入门级证明代码的人力工作。