Accompanying Repository for The Verification of a Distributed System Talk to be given at

• GOTO Chicago 2016: [Slides][Video]
• Qcon New York 2016 [Slides][Video]
• YOW Melbourne 2016 [Slides]
• YOW Brisbane 2016 [Slides]
• YOW Sydney 2016 [Slides]

Distributed Systems are difficult to build and test for two main reasons: partial failure & asynchrony. These two realities of distributed systems must be addressed to create a correct system, and often times the resulting systems have a high degree of complexity. Because of this complexity, testing and verifying these systems is critically important. In this talk we will discuss strategies for proving a system is correct, like formal methods, and less strenuous methods of testing which can help increase our confidence that our systems are doing the right thing.

• The Verification of a Distributed System
• Formal Specifications
  • Specifying Systems
  • Use of Formal Methods at Amazon Web Services
  • The Coq Proof Assistant
• Simple Testing Can Prevent Most Critical Failures
• Property Based Testing
  • Haskell: Quick Check
  • Erlang: Quick Check
  • Other Quick Check Implementations
  • ScalaCheck
  • 29 GIFs only ScalaCheck Witches will Understand
  • Quick Checking Riak
  • Testing Eventual Consistency in Riak
  • Combining Model Checking and Testing
  • Testing AUTOSTAR Software with QuickCheck
  • Modeling Eventual Consistency Databases with QuickCheck
  • The Mysteries of Dropbox
• Fault Injection
  • Jepsen
  • Netflix Simian Army
  • Game Days
    • Resilience Engineering: Learning to Embrace Failure
    • Game Day Exercises at Stripe: Learning from kill-9
• Systems Complexity Model from Architectural Patterns of Resillent Distributed Systems
• Areas of Research
  • Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems
    • The CISE Tool: Proving Weakly Consistent Applications Correct
    • CISE Tool Demo
    • Github: Syncfree/CISE
    • Syncfree CISE website
• IronFleet: Proving Practical Distributed Systems Correct
  • Dafny
• Lineage-Driven Fault Injection aka Molly
  • Lineage-Driven Fault Injection
  • Sigmod 2015 Slides
  • Automated Failure Testing at Netflix
  • "Monkeys in Lab Coats": Applied Failure Testing Research at Netflix
  • Automating Failure Testing Research at Internet Scale
  • Orchestrated Chaos: Applying Failure Testing Research at Scale
• Towards Property Based Consistency Verification
• Certified Causally Consistent Distributed Key Value Stores
• Planning for Change in a Formal Verification of the Raft Consensus Protocol

Caitie McCaffrey is a Backend Brat and Distributed Systems Diva at Twitter. Prior to that she spent the majority of her career building large scale services and systems that power the entertainment industry at 343 Industries, Microsoft Game Studios, and HBO. Caitie has a degree in Computer Science from Cornell University, and has worked on several video games including Gears of War 2, Gears of War 3, Halo 4, and Halo 5. She maintains a blog at CaitieM.com and frequently discusses technology on Twitter @Caitie