I think the interesting part isn't in a single component's edge cases at all, but in how complex webs of many, many things interact.
I've yet to see a hard debugging problem that didn't boil down to something like, in the best of possible worlds:
"component A expected something to meet promise FOO when it calls component B, because that's obvious, right?" combined with
"component B just passes requests and routes results, dude, component C is messed up" combined with
"component C never promised that behavior and if you look at our spec it even says so!"
That's an example of your "does not match what was expected" case.
I think most of formal methods is an academic waste of time. Whether they take a more formal or a more practical approach, I see high value in contract tests and data flow analysis because they're more likely to catch the bugs that cross Conway's code/org boundaries.
I've yet to see a hard debugging problem that didn't boil down to something like, in the best of possible worlds:
"component A expected something to meet promise FOO when it calls component B, because that's obvious, right?" combined with
"component B just passes requests and routes results, dude, component C is messed up" combined with
"component C never promised that behavior and if you look at our spec it even says so!"
That's an example of your "does not match what was expected" case.
I think most of formal methods is an academic waste of time. Whether they take a more formal or a more practical approach, I see high value in contract tests and data flow analysis because they're more likely to catch the bugs that cross Conway's code/org boundaries.