Imagine you have developed a spacecraft that is super-safe, because following the trends, you have applied model-based design and testing. All components modeled by statecharts, tested, implemented by automatically generated code, what can go wrong? Then on the day of launch, the whole thing explodes in a spectacular fireball. The cause? Interactions. The cure? Formal verification.