November 13, 2025
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.
About Prasita Mukherjee
Prasita Mukherjee is a PhD student working with Prof. Ben Delaware. Her research interests are in programming languages and neurosymbolic reasoning.