Carnegie Mellon: The Rare Glitch Project                                                          E. Clarke and D. Kroenig
Why is verification hard?
Introduction
lLarge state space per node
(message area) lMany features besides message transmission (membership service, global time base, mode changes, reconfiguration, download)
lProtocol provides clock synchronization
lMust have large number of nodes
Verifying with only 2 or 3 nodes is dangerous, protocol requires 4 minimum, 20-30 nodes realistic
Each node can receive all the messages on the bus; the message area can therefore be quite large. The controller provides numerous control and status registers.

With less than four operating nodes, the clock synchronization is no longer Byzantine resilient.