The gist is, you give the synthesizer a C++ implementation of a regular plain-old data structure along with a few annotations, and the synthesizer will synthesize a CRDT implementation of that data structure automatically that is provably-correct. The input needs to be in C++ using only a few types like int, set, etc, because the synthesizer's analysis is implemented against LLVM IR.
The driving example is taking a trivial implementation of a set, and getting back different CRDT implementation of sets depending on the annotations that guide the synthesis.
So, who is this for? A productionized version could be used by feature programmers who want to build new collaborative features. They can "just" write the feature for a single machine, and have the synthesis make it collaborative.