[dllthomas]

Importantly, specifying reasoning can have communicative value while falling very far short of formal verification. Personally, I also try to include a cross reference to the things that could allow "this" to happen were they to change.