# Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 20 of its 57 references that are in the map.
- First posted on arXiv 25 Sep 2025.

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

- [LoRA: Low-Rank Adaptation of Large Language Models](https://mlsanity.com/paper/2106.09685/) (2021)
- [LLaMA: Open and Efficient Foundation Language Models](https://mlsanity.com/paper/2302.13971/) (2023)
- [Qwen3 Technical Report](https://mlsanity.com/paper/2505.09388/) (2025)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [Qwen2.5-Coder Technical Report](https://mlsanity.com/paper/2409.12186/) (2024)
- [CodeMonkeys: Scaling Test-Time Compute for Software Engineering](https://mlsanity.com/paper/2501.14723/) (2025)
- [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)
- [SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulas](https://mlsanity.com/paper/2505.14615/) (2025)
- [CLN2INV: Learning Loop Invariants with Continuous Logic Networks](https://mlsanity.com/paper/1909.11542/) (2019)
- [Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks (Extended Version)](https://mlsanity.com/paper/2003.07959/) (2020)
- [CodeARC: Benchmarking Reasoning Capabilities of LLM Agents for Inductive Program Synthesis](https://mlsanity.com/paper/2503.23145/) (2025)
- [DRYVR:Data-driven verification and compositional reasoning for automotive systems](https://mlsanity.com/paper/1702.06902/) (2017)
- [Horn-ICE Learning for Synthesizing Invariants and Contracts](https://mlsanity.com/paper/1712.09418/) (2017)
- [SLING: Using Dynamic Analysis to Infer Program Invariants in Separation Logic](https://mlsanity.com/paper/1903.09713/) (2019)
- [Towards General Loop Invariant Generation: A Benchmark of Programs with Memory Manipulation](https://mlsanity.com/paper/2311.10483/) (2023)
- [Global Guidance for Local Generalization in Model Checking](https://mlsanity.com/paper/2005.13301/) (2020)
- [Ilinva: Using Abduction to Generate Loop Invariants](https://mlsanity.com/paper/1906.11033/) (2019)

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

- [Agentic Interpretation: Lattice-Structured Evidence for LLM-Based Program Analysis](https://mlsanity.com/paper/2605.12694/) (2026)
- [FVSpec: Real-World Property-Based Tests as Lean Challenges](https://mlsanity.com/paper/2606.01008/) (2026)
- [Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification](https://mlsanity.com/paper/2607.10291/) (2026)
- [Schwarz: Solver-Aware Agentic Program Verification](https://mlsanity.com/paper/2608.30803/) (2026)

## Abstract (arXiv)

Program verification relies on loop invariants, yet automatically discovering strong invariants remains a long-standing challenge. We investigate whether large language models (LLMs) can accelerate program verification by generating useful loop invariants. We introduce Quokka, a framework for LLM-based invariant synthesis with soundness guarantees and state-of-the-art performance. Unlike prior work that treats LLM outputs as noisy symbolic material requiring substantial post-processing, Quokka adopts a simpler algorithm design that directly validates whether each LLM-generated invariant helps prove the target assertion. We construct a benchmark of 866 evaluation instances and 3589 training instances derived from SV-COMP, and evaluate 9 LLMs spanning multiple model families. We demonstrate that supervised fine-tuning and Best-of-N sampling yield measurable improvements, and we show that Quokka consistently outperforms prior LLM-based verifiers. Our code and data are publicly available at https://github.com/Anjiang-Wei/Quokka