In this hour-long talk from Papers We Love NYC, Alex Weisberger presents on "Performal," a formal verification approach for analyzing latency properties in distributed systems. Explore how Performal provides a framework for stating and proving worst-case latency bounds while abstracting away the complexities of real-world infrastructure. Learn how this method pairs formal reasoning with performance measurements to accurately estimate end-to-end latency. The presentation covers the paper published in ACM (https://dl.acm.org/doi/pdf/10.1145/3591235) and is sponsored by Datadog. Alex Weisberger, a full-stack engineer at Datadog working on Database Monitoring, shares his expertise in applying formal methods to practical engineering challenges, including property-based testing, model-based testing, TLA+, and simulation.