Safe Coding with LLMs - Verifiable Scala Silver Bullet
summary
Explores whether LLMs can generate provably safe Scala by asking models to produce implementations plus Stainless specs; finds many models (Code Llama variants, Q1 2.5 coder, Qn) output syntax errors or insert @extern bypass to fake proofs, and prior C work reached only ~7% verified proofs. Builds a three-LLM TypePilot pipeline (draft, critique, rewrite using Scala types) and a demo; when the output compiles the generated code passes the team’s tests (matrix conv, Fibonacci), but full Stainless verification still fails routinely.
AI-written summary · about
chapters (14)
- 0:00Safe coding with LLMs and Scala
- 1:06LLMs struggle with secure code
- 9:11Risks of imperfect AI models
- 11:40Formal verification for mission-critical code
- 13:04Why Scala for safe coding
- 13:47Formal verification attempts
- 15:53Scala types for code safety
- 17:19Testing injection vulnerabilities
- 19:04LLM internals for security
- 21:54TypePilot for secure Scala
- 23:41Live demo and evaluation
- 25:45Will LLMs generate safe code?
- 27:10Future LLM-Scala directions
- 27:54Q&A
related talks
32mSafer Code with LLMs: Scala Types Silver Bullet?
30mFormal verification of Scala programs with Stainless
30mEfficient programming with Scala and LLMs
53mSemantics-based program manipulation in the age of LLMs
33mVerifiably Safe Agentic Compute
01h 00mAI Safety through Programming?
22mTowards Verified Code Reasoning by LLMs
21mA Case Study on the Effectiveness of LLMs in Verification with Proof Assistants