Hacker News new | ask | show | jobs
by mcguire 2708 days ago
Normal testing feeds selected inputs to the software and succeeds for the corresponding output.

QuickCheck feeds random values to the software and looks for "good" results.

TLA+ takes a model of the system (not the software) and explores the entire state space and looks for anything that violates given logical predicates. It is a different later of abstraction.