There’s a popular theory that AI will finally make formal verification mainstream because mathematical proof of correctness will be needed when machines write most or all of the code. But will this happen? Hillel Wayne is one of the best people to answer. Timestamps: 00:00 Intro 04:32 The Crossover... Project 11:37 What software engineering does better 15:30 What traditional engineering does better 18:17 Formal methods 29:32 TLA+: what it is and demo 36:58 TLA+ at Amazon 38:10 Ways distributed systems break 41:03 Formal methods and systems thinking 46:20 The value of learning math 50:23 What TLA+ is good for and isn’t 52:50 Alloy: a declarative language for software modeling 58:53 Other formal methods tools 1:01:24 Property-based testing 1:05:31 AI and the need for formal verification 1:12:29 Logic for programmers 1:14:35 Hillel’s 2025 prediction on AI’s impact 1:21:30 Book recommendation Brought to you by: • Antithesis – verify your system’s correctness without human review or traditional integration tests – and avoid bugs or outages. • turbopuffer – a vector and full-text search engine built on object storage. It’s fast, cheap, and extremely scalable. • WorkOS – everything you need to make your app enterprise ready. Two things I found especially interesting, talking with Hillel: 1. Amazon used TLA+ to find a bug almost impossible to locate without formal methods. In the paper How AWS uses formal methods, the AWS team shared that they’d found a complicated bug for which the shortest error trace to exhibit was 35 steps (!!). The bug passed unnoticed through extensive design review, code reviews, and testing. AWS concluded they wouldn’t have uncovered it if they’d stuck to conventional testing approaches. 2. Why not use formal verification for everything, then? It’s because specs in the real world are a nightmare to write. Even a simple problem like “find the file in a directory that has the most lines” gets complicated when modeled with formal methods. We would have to answer questions like: ‘do we look at ASCII or UTF-8 new line characters, what about unreadable files, and Symlinks?’ Without formal methods, we can write a simple verification that is right in 99%+ of cases. Formal methods require a lot of extra effort for the less than 1% of exotic use cases!show more

I saw the first one second flash of "formal methods" and thought "is it Hillel??" It's Hillel! I learnt so much from his blog: Great idea to chat with him about LLMs + verification.

Watch or listen on other platforms: • YouTube: • Spotify: • Apple:

specs are the hard part

That AWS 35-step bug trace is exactly why I stay away from distributed systems.

Hillel is the GOAT of formal methods 😎

I've been looking at this recently (in Lean, not TLA+). The results are very encouraging:

AI may be best at drafting the ugly first spec—humans are better at arguing over UTF-8 and symlinks than staring at a blank TLA+ file.

Isn't this what @VictorTaelin is working on

Yes — formal verification is the future of AI-assisted programming. AI can now churn out code at scale and at near-zero cost. Humans simply cannot keep up with reviewing it all. Formal verification is the only way out.

ai will probably just get better at hallucinating proofs.

AI can probably accelerate writing specifications, but the difficult work remains choosing the right invariants and abstraction boundaries. Do you expect AI to uncover missing assumptions, or mainly make model construction and checking more accessible?

formal methods for the scary 1%, good specs for the messy 99% :D

The proof is only as good as the spec. More AI in the pipeline raises the stakes for that spec work. So who should design the spec AI or humans?

Hillel's take usually: tools improve, but someone still has to write the spec. That bottleneck doesn't go away.

Me pregunto cómo se manejó el transcripts de los episodios, si se utilizó algún tipo de automatización o LLM para generarlos.

AI may make formal methods more attractive and more frustrating at the same time. It can help write the proof, but someone still has to decide what ‘correct’ means—including the ugly UTF-8 and symlink questions. The scarce skill may move from producing code to specifying reality precisely.

Ah chat with Hillel, I need to watch this!

Unless you can convince me we can suddenly become all mathematicians, and start writing in pure Math, I doubt people going to use TLA+ to write specs for UI, APIs, services, and so on. Here's an example of a simple system for you. URL shortener app. - HTML page for adding a URL with input and button - Enter the URL in the input - Click the button - "OK" modal appears + short URL - The request is sent to the API endpoint - The entry { original, short } appears in the database Now, if you try generating Lean for this, it would look crazy: (I can't fit it on my 1440p monitor, almost 200 lines of code) And this is all Math. Not Python or Ruby, or any programming language you're familiar with. Now, lemme explain the bottleneck. 1. You create this mental model (the drawing) in your head 2. You map this to intent you wrote as your product spec (6 bullet points) 3. You read the code/proof 4. You have to verify intent == code/proof #4 is the __main bottleneck__ If you have this drawing, it removes cognitive effort of visualizing this tiny system you are verifying. What I want to do is to be able to generate these diagrams/drawings and let programmers interact with them, or observe how they work when connected together. And I don't think Lean proofs are gonna help us at this stage yet. THE END.

People think the hard thing is evaluating what a function is supposed to do. But the hardest thing is really understanding 100% yourself what a function is supposed to do and being able to articulate that.

Who proves the proof?

Have you checked out Erik Meijer's CACM paper "Guardians of the Agents"? Nada Amin implemented it and I made an opencode plugin for it

The specification gap matters for AI refactoring too. Comparing old/new behaviour can expose an undocumented assumption, but agreement cannot tell us whether that assumption is right. I’d combine those comparisons with independently reviewed invariants for the highest-risk flows. My practical QA example:

@VictorTaelin