title: Leveraging Large Language Models for Automated Proof Synthesis in Rust
summary: 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.
paper_authors._id: 654af8e0fc2ecdff062a172a
paper_authors.name: Jianan Yao
paper_authors._id: 654af8e0fc2ecdff062a172b
paper_authors.name: Ziqiao Zhou
paper_authors._id: 654af8e0fc2ecdff062a172c
paper_authors.name: Weiteng Chen
paper_authors._id: 654af8e0fc2ecdff062a172d
paper_authors.name: Weidong Cui
paper_title: Leveraging Large Language Models for Automated Proof Synthesis in Rust
paper_summary: 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.
paper_ai_summary: A prototype combining Large Language Models and static analysis reduces human effort in writing formal verification proof code by generating logical structures but overlooks context retention.
paper_ai_keywords: Large Language Models LLMs formal verification static analysis Rust Verus postconditions loop invariants OpenAI's GPT-4 vector-manipulating programs