Is there something like high performance model checking using Alloy, something like assigning multiple cores to Alloy engine? Do you know any even experimental academic or industrial works that try to do this?

Alloy uses plugable solvers, see the menu. Some of these solvers use the parallelism available on a platform.

Adding to Peter’s answer (e.g. the PLingeling solver), notice that Alloy (thanks to @nmacedo and @alcino) 6 is equipped with a “Decompose strategy” entry in the options menu. The strategy consists in choosing, or not, to consider a verification problem featuring static sigs and fields as one big *amagalmated* problem (encompassing all possible instantiations for static sigs and fields) or as as many as possible *smaller* subproblems (where each subproblem corresponds to one *pre-computed* valuation of static sigs and fields, what we call a *configuration*).

- In the latter case, subproblems can be solved in parallel. In practice, the fully decomposed strategy can be very efficient for SAT problems as the said problems can be quite smaller than the amagalmated one.
- Conversely, for UNSAT problems, the amagalmated approach can be more relevant as the decomposed one may yield so many UNSAT subproblems that it may well be faster to just check one big problem.
- As a middle ground, you have the “hybrid” strategy which performs the decomposition but also keeps one core for the amagalmated problem