Next Steps in LLM-Supported Java Verification

TL;DR

This paper explores using Large Language Models to generate and verify code specifications for Java, aiming to establish correctness guarantees through rigorous verification tools, marking progress in reliable LLM-assisted software verification.

Contribution

It demonstrates early methods for extracting correct specifications from LLMs using formal verification tools, advancing the integration of LLMs in software correctness assurance.

Findings

LLMs can generate annotation-based specifications for Java code.

Formal verification tools can identify and correct errors in LLM-generated specifications.

Preliminary results show promise in achieving reliable specification extraction.

Abstract

Recent work has shown that Large Language Models (LLMs) are not only a suitable tool for code generation but also capable of generating annotation-based code specifications. Scaling these methodologies may allow us to deduce provable correctness guarantees for large-scale software systems. In comparison to other LLM tasks, the application field of deductive verification has the notable advantage of providing a rigorous toolset to check LLM-generated solutions. This short paper provides early results on how this rigorous toolset can be used to reliably elicit correct specification annotations from an unreliable LLM oracle.