When AI Writes the Code, Who Proves It Works? - The Data Exchange

In a podcast interview, Leo de Moura discusses how artificial intelligence is transforming formal verification through autoformalization and tools like Lean, making machine-checked proofs more accessible for software engineering and mathematics. The conversation explores the practical differences between testing and formal verification, the concept of a verified software stack, and how frontier models are reducing the cost of proving program correctness. Open article →