There has been recently some activity here in HN regarding formal model checking and protocol verification (TLA+, SPIN, Promela...) I guess they are relevant t

There has been recently some activity here in HN regarding formal model checking and protocol verification (TLA+, SPIN, Promela...) I guess they are relevant to this case. This stuff is hard.