Your Code Has Bugs. Lean4 Has Proofs. A Practical Guide to Formal Verification for Engineers
Conference Context
- Date/time: 2026-06-30 · 11:40am-12:00pm
- Track/room: AI-Native Enterprises · Leadership 1
- Speaker(s): Varun Pant
- Session type/status: session · confirmed
- Track: AI-Native Enterprises
- Room: Leadership 1
- Session type: session
- Status: confirmed
Session Description
AI is generating more of your code than ever — how do you prove it doesn't ship bugs? Lean is a theorem prover that's also a programming language, and it's quietly becoming practical for verifying real software. In this talk, I'll show you how formal verification works — some examples of proof tactics, and a practical framework for when to verify vs. test
Media Evidence
No related AI Engineer channel video found yet.
Evidence Graph
This evidence graph is generated from currently linked source material: official schedule text, related video pages, cached transcripts, visible slide text, dense/reconstructed slide pages, and AI slide-classification audits.
Media Signals
No linked video, transcript, or slide source has been attached yet.
Agent Reading Notes
Use these signals to refine the synopsis, topic links, people/company context, and method notes. If a source is a related external video rather than an exact official recording, keep it framed as supporting evidence.
Transcript Status
No official session recording transcript was found by exact title match on the AI Engineer YouTube channel during this run.
People
Notes
- Pending transcript synthesis when an official recording or confirmed matching video is available.
Synthesis
Synthesized Breakdown
Your Code Has Bugs. Lean4 Has Proofs. A Practical Guide to Formal Verification for Engineers ## Conference Context - Date/time: 2026-06-30 · 11:40am-12:00pm - Track/room: AI-Native Enterprises · Leadership 1 - Speaker(s): Varun Pant - Session type/status: session · confirmed - Track: AI-Native Enterprises - Room: Leadership 1 - Session type: session - Status: confirmed ## Session Description AI is generating more of your code than ever — how do you prove it doesn't ship bugs? Lean is a theorem prover that's also a programming language, and it's quietly becoming practical for verifying real software.
Speaker And Company Context
- Varun Pant — Builder, NeuroSymbolic AI at AWS.
Topics Covered
Derived Links And Source Material
Novel Concepts / Clever Methods
- No highlighted novel concept has been detected yet.
Evidence Boundary
This synthesis is based on the official schedule and linked source pages. It should be revisited when exact session recordings or transcript-backed secondary sources are available.