LLM-Assisted Synthesis of High-Assurance C Programs

We present SYNVER -a novel, general purpose synthesizer for C programs equipped with machine-checked proofs of correctness using the Verified Software Toolchain. To do so, SYNVER employs two Large Language Models (LLMs): the first generates candidate programs from user-provided specifications, and the second helps automatically construct formal proofs of their correctness in the Rocq proof assistant. To facilitate verification, SYNVER places a set of syntactic restrictions on candidate programs that make them amenable to automated reasoning. SYNVER uses a hybrid verification strategy that combines symbolic reasoning with LLM-powered proof generation to discharge proof obligations that the symbolic engine cannot handle on its own. We demonstrate the applicability of SYNVER using a diverse set of benchmarks drawn from the program synthesis and verification literature. Index Terms-Formal Verification, Automatic Programming, and Large Language Models / * h1 → l1 * h2 → l2 * / 2 struct sll * append(struct sll * h1, struct sll * h2) 3 4 struct sll * current = h1;