🤖 machine learning

Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis

The paper introduces Quokka, an evaluation-centric framework that leverages large language models to directly validate and synthesize loop invariants for program verification, demonstrating state-of-the-art performance through a comprehensive benchmark of 866 instances and various LLM configurations.

Original authors: Anjiang Wei, Tianran Sun, Tarun Suresh, Haoze Wu, Ke Wang, Alex Aiken

Published 2026-04-03

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Anjiang Wei, Tianran Sun, Tarun Suresh, Haoze Wu, Ke Wang, Alex Aiken

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are trying to prove that a complex machine (a computer program) will never break or do something dangerous. In the world of software, this is called Program Verification.

To prove a machine works forever, you need a "magic rule" called a Loop Invariant. Think of a loop in a program like a hamster running on a wheel. The invariant is a rule that stays true no matter how many times the hamster runs. For example, "The hamster is always on the wheel" or "The hamster's speed is always positive." If you can find a strong enough rule, you can prove the machine will never crash.

The problem? Finding these rules is incredibly hard. It's like trying to guess the secret combination to a safe without any clues.

Enter Quokka, a new tool described in this paper. Here is how it works, explained simply:

1. The Old Way: The "Over-Engineered" Mechanic

Previously, researchers tried to use AI (Large Language Models, or LLMs) to guess these rules. But they treated the AI like a clumsy apprentice who kept making mistakes.

The Approach: They would ask the AI for a rule, then build a massive, complex machine to "fix" the AI's answer. They would filter, reassemble, and repair the AI's output, hoping to turn a messy guess into a solid proof.
The Flaw: It was like hiring a genius chef to cook a meal, but then forcing a team of 10 sous-chefs to taste, chop, and re-season every ingredient before serving it. It was slow, complicated, and often missed the point.

2. The Quokka Way: The "Direct Judge"

The authors of this paper, led by Anjiang Wei, asked a simple question: "What if we stop trying to fix the AI's answers and just ask the AI for a guess, then immediately check if it works?"

They built Quokka, a framework that acts like a strict but fair judge:

The Ask: They ask the AI (the LLM) to propose a rule (invariant) for a specific part of the code.
The Test: Instead of trying to fix the rule, they immediately feed it into a "Verifier" (a super-strict robot mathematician).
The Verdict:
- Is the rule true? (Does the hamster stay on the wheel?)
- Does the rule help? (Is the rule strong enough to prove the machine won't crash?)

If the rule helps prove the machine is safe, Quokka wins. If not, it moves on. It doesn't waste time trying to "repair" a bad guess; it just checks if the guess is useful.

3. Why This is a Big Deal

Simplicity is Power: By removing the complex "repair" machinery, Quokka is faster and more efficient. It's like realizing that instead of building a factory to fix broken toys, you just need a good quality control inspector.
The Benchmark: The team created a massive test suite of 866 difficult programming puzzles (the "SV-COMP" dataset). It's like a "Olympics" for program verification tools.
The Results: Quokka, powered by smart AI models, beat all the previous complex methods. It solved more problems and did it faster.

4. Training the AI

The paper also shows that you can make the AI even better.

Fine-Tuning: They taught the AI by showing it thousands of examples of correct rules. It's like giving the apprentice a textbook of perfect solutions.
Best-of-N: They asked the AI to generate 8 different guesses and picked the one that worked best. It's like asking a chef to cook 8 versions of a dish and serving only the best one.

The Bottom Line

Quokka proves that we don't need to over-complicate how we use AI for safety-critical tasks. Instead of trying to "fix" the AI's output with complex algorithms, we should let the AI propose ideas and use a powerful checker to see if those ideas actually work.

It's a shift from "How do we fix the AI's mistakes?" to "How do we quickly find the AI's best ideas?"

In a nutshell: Quokka is a new, simpler, and faster way to use AI to prove that computer programs are safe, beating out all previous methods by trusting the AI's raw ideas and letting a strict robot verify them instantly.

1. Problem Statement

Program verification relies heavily on loop invariants—logical conditions that hold before, during, and after every iteration of a loop—to prove that software behaves as intended. While generating correct invariants is relatively easy (any universally true statement suffices), generating strong invariants that are sufficient to prove specific target assertions remains a significant challenge.

The Gap: Traditional automated verification tools often struggle with complex loops, leading to timeouts or inconclusive results.
The LLM Opportunity: Large Language Models (LLMs) have shown promise in code generation and reasoning. However, prior attempts to use LLMs for invariant synthesis suffered from two main issues:
1. Unsound Evaluation: Previous work (e.g., Pei et al., 2023) relied on dynamic analysis tools like Daikon to check correctness, which is unsound (may miss edge cases) and cannot assess if an invariant is "strong" enough to speed up formal verification.
2. Over-Engineering: Subsequent LLM-based verifiers (e.g., LaM4Inv, LEMUR, Loopy) treated LLM outputs as "noisy symbolic material," requiring complex post-processing pipelines (filtering, reassembling, recursive repair, and backtracking) to make them usable. This raises the question: as LLMs become more capable, is such heavy algorithmic intervention still necessary?

2. Methodology: The Quokka Framework

The authors introduce Quokka, an evaluation-oriented framework that adopts a simpler, direct, and sound approach to LLM-based invariant synthesis.

Core Design Philosophy

Instead of treating LLM outputs as imperfect artifacts requiring repair, Quokka treats them as direct proof candidates. It validates whether a generated invariant is correct and, crucially, whether it accelerates the verification of the target assertion.

Technical Workflow

Input: A program $P$ and a target property $p^* = \langle \phi^*, \ell^* \rangle$ .
LLM Proposal: The LLM proposes a candidate invariant $q = \langle \psi, \ell \rangle$ (a predicate at a specific program location).
Syntactic Validation: The system checks that $\psi$ is a valid Boolean state predicate (rejecting assignments or side effects).
Parallel Verifier Queries: Quokka issues two parallel queries to a formal verifier (specifically UAutomizer):
- Query A ( $d_a$ ): Verify if $q$ is a valid invariant ( $P \models q$ ).
- Query B ( $d_b$ ): Verify if the target property holds assuming $q$ is true ( $P \cup \{q\} \models p^*$ ).
Decision Logic:
- Success (T): If $q$ is valid AND $p^*$ holds under $q$ , the property is proven.
- Failure (F): If $p^*$ fails even under the assumption of $q$ , the property is refuted.
- Inconclusive (U): If either query times out or fails to prove/refute, the result is inconclusive.
Speedup Metric: The primary goal is not just finding any invariant, but finding one that reduces the solving time compared to the baseline (verifying without LLM assistance).

Enhancement Techniques

Supervised Fine-Tuning (SFT): The authors constructed a training dataset of 3,589 synthetic C programs with ground-truth invariants extracted from UAutomizer. They fine-tuned models (e.g., Qwen2.5-7B) using LoRA.
Best-of-N Sampling: The system generates $N$ candidate invariants and selects the one that yields the fastest verification time (or solves the instance), executing $2N$ verifier queries in parallel.

3. Key Contributions

Quokka Framework: A sound, evaluation-centric framework that eliminates complex post-processing logic, directly validating LLM invariants against a formal solver.
New Benchmark: A dataset of 866 instances derived from SV-COMP (Software Verification Competition), significantly larger and more complex (supporting multi-loops, multi-functions, arrays, and pointers) than previous LLM verification benchmarks.
Comprehensive Evaluation: Evaluation of 9 state-of-the-art LLMs (including GPT-5, Claude 4, Qwen2.5, and Llama-3.1) across multiple families.
Performance Optimization: Demonstration that Supervised Fine-Tuning and Best-of-N sampling yield measurable improvements in both correctness and verification speedup.

4. Experimental Results

Model Performance:
- Larger and more recent models (e.g., gpt-5.2, claude-opus-4.5) significantly outperformed smaller models.
- gpt-5.2 achieved the highest performance: 710 correct invariants and solved 21 additional instances beyond the UAutomizer baseline within a 60-second timeout.
- Speedup: Quokka reduced average solving times significantly (e.g., from ~41.9s to ~22.2s for top models under 60s timeout).
Comparison with Prior Work:
- Quokka consistently outperformed prior LLM-based verifiers (LEMUR, Clause2Inv, Loopy, LaM4Inv) across all timeout thresholds.
- On a challenging subset where the baseline solver (UAutomizer) failed within 10 minutes, Quokka solved substantially more instances with lower average solving times than LEMUR.
Failure Analysis:
- Most failures were due to timeouts rather than incorrect invariants (only ~14% of sampled failures were genuinely incorrect invariants).
- Common failure modes included generating invariants identical to the target assertion (no decomposition benefit) or trivial bounds that failed to capture loop behavior.
Fine-Tuning & Sampling:
- Fine-tuning provided modest gains (e.g., +2 correct invariants for Qwen2.5-7B).
- Best-of-N showed diminishing returns after $N=8$ , with $N=8$ achieving the optimal balance between sampling cost and verification success.

5. Significance and Impact

Paradigm Shift: Quokka challenges the prevailing "repair-heavy" paradigm in neuro-symbolic verification. It suggests that as LLMs improve, simpler, direct evaluation strategies are more effective than complex algorithmic pipelines designed to "fix" LLM outputs.
Soundness: By relying on a formal verifier (UAutomizer) rather than dynamic analysis, Quokka provides sound guarantees, ensuring that reported speedups are mathematically valid.
Scalability: The framework demonstrates that LLMs can effectively accelerate formal verification on complex, real-world benchmarks (SV-COMP), bridging the gap between AI reasoning and formal methods.
Future Direction: The work establishes a new state-of-the-art and provides a principled foundation for future research, emphasizing the importance of base solver choice (UAutomizer) and the potential of direct evaluation over complex synthesis algorithms.

In summary, Quokka proves that a streamlined, evaluation-centric approach using LLMs can outperform complex, heuristic-heavy systems in program verification, offering a robust path toward faster and more reliable software analysis.