Specification and verification of a simplified cloud synchronization protocol. Arbitrary many PCs can connect to a central cloud, fetch the value from the cloud, compare it with their own value, and update the cloud or their own value depending on which is larger. A detailed explanation can be found in a (part of) a presentation I gave during a work meeting: cloudsync.pdf.
The CafeOBJ specification and proof score are both available in cloudsync.cafe.
An independent implementation and verification of this protocol has been done in Constructor-based Inductive Theorem Prover (CITP) by Daniel Gaina.