Jason Gross comments on Formal verification, heuristic explanations and surprise accounting