I think there's also a level of "it's doing something weird in practice, I know why it's doing that weird thing". I've been working with a team on TLA+ specs and it's surreal how often I can divine bizarre behaviors from the error messages