We present a novel approach aimed at synthesizing synchronized process designs from lightweight formal specifications. Our approach takes as input a collection of process specifications expressed in terms of pre/post-conditions, together with a global constraint, expressed in linear-time temporal logic, to be fulfilled by the interaction of these processes. Our approach uses the Alloy Analyzer to enumerate potential implementations of the specified components, up to a given bound, the NuSMV model checker to verify whether their concurrent composition satisfies the global property, and produces executable implementations for the processes–in the style of the Promela language. Due to the exponential number of candidate implementations, our approach implements a two steps process to efficiently prune the solution space. During the exploration phase, our approach first collects a batch of counterexamples that are later used during the exploitation phase, to speed up the search. Our approach is sound and, for an adequate size of counterexamples’ batches, is also complete. We present a prototype implementation of this approach, together with a set of experiments, and compare our technique against related approaches.