Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis

Anjiang Wei, Tianran Sun, Tarun Suresh +3

Program verification relies on loop invariants, yet automatically discovering strong invariants remains a long-standing challenge. We investigate whether large language models (LLM…