Three case studies in useful interaction between smart contracts, with a smart contract as a service provider and another as as user of it. A user expects some behaviou out of the service, while the service promises some behaviour. We use these case studies to show how verification can be used to give guarantees to the user about the service's behaviour both statically and at runtime.
See 21-25 in main.pdf for description of the case studies and the properties verified.