NuSMV reengineered the pioneering SMV model checker into an open, modular verification platform that combined symbolic state-space reasoning with a tool architecture suitable for research and industrial experimentation.
Amir Pnueli brought temporal logic into program verification, giving concurrent and reactive systems a language for safety, liveness and behavior across time.
Model checking combined temporal logic with exhaustive state-space algorithms, allowing finite-state hardware and software designs to be checked automatically and failures returned as counterexamples.
TLA+ combines state-transition modeling, temporal logic and model checking so engineers can find concurrency and distributed-system design errors before implementation.