Quokka uses large language models to generate loop invariants and speed up program verification

Loop invariants are a cornerstone of formal program verification, but discovering strong ones automatically has remained difficult. Researchers exploring whether large language models can help have developed Quokka, a framework that uses LLMs to generate invariants and verify whether they assist in proving target assertions—with soundness guarantees built in.

How Quokka Works#

Rather than treating LLM outputs as raw material requiring heavy post-processing, Quokka takes a pragmatic approach: it generates candidate invariants from an LLM and directly checks whether each one helps establish the desired proof. This simpler design keeps the verification step rigorous while letting the model handle the creative work of invariant discovery.

Benchmark and Evaluation#

The team constructed a comprehensive evaluation suite with 866 test instances and 3,589 training cases drawn from SV-COMP, a standard program verification competition. They tested nine different LLMs across multiple model families and found that supervised fine-tuning and Best-of-N sampling (generating multiple candidates and selecting the best) both improved results. Quokka consistently outperformed earlier LLM-based verification systems on the benchmark.

Availability#

Code and data for Quokka are publicly available, enabling researchers to build on the findings and explore LLM-accelerated verification further.