Natural Language based Specification and Verification

TL;DR

This paper explores using large language models to generate and verify natural language specifications for code, aiming to prevent vulnerabilities in AI-generated software.

Contribution

It proposes a novel approach of employing LLMs for both specification synthesis and verification in natural language, diverging from traditional formal methods.

Findings

Preliminary results indicate the approach is promising.

Using LLMs for natural language specification and verification is feasible.

The method could enhance security in AI-generated code.

Abstract

Recent frontier large language models (LLMs) have shown strong performance in identifying security vulnerabilities in large, mature open-source systems. As LLM-generated code becomes increasingly common, a natural goal is to prevent such models from producing vulnerable implementations in the first place. Formal verification offers a principled route to this objective, but existing verification pipelines typically require specifications written in rigid formal languages. Prior work has explored using LLMs to synthesize such specifications, with limited success. In this paper, we investigate a different approach: using LLMs both to generate specifications and to verify implementations compositionally when the specifications are expressed in natural language. Our preliminary results suggest that this approach is promising.