Within recent years, Large Language Models (LLMs) have seen a significant increase in usage in various domains. One such domain is the field of safety-critical software, where the technology can generate code. However, code generated by these LLMs often contains mistakes and vulnerabilities, making it dangerous for systems where the failure can have severe consequences. In this thesis, we propose Vecogen. Vecogen uses LLMs to generate C code that is formally verified to ensure its correctness. The thesis touches on different parameters, models, prompting techniques and specifications as input for formally verified code generation. Additionally, feedback from a compiler GCC and a formal verification tool, Frama-C, attempts to improve non-verifying attempts iteratively, automated in a tool named Vecogen. Formal specifications in ANSI/ISO C Specification Language (ACSL) and natural language specifications are used for the generation and improvement process. As these formal specifications also give different amounts of information, we curate two datasets. The first dataset contains formal specifications closely tied to a solution. The second dataset consists of formal specifications providing properties and equations to which a solution must adhere. For the first dataset, all 30 are solved using prompts, including formal specifications, while 24 are solved using natural language. LLMs can successfully translate the formal specifications into a solution if the formal specification explains an implementation. In the other dataset, natural language prompts perform better, solving 13 of 15 problems, while formal specifications solve 10. When the formal specification does not give direct information about a solution, natural language prompts are more helpful in generating code. The LLM often generates wrong code and code with signed overflows, syntax, and logic errors. Iterations help resolve these errors by prompting the LLM with the failed proof attempts and compiler output. Overall, LLMs show promise in generating formally verified C code for safety-critical applications.

De senaste åren har sett en betydande ökning av användningen av Stora Språkmodeller (LLMs) inom olika domäner. En sådan domän är området säkerhetskritisk programvara, där tekniken kan generera kod. Kod som genereras av dessa LLMs innehåller dock ofta misstag och sårbarheter, vilket gör det farligt för system där felet kan få allvarliga konsekvenser. Inom denna masteruppsats genererar LLMs C-kod som sedan formellt verifieras för att säkerställa korrektheten. Avhandlingen berör olika parametrar, modeller, prompttekniker och specifikationer som input för formellt verifierad kodgenerering. Dessutom, återkoppling från en kompilator GCC och ett formellt verifieringsverktyg, Frama-C, försöker förbättra icke-verifierande försök iterativt, automatiserat i ett verktyg som heter Vecogen. Formella specifikationer i ANSI/ISO C Specification Langage (ACSL) och naturliga språkspecifikationer används för genererings- och förbättringsprocessen. Eftersom dessa formella specifikationer också ger olika mängd information, sammanställer vi två datamängder. Den första datamängden innehåller formella specifikationer som är nära kopplade till en lösning. Den andra datamängden består av formella specifikationer som tillhandahåller egenskaper och ekvationer som en lösning måste följa. För den första datamängden löses alla 30 med hjälp av prompter, inklusive formella specifikationer, medan 24 löses med naturligt språk. LLMs kan framgångsrikt översätta de formella specifikationerna till en lösning om den formella specifikationen förklarar en implementering. I den andra datamängden presterar uppmaningar med naturligt språk bättre och löser 13 av 15 problem, medan formella specifikationer löser 10. När den formella specifikationen inte ger direkt information om en lösning är promptingar med naturligt språk mer användbara för att generera kod. LLM genererar ofta fel kod och kod med signed overflows, syntax och logiska fel. Iterationer hjälper till att lösa dessa fel genom att fråga LLM med misslyckade provförsök och kompilatorns utdata. Sammantaget visar LLMs löfte när det gäller att generera formellt verifierad C-kod för säkerhetskritiska applikationer.