Abstract
We investigate how combinations of Large Language Models (LLMs) and symbolicanalyses can be used to synthesise specifications of C programs. The LLMprompts are augmented with outputs from two formal methods tools in the Frama-Cecosystem, Pathcrawler and EVA, to produce C program annotations in thespecification language ACSL. We demonstrate how the addition of symbolicanalysis to the workflow impacts the quality of annotations: information aboutinput/output examples from Pathcrawler produce more context-aware annotations,while the inclusion of EVA reports yields annotations more attuned to runtimeerrors. In addition, we show that the method infers rather the programs intentthan its behaviour, by generating specifications for buggy programs andobserving robustness of the result against bugs.