Abstract
The paper studies how code generation by LLMs can be combined with formalverification to produce critical embedded software. The first contribution is ageneral framework, spec2code, in which LLMs are combined with different typesof critics that produce feedback for iterative backprompting and fine-tuning.The second contribution presents a first feasibility study, where aminimalistic instantiation of spec2code, without iterative backprompting andfine-tuning, is empirically evaluated using three industrial case studies fromthe heavy vehicle manufacturer Scania. The goal is to automatically generateindustrial-quality code from specifications only. Different combinations offormal ACSL specifications and natural language specifications are explored.The results indicate that formally correct code can be generated even withoutthe application of iterative backprompting and fine-tuning.