# Next Steps in LLM-Supported Java Verification

arXiv: https://arxiv.org/abs/2502.01573 · HTML: https://mlsanity.com/paper/2502.01573/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 38 references that are in the map.
- First posted on arXiv 3 Feb 2025.

## Builds on (most cited first, 9 of 9)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [Lemur: Integrating Large Language Models in Automated Program Verification](https://mlsanity.com/paper/2310.04870/) (2023)
- [Finding Inductive Loop Invariants using Large Language Models](https://mlsanity.com/paper/2311.07948/) (2023)
- [Ranking LLM-Generated Loop Invariants for Program Verification](https://mlsanity.com/paper/2310.09342/) (2023)
- [Can ChatGPT support software verification?](https://mlsanity.com/paper/2311.02433/) (2023)
- [Leveraging Large Language Models for Automated Proof Synthesis in Rust](https://mlsanity.com/paper/2311.03739/) (2023)
- [Intersymbolic AI: Interlinking Symbolic AI and Subsymbolic AI](https://mlsanity.com/paper/2406.11563/) (2024)
- [OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse](https://mlsanity.com/paper/1404.6608/) (2014)

## Built on by (most cited first, 3 of 3)

- [Do AI models help produce verified bug fixes?](https://mlsanity.com/paper/2507.15822/) (2025)
- [Decision-Theoretic Safety Assessment of Persona-Driven Multi-Agent Systems in O-RAN](https://mlsanity.com/paper/2604.09682/) (2026)
- [AutoACSL: Synthesizing ACSL Specifications by Integrating LLMs with CPG-Based Static Analysis](https://mlsanity.com/paper/2606.20969/) (2026)

## Abstract (arXiv)

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.