# LLMs and Fuzzing in Tandem: A New Approach to Automatically Generating Weakest Preconditions

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 8 of its 49 references that are in the map.
- First posted on arXiv 3 Jul 2025.

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

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [A Comprehensive Overview of Large Language Models](https://mlsanity.com/paper/2307.06435/) (2023)
- [CodeT: Code Generation with Generated Tests](https://mlsanity.com/paper/2207.10397/) (2022)
- [Impact of Code Language Models on Automated Program Repair](https://mlsanity.com/paper/2302.05020/) (2023)
- [The Art, Science, and Engineering of Fuzzing: A Survey](https://mlsanity.com/paper/1812.00140/) (2018)
- [Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?](https://mlsanity.com/paper/2310.01831/) (2023)
- [Lemur: Integrating Large Language Models in Automated Program Verification](https://mlsanity.com/paper/2310.04870/) (2023)
- [Data-Driven Abductive Inference of Library Specifications](https://mlsanity.com/paper/2108.04783/) (2021)

## Abstract (arXiv)

The weakest precondition (WP) of a program describes the largest set of initial states from which all terminating executions of the program satisfy a given postcondition. The generation of WPs is an important task with practical applications in areas ranging from verification to run-time error checking. This paper proposes the combination of Large Language Models (LLMs) and fuzz testing for generating WPs. In pursuit of this goal, we introduce Fuzzing Guidance (FG); FG acts as a means of directing LLMs towards correct WPs using program execution feedback. FG utilises fuzz testing for approximately checking the validity and weakness of candidate WPs, this information is then fed back to the LLM as a means of context refinement. We demonstrate the effectiveness of our approach on a comprehensive benchmark set of deterministic array programs in Java. Our experiments indicate that LLMs are capable of producing viable candidate WPs, and that this ability can be practically enhanced through FG.