LLM Agent Automates Proof Discovery for Complex Program Verification

Formal program verification—the practice of mathematically proving that code behaves correctly—remains a labor-intensive bottleneck in software engineering. The core challenge lies in proving verification conditions (VCs), logical statements that must hold for code to be considered correct. Recent advances in large language model agents have begun automating this proof work, but existing systems hit a critical wall: they cannot discover the auxiliary mathematical lemmas that human experts instinctively invoke to make difficult proofs tractable.

The Core Insight#

A new paper from arXiv argues that VC proving is not purely mathematical reasoning. Instead, it deeply benefits from understanding the program itself—what it does, what it intends, how its parts relate to each other. Professional proof engineers routinely invent helper lemmas by drawing on their grasp of program semantics, insights that are often invisible in the raw, verbose logical encodings that VC generators produce. This gap between human intuition and machine-readable proof states is where existing agents stumble.

How LemmaNet Works#

The researchers propose LemmaNet, an LLM agent that discovers helper lemmas in two complementary ways:

• Offline synthesis: The agent directly reads source code and specifications, building a semantic understanding of the program, and maps that understanding onto the mechanical VC encoding to generate useful lemmas before proof begins.
• Online adaptation: As the proof unfolds, LemmaNet refines and adjusts existing lemmas to fit evolving proof states, enabling it to handle complex VCs on the fly.

The system builds on AutoRocq, an existing proof agent for the Rocq proof assistant and Frama-C verification ecosystem.

Real-World Results#

The team evaluated LemmaNet on standard benchmarks (SV-COMP) and established real-world codebases including Linux kernel modules, Contiki OS, the C++ standard library, and X.509 cryptographic parsers. Results show that LemmaNet substantially outperforms state-of-the-art verification approaches, suggesting that integrating program comprehension into proof automation is essential for scaling formal verification to larger, more complex systems.