Probably Proven

Formal verification gives you a mathematical yes or no. A large language model gives you its best guess. What happens when the LLM writes the properties and drives the proof? Prof. Ziyad Hanna, Corporate Vice President of R&D and Strategic Head of AI at Cadence Design Systems, returns to Wearing Flip-Flops with host Ronen Laviv. Ziyad worked on formal verification at Intel and led R&D for the Jasper formal verification platform, so this one goes deep on the discipline he grew up in. In this episode: - When formal verification moved from research into everyday engineering - LLMs in front of formal engines: a category error, or what makes AI safe to use? - AI-generated assertions, and weak properties that prove trivially and still show green - Bounded proofs: does AI make them more trustworthy, or just more comfortable? - State space explosion and the formal skills barrier: what AI solves, and what it might hide - Formal apps vs AI agents, and how many engineers can now drive Jasper on their own - Where the line between formal and simulation sits in 2026 - Agents launching hundreds of simulation and formal jobs: who schedules them, and where they run - Verification in the cloud: cloud-native or lift and shift, burst capacity, spot instances and checkpointing long proofs - Who watches the compute farm at 2am when agents run unattended Part 1 with Ziyad, Who Signs the Tapeout?, covers agentic AI in chip design and who owns a silicon failure. Enjoyed the episode? Rate and review Wearing Flip-Flops on Apple Podcasts or Spotify, or subscribe on YouTube. It takes a minute and helps other chip designers find the show. Want to be a guest? If you work on formal verification, chip design or the silicon behind AI and have a story worth telling, reach out: https://wearing-flip-flops.com/contact Follow the show on LinkedIn: https://www.linkedin.com/company/wearing-flip-flops Wearing Flip-Flops is a hardware podcast for chip designers, with deep dives into verification, emulation and the silicon powering AI.