Genefication: Generative AI + Formal Verification
Generative AI is a powerful tool that can significantly enhance developer productivity by generating code quickly and efficiently. However, a major challenge when using generative AI is ensuring the correctness of the generated code, especially in critical systems where errors can have significant consequences. I have heard of companies dealing with critical systems have banned the use of any code generation technologies, including generative AI, to minimize the risk of introducing bugs. In addition, there are reports suggesting using AI coding assistants has led to a 40% increase in the bug rate. A promising way to address the correctness challenges of AI-generated code, particularly in the context of high-level distributed system design, is by combining generative AI with formal verification. This approach could be referred to a...