No puedes hacer pruebas unitarias de un protocolo distribuido, pero sí puedes verificarlo con model checking
Los errores distribuidos son costosos de corregir después del despliegue. El model checking te permite encontrarlos antes de escribir una sola línea de código de implementación. Así es como hacerlo con TLA+.
