To give more context, B. Pierce, one of the authors of the Dropbox paper is (one of?) the main author of Unison, and also coauthor of the paper you linked.
> Abstract—File synchronization services such as Dropbox are used by
> hundreds of millions of people to replicate vital data. Yet formal
> models of their behavior are lacking. We present the first
> formal—and testable—model of the core behavior of a modern file
> synchronizer, and we use it to discover surprising behavior in two
> widely deployed synchronizers. Our model is based on a technique for
> testing nondeterministic systems that avoids requiring that the
> system’s internal choices be made visible to the testing framework.
