Workshop: Executable Specifications for Adversarial Testing of Distributed Systems
Hands-on training for distributed systems engineers, SREs, and QA architects.
What This Workshop Is
An interactive, hands-on session that shows how to write executable protocol specifications as code and use them to systematically generate adversarial test scenarios against your implementation. We focus on systems with complex, unexpected failure modes: consensus protocols, replication, distributed transactions.
The majority of workshop time is hands-on coding. This is not a formal methods lecture. If your team has been curious about TLA+ but found it intimidating, this is the practical entry point. All code and libraries are open-source.
What Participants Learn
Write Executable Specifications
Write executable protocol specifications using practical modeling and abstraction patterns. Replace informal sequence diagrams with runnable spec executions.
Generate Adversarial Test Cases
Generate test cases via random and symbolic execution — covering both happy paths and adversarial scenarios your hand-written tests would never reach.
Build a Golden Reference Model
Use the spec as a golden reference model for differential and conformance testing. Drive tests of the implementation directly from the specification.
Establish Safety and Liveness Properties
Express and check safety and liveness properties through model checking when you need the strongest possible guarantees.
Who This Is For
Distributed systems engineers, SREs, and QA architects who are already familiar with property-based testing, fuzzing, or deterministic simulation — and want to systematically close the gap between what their tests check and what their system actually does.
No prior formal methods experience required. All examples use open-source tooling.
Format and Delivery
Available for remote or on-site delivery. Reach out to discuss scope, team size, and format. Teams leave with a working spec for their own system and a concrete technique they can apply immediately.
Interested? Limited Availability
Reach out to discuss scope and format. Remote or on-site.
