Experiments in verification with Prusti

[adizere]

Ref: #1694 and the discussion therein.

[seanchen1991]

This seems like really interesting work. I am a bit curious whether there is overlap between using prusti to verify ibc-rs vs. the MBT and integration test work that is currently being done. Do they complement one another or does one obviate the other?

I don't actually expect anyone to have answers to this, just noting some preliminary thoughts down here 🙂

[adizere]

This seems like really interesting work. I am a bit curious whether there is overlap between using prusti to verify ibc-rs vs. the MBT and integration test work that is currently being done. Do they complement one another or does one obviate the other?

I would expect the two approaches to complement each other. In my current understanding:

• Prusti can help with verification of methods via local invariants. It looks to me like the approach (Verification with Prusti #1694) relies on pre- and post-condition specification of program variables;
• I'd expect MBT and integration tests complement this by being able to reason about the behavior of an execution of the whole system (instead of single methods), beyond the relayer, so it would be able to look whether the execution of certain relayer operations resulted in the intended I/O side-effects (e.g., balances increasing, retrying, timeouts).