With the power provided by Erlang/OTP, developing complex distributed systems is easier than ever. However, verifying the correctness of these complex systems remains a challenge. This talk will present an approach to testing that I have used at Basho which leverage's QuviQ's QuickCheck. I will present how to build a system model in QuickCheck to test an early-stage idea against random orderings of client events and server state transitions. Then, how the model can be converted into the actual intended product code. And finally, how unit tests and system tests can be extracted from the original model, with the system tests leveraging a QuickCheck harness that deploys and runs command sequences against a cluster of multiple Erlang VMs. I will also present preliminary details about integrating the Concuerror tool into this approach, as well as thoughts on generating Coq proof scripts from the original Erlang model.