# Towards Automated Verification of LLM-Synthesized C Programs

arXiv: https://arxiv.org/abs/2410.14835 · HTML: https://mlsanity.com/paper/2410.14835/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 18 Oct 2024.

## Built on by (most cited first, 1 of 1)

- [HoarePrompt: Structural Reasoning About Program Correctness in Natural Language](https://mlsanity.com/paper/2503.19599/) (2025)

## Abstract (arXiv)

We present synver, a novel synthesis and verification framework for C programs, that deploys a Large Language Model (LLM) to search for a candidate program that satisfies the given specification. Our key idea is to impose syntactic and semantic biases on programs generated by LLMs, such that the synthesized program is more amenable to automated verification. Based on this idea, we propose a novel specification-verification tool, built on top of Verified Software Toolchain, that help automate the process. Our experiments on a diverse set of benchmarks drawn from the deductive program synthesis community, shows that this approach is scalable and extensible. The benchmarks constitute of specifications comprising of basic coding examples, Separation Logic based assertions, and API specifications.