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.