Can you define equivalence classes (mutations that shouldn't change the result) eg timing, order of events, idempotence, etc? So that you can use (3) to define the correct result for all members of the class

(Sorry if this is explained in the talk - I'll watch it but it's now too late in the day in my timezone)