This video from AWS re:Invent 2023 explores how formal methods can improve the design and testing of distributed systems. Ankush Desai and Bikash Behera introduce P, an open-source framework used by AWS to model and verify complex distributed protocols. They demonstrate how P allows developers to express system designs as communicating state machines and systematically check for correctness before implementation. The speakers highlight how integrating formal methods like P into the development process helps catch design flaws early, increases confidence in system resilience, and ultimately boosts developer productivity when building mission-critical distributed applications. Through examples like modeling a two-phase commit protocol, they show how P enables rigorous verification of system properties without requiring advanced mathematical knowledge. The session provides practical guidance for AWS customers to leverage P for validating their own distributed workloads.