Alloy allows verifying a model's correctness by... [1] ... automatically checking all instances within a certain scope 2 ... automatically constructing a proof using the SAT-solver (or finding a counterexample) 3 ... checking whether there are any counterexamples and concluding that the model is valid if there aren't any Message for correct answer: Alloy cannot automatically prove that a model is valid in general but can be used to check whether it is correct up to a certain size. As most errors usually already occur in small instances, using Alloy to exhaustively check a finite scope allows us to gain a fair level of confidence in our model. Message for wrong answer: You might want to read the Introduction and Statics I again.