We have worked on the development of techniques for the verification of APIs of data implemented on top of eventual consistent data stores. In particular, we addressed the verification of invariants preserved by data when implemented on a replicated data store offering a particular consistency guarantee: for this goal, we worked on the development of a sound proof technique that can reuse tools previously developed at NOVA (CISE, IPA). The final goal is to ensure that an API is “robust” with respect to a given consistency model, i.e., to ensure that the observable behaviour of an API remains the same even if the consistency level of the store is relaxed/strengthen. This secondment was related to Task T.4.3-  (O.4.2 & O.4.3).