FormAI - Formally Verified AI-Generated Software

Purpose and goal

The overall goal is to extend the use case for generative AI to create software to areas where the correctness of the software is critical, e.g. in safety-critical systems. More detailed objective are: generate C++ code using LLM, automate deductive verification of C++ code, use automatic deductive verification to iteratively generate code using AI; use verification to improve AI code generation models through “reinforcement learning”, create a demonstrator and proof-of-concept, and explore methods to derive the formal eligibility requirements needed.

Expected effects and result

Provided the project is successful, the result will be that formal deductive verification can be done for C++ code and not just C as today. The degree of automation of formal code verification will be increased, making it useful and available for more applications. These effects in turn contribute to increased software quality in critical software, which makes systems safer and more reliable. Furthermore, increased quality of code generated via AI is achieved through improved AI code generation models that are achieved from reinforcement learning combined with formal feedback.

Planned approach and implementation

The project is led by Scania. The first months focus on recruitment and start-up. In 2024, the focus is also on selection of LLM and initial guiding experiments with C. In parallel, support for verification of C++ code is being developed. The project works with case studies with real industrial requirements and industrial code. Experiments are gradually made with more and more difficult examples. The focus in development and research is placed on things that need to be improved to make these industrial examples work.