---
title: "Your Code Has Bugs. Lean4 Has Proofs. A Practical Guide to Formal Verification for Engineers"
category: "talks"
date: "2026-06-30"
time: "11:40am-12:00pm"
track: "AI-Native Enterprises"
room: "Leadership 1"
speakers: ["Varun Pant"]
sourceLabels: ["Official conference schedule", "Public YouTube metadata"]
scheduleTrack: "AI-Native Enterprises"
scheduleRoom: "Leadership 1"
scheduleLabels: ["AI-Native Enterprises", "Leadership 1", "session", "confirmed"]
---
# 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
- [[varun-pant]]

## 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|Varun Pant]] — Builder, NeuroSymbolic AI at [[aws|AWS]].

### Topics Covered
- [[coding-agents]]

### 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.