Safe Coding with LLMs - Verifiable Scala Silver Bullet

Explore the intersection of large language models and formal verification in this conference talk examining whether state-of-the-art LLMs can generate certifiably safe Scala code. Discover the challenges and opportunities of using AI for code generation in mission-critical systems, where correctness and security are paramount. Learn about the Stainless verification framework and how it can be leveraged to ensure generated code is not just functional, but provably correct and secure. Examine the current limitations of LLMs when tasked with generating both implementation code and formal specifications, including common issues like syntax errors and verification bypass attempts. Understand the unique advantages Scala offers for LLM code generation due to its extensive public codebases, comprehensive documentation, and strong type system that supports static verification techniques. Gain insights into research findings that reveal the complexity of achieving truly verifiable AI-generated code, and explore potential solutions through refined prompting strategies and leveraging Scala's rich type system for static safety guarantees. This presentation addresses the critical gap between the productivity benefits of AI-assisted coding and the stringent safety requirements of enterprise and mission-critical software development.