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.

EDIT: The parent cited http://www.cis.upenn.edu/~bcpierce/papers/unisonspec.pdf by Pierce in 2004, where the authors stressed the difficulty of writing a specification for a file synchronizer, in this case Unison.

Property based testing really is getting some great results.

Abstract:

    > 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.