Effectiveness of Large Language Models to Generate Formally Verified C code

Sammanfattning

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.