Skip to content
The BugBash Podcast cover art

Antithesis

The BugBash Podcast

A Technology podcast

Good podcast? Give it some love!

About the show

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 practices, and nuanced discussion of how these strategies combine to deliver software that works. And if you’re enjoying these conversations, check out the talks from BugBash 2025 on YouTube, and join us at BugBash 2026 on April 23-24, 2026, in Washington DC!

Newest episodes

Retrofitting Proofs onto Existing Rust Codebases

47 min

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.

Beyond Academic Proof: Scaling Provable Correctness in Production

49 min

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.

Stop Talking About Formal Methods

47 min

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 autonomous nuclear reactors to creating resilient space architectures, discover how formal verification is moving from an academic ideal to an accessible engineering reality.

Similar podcasts

All episodes

Retrofitting Proofs onto Existing Rust Codebases

47 min

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.

Beyond Academic Proof: Scaling Provable Correctness in Production

49 min

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.

Stop Talking About Formal Methods

47 min

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 autonomous nuclear reactors to creating resilient space architectures, discover how formal verification is moving from an academic ideal to an accessible engineering reality.

An Oceanographer Talks About Scientific Rigor in Software Engineering

42 min

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

Virtual Time on a Deadline: Building an Open-Source Deterministic Hypervisor

40 min

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

Replication Before Raft: 15 Years of Correctness at MongoDB

39 min

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.

The People Behind the Hamsters and Other Stories of Downtime

53 min

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.com The 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.

From 18 months to 6: High-velocity database engineering

1 hr 12 min

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.

A Wild Hypothesis: The Python Library that Kills PhDs

1 hr 2 min

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.

Dev in the Street

35 min

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.

Why simple workloads find the hardest bugs

57 min

You hit 100% test coverage, deploy to production, and the system still falls over. An old story, maybe aside from the 100% coverage percent part. In this episode, David sits down with Marco Primi and Sean Allen from the Antithesis Red Team to talk about a likely missing piece in your testing strategy: workloads. They break down exactly what workloads are, why they are so helpful for testing distributed systems, and the biggest pitfalls engineers hit when trying them out. They talk about why you have to let go of deterministic, "happy path" testing, and how even a workload as "dumb" as a basic `while true` loop can expose silent data loss that your unit tests would never catch.

Programming as an Act of Building Vocabulary

49 min

Why do LLMs struggle to build complex architecture?  According to Unmesh Joshi, Distinguished Engineer at ThoughtWorks, it often comes down to a lack of shared abstractions, of a shared vocabulary. Today he joins Will Wilson and David Wynn to unpack how we learn about, build, and test distributed systems. We cover the value of building miniature versions of systems like Kafka to grasp the basics, why Deterministic Simulation Testing (DST) is a highly effective tool for teaching as well as finding bugs , and why Guy Steele's 1998 keynote holds the secret to successfully collaborating with modern AI tools.

The Dollar Bet that Fuzzed Figma: Exploding Laptops and UI Reliability with Jonathan Chan

51 min

Can you stress-test a React UI completely hands-free? In this episode, Oskar Wickström and I are joined by Jonathan Chan to discuss the origins of Fuzzmap. From a janitor’s closet in Figma—where end-to-end tests once lived on a "spicy pillow" MacBook—Jonathan shares how he applied coverage-guided fuzzing (inspired by AFL) to the world of web front-ends. We dive into the gnarly hacks required to instrument React, the challenges of visualizing complex state machines, and the future of "full-stack" fuzzing in the age of LLMs and team agents.

Semmathesy and the Agentic Era: Learning Systems in 2026

51 min

With the "Agentic Era" coming online, teams are onboarding new AI "minions" into our codebases every thirty minutes. So a critical question emerges: Are we actually becoming more productive, or just more busy?Jessica Kerr (Jessitron) joins me to explore symmathesis—the theory of learning systems made of learning parts. We dive into viewing software as a teammate, how the definition of "legacy code" is shifting to anything an AI can't understand, and why our most important human contribution is moving from writing lines of code to orchestrating the flows of learning across the entire system.We dive into the shifting boundaries between the social and technical worlds, and why the "productivity unlock" of AI might actually make software engineering a more human endeavor than ever before.

From Scale to Rigor: An Engineering Journey at Meta and Oxide

1 hr 1 min

Today we’re talking with Rain from Oxide Computing, tracing their journey from the massive, data-driven scale of Meta to the high-stakes, air-gapped world of shipping a 'cloud in a box'. We talk about moving from an environment of over 10,000 engineers—where a 10% tooling improvement is worth a thousand people—to a culture where you’re shipping hardware that simply cannot be patched once it leaves the building. Rain shares how they realized that technical writing is a senior engineer’s ultimate force multiplier for justifying complex designs. We also dive deep into the 'invisible superpower' of property-based testing and using Oracles to kill bugs in the developer’s inner loop long before they ever have a chance to reach production. Mentioned: https://rfd.shared.oxide.computer/rfd/0576 Further reading: https://oxide-and-friends.transistor.fm/episodes/engineering-rigor-in-the-llm-age

Escaping the Spaghetti: How to Test Untestable Codebases

58 min

Everyone wants reliable software. But nobody wants to test messy legacy code. Today, Lewis Campbell from Outdata joins the show to share a practical approach for bringing deterministic simulation testing to existing systems.  We get into why React components are terrible for business logic, and why front end static typing stops non-determinism at the door. We also take on non-tech aspects, like the politics of updating old code bases, the danger of hiding data conflicts, and how to ease your team into property-based testing. There’s even an Internet-hungry sheep named Angus.

How rr Became a Protected Species: A Story of Necessary Hacks

51 min

Building the rr replay debugger wasn't about academic purity. It was about survival. Today, creator Rob O'Callahan reveals the "necessary” complexity that makes time-travel debugging possible on Firefox. We dig into the engineering nightmares behind the tool: from patching 2-byte system calls to the constant fear of silent hardware failures. Rob explains how rr became a "protected species" inside the Linux kernel—and why messy, manual hacks often beat six months of theoretical work.

Re-Designing Data-Intensive Applications: The Shift to Cloud-Native Storage

1 hr 20 min

It’s been nine years since Designing Data-Intensive Applications became the standard text for distributed systems. Today, Martin Kleppmann and Chris Riccomini join the show to pull back the curtain on the upcoming Second Edition. After all, the era of local disks are giving way to cloud-native object storage. So we discuss why modern databases are being rebuilt entirely on top of S3. From there, we revisit the CAP theorem—and why it might be time to retire it in favor of "offline availability." We also get into a surprisingly practical debate on AI, exploring how LLMs might be terrible at creative design but perfect as "test oracles" for verifying complex system migrations. You’ll want to stick around for this one.

Hypothesis vs. Hallucinations: Property Testing AI-Generated Code

1 hr 18 min

Large Language Models can generate code in a flash, but that code is notoriously unreliable. Traditional unit tests often can’t put enough guardrails in place to ensure correctness… even if they’re written by the LLM itself. This is where property-based testing (PBT) becomes essential. Today, we're joined by David R. MacIver, creator of the PBT library Hypothesis, and now an Antithesis employee! We discuss how to build robust feedback loops that are needed to make AI-generated code trustworthy. We'll cover why standard AI coding benchmarks are flawed, how Hypothesis makes PBT approachable, and the challenge of getting developers to think in "invariants." David also shares his perspective on the future of AI in software engineering. If you want to build a reliability backstop for your code, vibed or otherwise, stick around.

From the Lab to Production: Making Cutting-Edge Testing Practical

39 min

Software testing research is exploding, but in practice, most companies' testing approaches seem stuck in the past. Where does that gap come from? It often boils down to the distance between academic promises and the practical needs of developers who need usable tools and fast results. In this episode, David talks with Rohan Padhye, head of the PASTA research group at Carnegie Mellon University, who has lived on both sides of that divide. They explore how fuzz testing crossed that chasm—from industry curiosity to academic focus and back again—and what it will take for other techniques to do the same. Rohan shares insights on designing testable software, building a robust testing culture, and what truly makes a "good" property for finding bugs.

Ergonomics, reliability, durability

40 min

Integrating non-deterministic, non-durable elements like AI agents into our workflows tends to lead to a lot of do-overs. But restarting AI processes can be costly, burning through tokens and losing valuable progress. Wouldn’t it be easier if there was always a clear checkpoint to restart a task from? Today I talk with Qian Li, co-founder of the DBOS durable execution engine, about reliability, ergonomics, and actually understanding your software. We discuss the long history of checkpointing, mental models, and how using durable execution allows systems to resume right where they left off after a crash. It makes your software resilient by default. Learn how this architectural pattern can impact an AI-assisted or any complex system that could use a little improvement in how developers work with it.

No actually, you can property test your UI

54 min

How do you test for bugs that only appear when a user clicks frantically, or when asynchronous data loads in an unexpected order? Standard UI tests often miss the subtle stuff that happens all the time in the stateful, dynamic applications. In this episode, Paul Ryan and I sit down with Oskar Wickström, creator of the QuickStrom framework, among other things, to explore how to apply generative testing to the complex world of user interfaces.  Oskar argues that you don't need to be a formal methods genius to get real value out of the approach. Even simple properties can uncover deep bugs, like ensuring a loading spinner eventually disappears or that the screen never goes blank.  If you've been intrigued by property-based testing but intimidated by the thought of writing complex formal models for UIs, stick around. 

Slow down to go fast: TDD in the age of AI with Clare Sudbery

52 min

AI coding assistants promise incredible speed, but what happens when you run straight into a wall of buggy code and technical debt? In this episode, Clare Sudbery, a software engineer with over 25 years of experience, discusses a crucial paradox for modern developers.  The secret to harnessing AI's power isn't to move faster, but to slow down. Clare explains why deliberate, rigorous practices like Test-Driven Development (TDD) are the essential "guardrails" needed to guide AI tools toward reliable, high-quality software. You'll learn why "more, smaller steps" is the key to tackling technical debt and how throwing your code away might be the most productive thing you do all week.

Fixing five "two-year" bugs per day

1 hr 10 min

Some bugs are so rare, they can take years to track down and fix. What if you could find and fix five of them per day?  For Joran Dirk Greef, the creator of the TigerBeetle database, that's not a wild dream — it's how his team works every day. While most people think building a new database takes a decade, Joran's team built TigerBeetle in just three and a half years. The key is a unique philosophy for writing software called "Tiger Style". Joran joins the show to share the secrets behind their speed and safety. You'll hear why he thinks picking C would have been a "fatal" mistake , how a strict rule about memory can force you to write better code , and why Zig was the perfect choice for TigerBeetle. The key to it all is a powerful testing method that Joran calls "existential" for any important project. If you want to hear more about how his team turns squashing impossible bugs into their normal day-to-day, stay tuned.

No really, some bugs aren’t real

41 min

When is a bug not really a bug? In this episode, host David Wynn talks with SRE veteran Dan Slimmon about a radical idea: chasing perfect code might not be the best way to make your service reliable. Dan argues that once your code is "good enough," most outages aren't caused by code defects. They're caused by weird interactions between different parts of a system or by users doing things you would never expect. He shares wild stories from his career, including how a tiny database hiccup created a massive, repeating traffic jam and how a single user crashed servers by uploading a 3.2-gigabyte config file. This conversation will make you rethink what you thought you knew about bugs, quality, and what "reliability" truly means.

Every map is wrong, but we made one anyway

53 min

Every map of a complex territory is inherently wrong, but without one, we're completely lost. So what happens when the territory is the vast, ever-changing landscape of distributed systems? In this episode, David Wynn sits down with Kyle Kingsbury, the renowned researcher behind Jepsen, to discuss a monumental effort to chart this landscape: the new Distributed Systems Reliability Glossary. Kyle explains why he and T.W. Lim from Antithesis felt the need to "put this all in one place," creating a practical roadmap for testers and engineers navigating the field. They explore the challenge of creating "directionally correct" definitions , the surprising "urban legends" that persist in system design (like yelling at hard drives to increase error rates ), and why even the most rigorous formal models can drift from the code they're meant to describe. Tune in for a deep dive into the subtle bugs that defy simple explanations , the future of reliability in the age of AI-generated code, and the one problem Kyle is still determined to solve in his own work: reproducibility.

Fail loudly, fail fast, fail in production

52 min

Is it just a fact of life that software is broken? Our industry often operates as if the answer is "yes." We write tests, we fix bugs, but we seem to accept a certain level of failure as the cost of doing business. Our guest today is tired of it. Isaac Van Doren is a software engineer at Paytient, a healthcare payment solutions provider,   and he’s "sick of software being broken all the time". Isaac makes the provocative case for a radical cultural shift in how we approach software reliability. He argues that we need to move beyond the narrow view that reliability simply equals testing and instead adopt practices that force us to be explicit about the rules of our systems. Listen to explore a different philosophy of development—one where engineers are fully responsible for defining business logic , assertions are a tool for building a "theory of the system" , and failures in production are not just bugs, but immediate, unmissable signals that our understanding was wrong. This conversation will challenge your assumptions and give you a new vocabulary for building software that, as Isaac puts it, "actually works".

Scaling Correctness: Marc Brooker on a Decade of Formal Methods at AWS

1 hr 7 min

How do you prove the correctness of services that underpin a huge portion of the internet?  At the scale of Amazon Web Services, traditional testing falls short. In this episode, Antithesis’ own Will Wilson and Ben Collins talk with Marc Brooker, a Distinguished Engineer who has spent nearly 17 years building core AWS infrastructure like S3, Lambda, and Aurora Serverless. Marc gives us the inside story on AWS's decade-long journey with formal methods, from the early days of using complex tools like TLA+ to the current focus on "lightweight" approaches that any engineering team can adopt. He shares the counterintuitive lesson learned at AWS: investing in correctness up front doesn't just improve reliability, it actually boosts development velocity and leads to faster delivery. We also explore the convergent evolution of deterministic simulation testing, the challenge of applying these techniques to user interfaces and control planes , and what role AI will play in the future of programming and verification.

FoundationDB: From Idea to Apple Acquisition

40 min

The BugBash Podcast kicks off with a bit of pre-history -- the story of FoundationDB, one of the first companies to successfully use deterministic simulation testing to accelerate development, assure reliability, and build something legendary. Today, FoundationDB is the hidden layer in Snowflake, DeepSeek, and many core systems at places like Apple and Goldman Sachs. But it started with some guys in a garage, building a system demo with plywood and lightbulbs...

–

0 ratings from members

5
4
3
2
1

Rate this podcast

Log in to rate and review the shows you listen to.

No reviews yet — be the first member to rate "The BugBash Podcast".

This podcast, its content and its artwork are not owned by, affiliated with, or endorsed by Castquire.

Keep listening

Discover more podcasts like this.

Up next

  1. Nothing queued. Use + Queue on any episode to line it up.

0:00 0:00