Your Code Has Bugs. Lean4 Has Proofs. A Practical Guide to Formal Verification for Engineers
Varun Pant
- When
- Wednesday, July 111:40 AM – 12:00 PM · 20 min
- Where
- Leadership 1San Francisco, CA · imported from ai.engineer's public schedule feed
About this session
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
Speaker
More in AI-Native Enterprises
- Building the engine while flying the plane — launching the Figma MCP serverTuesday, June 30 · 11:10 AM – 11:30 AM · Leadership 1
- Agentic SDLC at Uber: Building Blocks for Uber's Software FactoryTuesday, June 30 · 11:40 AM – 12:00 PM · Leadership 1
- Scaling Code Quality: Building uReview, Uber’s Multi-Agent Code Review EngineTuesday, June 30 · 12:05 PM – 12:25 PM · Leadership 1
- AI Evals Platform for Cross-Functional Teams at ScaleTuesday, June 30 · 1:55 PM – 2:15 PM · Leadership 1
- Productionizing LLM Gateways: Architecture, Tradeoffs, and Hard Lessons from the TrenchesTuesday, June 30 · 2:25 PM – 2:45 PM · Leadership 1
For developers: this programme is open data — JSON, iCal, schedule XML and an MCP endpoint.Show endpointsHide
- JSONEvery published session and speaker, in one request./aie-worldsfair-2026-import/feed.json
- iCalSubscribe in Google, Apple or Outlook Calendar./aie-worldsfair-2026-import/feed.ics
- Schedule XMLfrab / pentabarf — the format conference apps import./aie-worldsfair-2026-import/feed.xml
- MCP + RESTPoint Claude at the programme. OpenAPI 3.1 included./agents
No key, no signup, CORS open. Everything here is generated from the same data the organisers edit.