tlaplus

분산 프로토콜은 단위 테스트할 수 없지만, 모델 검증은 할 수 있다

분산 버그는 배포 후 수정 비용이 많이 든다. 모델 검증을 사용하면 구현 코드를 한 줄도 작성하지 않은 상태에서 그 버그를 찾을 수 있다. 다음은 TLA+를 이용한 방법이다.