What sort of cycle-accurate simulation are you proposing, exactly (I assume you're aiming for something pretty accurate if your simulation is going to figure ou

What sort of cycle-accurate simulation are you proposing, exactly (I assume you're aiming for something pretty accurate if your simulation is going to figure out performance-related problems!), and how will it be improved by dependency injection? If you just want to simulate a network, why not use something like http://mininet.org/ http://mininet.org/? (Also: formal proofs of correctness for stuff like leader election are very much concerned with stability / liveness, not just safety; that's a common misconception).