It's easy to find TLA+ specifications which pass the model checker, but rare (and much more useful!) to see one which fails, in an informative way. In this case

It's easy to find TLA+ specifications which pass the model checker, but rare (and much more useful!) to see one which fails, in an informative way. In this case, the author adds the assertion right /= CREATURES to the spec, which evaluates to right != {Farmer, Fox, Chicken, Grain}. Basically, this asserts no state exists in which all entities have made it to the right side of the river (the goal state). If the TLC model checker makes it to the invalid (goal) state, it will appropriately register the failure and execution trace - the state path to the goal state. Very clever!