# Automated Lemma Discovery in Agentic Program Verification

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use.
- Builds on 14 of its 68 references that are in the map.
- First posted on arXiv 23 Mar 2026.

## Placed in

- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)

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

- [Using an LLM to Help With Code Understanding](https://mlsanity.com/paper/2307.08177/) (2023)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)
- [Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?](https://mlsanity.com/paper/2310.01831/) (2023)
- [RepoAudit: An Autonomous LLM-Agent for Repository-Level Code Auditing](https://mlsanity.com/paper/2501.18160/) (2025)
- [Generating Correctness Proofs with Neural Networks](https://mlsanity.com/paper/1907.07794/) (2019)
- [Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification](https://mlsanity.com/paper/2412.14063/) (2024)
- [Passport: Improving Automated Formal Verification Using Identifiers](https://mlsanity.com/paper/2204.10370/) (2022)
- [Deductive Verification of Unmodified Linux Kernel Library Functions](https://mlsanity.com/paper/1809.00626/) (2018)
- [Adaptive Proof Refinement with LLM-Guided Strategy Selection](https://mlsanity.com/paper/2510.25103/) (2025)
- [Neural Theorem Proving for Verification Conditions: A Real-World Benchmark](https://mlsanity.com/paper/2601.18944/) (2026)
- [PAT-Agent: Autoformalization for Model Checking](https://mlsanity.com/paper/2509.23675/) (2025)
- [Automated Lemma Synthesis in Symbolic-Heap Separation Logic](https://mlsanity.com/paper/1710.09635/) (2017)

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

- [Schwarz: Solver-Aware Agentic Program Verification](https://mlsanity.com/paper/2608.30803/) (2026)
- [Cost-Efficient Theorem Proving via Agent Orchestration in Program Verification](https://mlsanity.com/paper/2610.09681/) (2026)

## Abstract (arXiv)

Deductive verification provides strong correctness guarantees for code by extracting verification conditions (VCs) and writing formal proofs for them. The expertise-intensive task of VC proving is the main bottleneck in this process, and has been partly automated owing to recent advances in Large Language Model (LLM) agents. However, existing proof agents are not able to discover helper lemmas -- auxiliary lemmas that aid in proving -- and thus fall short as programs grow in size and complexity. In this paper, we argue that VC proving for program verification is more than a purely mathematical task, and benefits considerably from program comprehension. Our key insight is that human proof engineers often discover and apply helper lemmas based on their understanding of the program semantics, which are not directly reflected in the VCs produced by VC generators. Inspired by this insight, we propose an LLM agent, LemmaNet, that discovers helper lemmas in two ways. Specifically, the agent first synthesizes lemmas offline by directly analyzing the source code and specifications and then relating this semantic understanding to the mechanical, verbose encoding produced by VC generators. As the proof unfolds, LemmaNet then adapts existing helper lemmas online to accommodate evolving proof states, enabling the agent to effectively discharge complex VCs on-the-fly. We implement LemmaNet on top of an existing proof agent AutoRocq for Rocq and the Frama-C ecosystem, and evaluate it on SV-COMP and established real-world subjects, including modules of the Linux kernel, Contiki OS, standard C++ library, and X.509 parser. Our experimental results demonstrate that LemmaNet significantly outperforms state-of-the-art approaches, highlighting the importance of program comprehension-aided lemma discovery in agentic program verification.