Specify What? A Case-Study using GPT-4 and Formal Methods For Specification Synthesis

Formal specifications are supposed to unambigu-ously describe the behaviour of (parts of) pro-grams and are usually provided as extra annota-tions of the program code. The intention is bothto document the code and to be able to automati-cally check compliance of programs using formalmethods tools. Writing good specifications canhowever be both difficult and time-consuming forthe programmer. In this case-study, we investigatehow GPT-4 can help with the task. We proposea neuro-symbolic integration, by which we aug-ment the LLM prompts with outputs from twoformal methods tools in the Frama-C ecosystem(Pathcrawler and EVA), and produce C programannotations in the specifications language ACSL.We demonstrate how this impacts the quality ofannotations: information about input/output ex-amples from Pathcrawler produce more context-aware annotations, while the inclusion of EVAreports yields annotations more attuned to run-time errors.