FormAI

Challenges

Generative AI is already being utilized in industry for creating software. However, a significant challenge lies in ensuring the reliability of such software and meeting safety-critical system requirements. The FormAI project combines generative AI for creating software with deductive verification, providing formal proof that the software satisfies its requirements.

About

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 objectives 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 outcomes

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.

For more information, contact