[2509.21629] Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis

Computer Science > Programming Languages arXiv:2509.21629 (cs) [Submitted on 25 Sep 2025 (v1), last revised 2 Apr 2026 (this version, v3)] Title:Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis Authors:Anjiang Wei, Tianran Sun, Tarun Suresh, Haoze Wu, Ke Wang, Alex Aiken View a PDF of the paper titled Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis, by Anjiang Wei and 5 other authors View PDF HTML (experimental) Abstract: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, an evaluation-oriented framework for LLM-based invariant synthesis that provides sound evaluation and achieves state-of-the-art performance. Unlike prior work that treats LLM outputs as noisy symbolic material requiring substantial post-processing, Quokka adopts a simpler and evaluation-centric design that directly validates whether each LLM-generated invariant helps prove the target assertion. We construct a benchmark of 866 instances derived from SV-COMP and evaluate 9 state-of-the-art LLMs across 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 avail...