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:

• @AntithesisHQ – verify your system’s correctness without human review or traditional integration tests – and avoid bugs or outages. https://antithesis.com/pragmatic

• @turbopuffer – a vector and full-text search engine built on object storage. It’s fast, cheap, and extremely scalable. https://turbopuffer.com/pragmatic

• @WorkOS – everything you need to make your app enterprise ready. https://workos.com

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!

Redirecting…

Source: https://antithesis.com/pragmatic/ Redirecting to/?utm_medium=podcast&utm_campaign=pragmatic_2026&utm_source=pragmatic&utm_content=pragmatic_20260513