Anda Tidak Bisa Melakukan Unit Test pada Protokol Terdistribusi, tetapi Anda Bisa Melakukan Model Checking
Bug terdistribusi mahal untuk diperbaiki setelah deployment. Model checking memungkinkan Anda menemukannya sebelum menulis satu baris kode implementasi pun. Berikut cara melakukannya dengan TLA+.