We discuss using formal run-time verification techniques in conjunction
with very detailed simulations of ad hoc routing protocols in the NS
network simulator.  Our analysis has found violations of significant
high-level protocol properties.  We also discuss debugging strategies
that utilize the interplay between the simulation and verification
engines.