Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications

TL;DR

This paper presents a neuro-symbolic framework that automatically generates and validates memory-aware formal function specifications for C programs, improving correctness and validity through iterative refinement and symbolic feedback.

Contribution

It introduces a novel neuro-symbolic approach combining LLMs and symbolic provers for generating and validating formal specifications from natural language descriptions.

Findings

Iterative refinement improves specification validity.

Symbolic prover-based validation filters false positives.

The approach outperforms LLM-only methods in correctness assessment.

Abstract

Formal verification of memory-manipulating programs critically depends on precise function specifications that capture memory states written by experts. This requirement has become a major bottleneck as large language models (LLMs) increasingly generate low-level systems code whose correctness cannot be assumed. To enable scalable formal verification, we focus exclusively on function specification generation, deliberately avoiding the synthesis of complex loop invariants that are central to traditional verification pipelines. We propose a neuro-symbolic framework for automatically generating memory-aware formal function specifications for C programs from natural language problem descriptions and function signatures. The pipeline first produces candidate specifications via in-context learning, and then iteratively refines them using compiler diagnostics from symbolic provers and the verification toolchain. In particular, we validate candidate specifications by constructing a proof for the negation of the specification with concrete examples, enabling machine-checked rejection of plausible-but-incorrect specifications. To support systematic evaluation, we introduce LeetCode-C-Spec, a new benchmark of 200 C programming problems for generating memory-aware formal function specifications. Experiments show that iterative refinement substantially improves syntactic validity, while symbolic prover-based refutation significantly enhances correctness assessment by filtering false positives that LLM-only judges frequently accept. Our results demonstrate that combining neural generation with symbolic feedback provides an effective approach to formal specification synthesis for memory-safe systems software.