The BugBash Podcast

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.

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

Anjana Rajan, Atalanta CEO and former assistant national cyber director, and Jonathan Ring, Atalanta COO and former CIA cyber operator, explore formal verification beyond academia. They discuss translating mission goals into code-level proofs, securing critical infrastructure and autonomous systems, and connecting policy, architecture, hardware, and software. They also examine AI’s role, domain expertise, and why clearer software understanding is essential for resilient systems.

Deepak Cherian is an oceanographer turned software engineer building cloud platforms for scientific data. He explores the data deluge reshaping research, IceChunk’s database rigor for n-dimensional datasets, and property-based testing as an automated peer reviewer. The conversation connects ocean modeling, conservation laws, metamorphic tests, and the scientific method to more rigorous software engineering.

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 chaotic spectrum of determinism, and built "AI-friendly" CLI tools to automate their massive testing pipelines. Joining him for the conversation is Alex Pshenichkin, the architect of Antithesis’ own deterministic hypervisor. And if you like conversations like this, you’ll want to join us at the first ever European edition of the Bug Bash conference, happening on September 30 in Copenhagen. Check it out at bugbash.antithesis.com

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, and Jesse’s predictions about the future of code review.

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 cultures are mandatory for survival, and the stories that we only tell over beers years after the fact. And of course, AI worms its way into the conversation as well.It’s a look at the pride, the panic, and the people keeping real world services online, and the lessons we learn from going offline. And if you like conversations like this, you’ll want to join us at the first ever European edition of the Bug Bash conference, happening on September 30 in Copenhagen. Check it out at bugbash.antithesis.comThe Downtime Project is still online, and you can find all 8 episodes on Spotify or wherever you get your podcasts. If you’re enjoying the Bug Bash podcast, you’ll probably enjoy the Downtime Project too.

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.

What happens when your open source library changes millions of lives?In this episode, we sit down with David MacIver, Zac Hatfield-Dodds, and Liam DeVoe — three generations of maintainers of Hypothesis, the property-based testing library used by roughly 5% of all Python developers. It’s by orders of magnitude the most-widely used property-based testing tool in the world. Hypothesis has introduced millions of developers to property-based testing, and made instant converts out of many others.All three maintainers quit their PhDs to work on Hypothesis, and today they talk about just why they did that, how pull requests lead to lifelong friendships, and about the factors that led to Hypothesis’ success.

In this episode of the Bug Bash podcast, host David Wynn shares a collection of conversations recorded at Bug Bash 2026. 11 developers share their war stories about the most interesting bugs they've encountered and resolved.They talk about JDK issues on ARM architecture, kernel hangs related to NFS and half-duplex Ethernet, memory fences in Spark workloads, and complex logic bugs in iMessage.Together these conversations become a picture of what reliability-focused developers are thinking about today: the importance of formal verification, the rise of property-based testing, and how the only thing that makes systems work is our effort and care.