Episode notes
For decades, formal methods were considered theoretical exercises locked in academic labs—too brittle, complicated, and expensive for most production software. But as vital systems and AI-driven infrastructure face ever greater challenges, just testing edge cases by hand is no longer enough. Today, we're joined by Anjana Rajan and Jonathan Ring, co-founders of Atalanta, to explore how they are bridging the software understanding gap. They break down how to take high-level mission objectives and translate them into code-level proofs without needing a PhD in mathematics. From securing…
Podcast
The BugBash Podcast
Antithesis · Tech & Science · English
The BugBash podcast is a lively look at all aspects of software reliability, by enthusiasts, for everyone. Each episode brings leading engineers and researchers together for deep dives on everything from formal methods to testing to observability to human factors. There’s concrete advice on best pr
More from The BugBash Podcast All episodes →
-
S3 · E9 · 7 Oct 2026 · 48 min
Retrofitting Proofs onto Existing Rust Codebases
In this episode we sit down with Jay Lorch and Chris Hawblitzel from Microsoft Research, along with Sr Engineer Shuxian Wang from Antithesis, all to talk about Verus. We break down how to retrofit proofs onto code you have already shipped, without starting over from scratch. Learn how modern SMT solvers check your code at compile time, why Rust ownership maps naturally to separation logic, and what happens when AI coding agents try to cheat their way through mathematical proofs.
-
S3 · E8 · 1 Oct 2026 · 49 min
Beyond Academic Proof: Scaling Provable Correctness in Production
Many elegant theoretical proofs exist for distributed systems, but local hardware and production realities rarely play by the rules. Today, we're joined by UIUC professors Ram Alagappan and Aishwarya Ganesan, along with Antithesis Sr Engineer Michael Vaughn, to explore what it actually takes to build resilient architectures. We look at how recovery protocols can actively backfire under disk faults, how novel storage interfaces let us achieve high performance without sacrificing guarantees, and why the emergence of autonomous agents is forcing us to rethink data infrastructure from the ground…
-
S3 · E6 · 17 Sep 2026 · 43 min
An Oceanographer Talks About Scientific Rigor in Software Engineering
Can thinking like an idealistic scientist make you a better developer? In this episode, Deepak Cherian, oceanographer turned software engineer joins the show to discuss the massive data deluge facing scientists—and what’s being done to keep up. Discover how Deepak’s team is building Ice Chunk to bring database-level transactions to n-dimensional datasets, how property-based testing acts as the ultimate automated peer reviewer, and why software engineering might benefit from embracing the scientific method a little more vigorously. And if you like conversations like this, you’ll want to join…
-
S3 · E5 · 9 Sep 2026 · 40 min
Virtual Time on a Deadline: Building an Open-Source Deterministic Hypervisor
Building a deterministic hypervisor is an incredibly difficult feat of engineering. Doing it as a bachelor’s thesis in just four months is even more so. In this episode, David Wynn sits down with Peter Graugaard and Nicholas Kristensen, the creators of Dhyv—an open-source deterministic hypervisor they wrote for their undergraduate thesis at the Danish Technical University. Inspired by Antithesis, these two software engineering students dove straight into CPU manuals, custom kernel patches, and the brutal realities of virtualizing time. Listen to how they survived the crunch, wrangled the…
-
S3 · E4 · 2 Sep 2026 · 39 min
Replication Before Raft: 15 Years of Correctness at MongoDB
AI makes writing code faster, but shouldn’t it make software better, too? Today, Jesse Jiryu Davis, Senior Staff Research Engineer at MongoDB joins Carl Sverre to discuss why the time saved by AI should be reinvested and not squandered. Jesse talks about MongoDB’s journey with formal verification – and his own. He shares what it was like to build a custom replication protocol using TLA-plus, and how he realized that you can work in TLA-plus without a PhD. Jesse and Carl also talk about the future of formal methods – the impact of AI, the advent of simple but powerful tools like Antithesis,…
-
S3 · E3 · 26 Aug 2026 · 54 min
The People Behind the Hamsters and Other Stories of Downtime
Behind every catastrophic system failure is a room full of stressed-out people trying to fix it. Launched in 2021, the Downtime Project was a podcast run by two seasoned distributed system engineers, who dissected post-mortems published after notable outages. Today, those two engineers, Jamie Turner and Tom Kleinpeter join David Wynn on the Bug Bash podcast to talk about their collaboration and what they learned. The two Dropbox veterans look back at the war rooms of the internal incidents behind their service and others. We dive into the emotional toll of managing outages, why zero-blame…
-
S3 · E2 · 19 Aug 2026 · 1 hr 13 min
From 18 months to 6: High-velocity database engineering
In this episode, Carl Sverre and David Wynn sit down with Philip O'Toole, creator of rqlite. We dive into his philosophy of using tests as a core design strategy, his tactical advice for turning AI agents into technical research assistants, and how leveraging AI tools compressed his typical 18-month release cycle down to just six months. If you’re interested in a principled approach to solo projects in the AI era, or where the future of AI swarm management for critical infrastructure might be going, you’ll want to give it a listen.
Take it with you
The Melo app keeps playing with the screen off, works in the car and on your watch, wakes you to your station, and browses the whole catalogue offline. Free, no ads, no account.
