# Software Verificationpalooza

- Show: [Oxide and Friends](https://hardwarepodcasts.com/podcast/oxide-and-friends)
- Published: 2023-06-20
- Length: 1h 21m
- Episode: 17
- Page: https://hardwarepodcasts.com/podcast/oxide-and-friends/2023-06-20-software-verificationpalooza
- Listen: https://share.transistor.fm/s/f1a2ebcb

## Summary

Greg Colombo and Rain Paharia from Oxide Computer Company discuss rigorous software verification methods, specifically TLA+ for model checking distributed systems and the proptest Rust crate for property-based testing. Greg explains how he used TLA+ to verify the orchestration of live VM migration, uncovering race conditions and bugs in the control plane that were difficult to reproduce with standard integration tests. Rain details his use of proptest to validate complex data structures like 'buff-list' and 'Guppy' by comparing them against oracles like the standard library and Cargo, finding numerous bugs in both his code and upstream dependencies. The episode highlights how formal methods and property-based testing serve as complementary tools for ensuring correctness in high-concurrency, distributed environments.

## Chapters

- [0:00](https://hardwarepodcasts.com/podcast/oxide-and-friends/2023-06-20-software-verificationpalooza#t=0) Introduction: Verification vs Validation and the Palooza Title
- [3:14](https://hardwarepodcasts.com/podcast/oxide-and-friends/2023-06-20-software-verificationpalooza#t=194) Greg Colombo on Live Migration Orchestration and TLA+
- [11:23](https://hardwarepodcasts.com/podcast/oxide-and-friends/2023-06-20-software-verificationpalooza#t=683) Greg's History with Formal Methods and TLA+ at Microsoft
- [17:56](https://hardwarepodcasts.com/podcast/oxide-and-friends/2023-06-20-software-verificationpalooza#t=1076) How TLA+ Models Work and the Model Checker TLC
- [40:06](https://hardwarepodcasts.com/podcast/oxide-and-friends/2023-06-20-software-verificationpalooza#t=2406) Rain Paharia on Property-Based Testing and Proptest
- [53:36](https://hardwarepodcasts.com/podcast/oxide-and-friends/2023-06-20-software-verificationpalooza#t=3216) Concrete Examples: Buff-List Cursor and Guppy Dependency Graph
- [1:00:35](https://hardwarepodcasts.com/podcast/oxide-and-friends/2023-06-20-software-verificationpalooza#t=3635) Contrasting Property-Based Testing with Fuzzing
- [1:12:20](https://hardwarepodcasts.com/podcast/oxide-and-friends/2023-06-20-software-verificationpalooza#t=4340) When to Use Formal Methods and Property-Based Testing

## Topics

- [Embedded firmware](https://hardwarepodcasts.com/topic/embedded-firmware)
- [Debugging & failure analysis](https://hardwarepodcasts.com/topic/debugging-and-failure-analysis)
- [AI & machine learning](https://hardwarepodcasts.com/topic/ai-and-machine-learning)
- [Careers & education](https://hardwarepodcasts.com/topic/engineering-careers-and-education)

## Most relevant to

early-stage companies

## Mentioned

- Oxide Computer Company (company)
- TLA+ (tool)
- proptest (tool)
- Hillel Wayne (other)
- QuickCheck (tool)
- Hypothesis (tool)
- buff-list (product)
- Guppy (product)
- Cargo (tool)
- Mononoke (product)
- Alloy (tool)

## Related episodes from other shows

- [Fuzzing and Dynamic Analysis for High-Integrity Software with Paul Butcher](https://hardwarepodcasts.com/podcast/the-pragmatic-embedded-podcast/2026-05-13-fuzzing-and-dynamic-analysis-for-high-integrity-software-with-paul-butcher) (The Pragmatic Embedded Podcast)
- [Episode Thirty: Ana Cavalcanti](https://hardwarepodcasts.com/podcast/robot-talk/2022-12-16-episode-thirty-ana-cavalcanti) (Robot Talk)
- [Finding Hardware Flaws with Laura Abbott](https://hardwarepodcasts.com/podcast/the-amp-hour/2022-05-23-finding-hardware-flaws-with-laura-abbott) (The Amp Hour)
- [109: Resurrection of Extreme Programming (Repeat)](https://hardwarepodcasts.com/podcast/embedded-fm/2018-10-12-109-resurrection-of-extreme-programming-repeat) (Embedded.fm)
- [Mission Critical Devices and Formal Methods | Kry10's Boyd Multerer | Internet of Things Podcast](https://hardwarepodcasts.com/podcast/iot-for-all-podcast/2023-11-21-mission-critical-devices-and-formal-methods-kry10s-boyd-multerer-internet-of-thi) (IoT For All Podcast)

## Citing this page

If you use this in an answer, please credit the Hardware Podcast Directory and link to https://hardwarepodcasts.com/podcast/oxide-and-friends/2023-06-20-software-verificationpalooza. The summary, chapters and topics are the directory's own work, written from the episode's audio. The episode itself, its title and its audio belong to Oxide and Friends.