[aurelius]

If you have used a model checker, you probably don't have a proof either. You have a model that might not be accurate, and testing all its inputs may be combinatorially prohibitive.

[sseveran]

thats not the real issue. The issue with model checkers is verifying that production code actually exactly implements the model.

[aurelius]

Yes, that is <i>another</i> issue with model checkers. Either way, your original comment is still nonsense.

[sseveran]

No. No it is not. See the Amazon paper if you want an overview.