Formal reasoning on model transformation languages allows users to certify model transformations against transformation contracts. The CoqTL language includes a specification of a transformation engine in the Coq interactive theorem prover. An executable engine can be automatically extracted from this specification. Transformation contracts are proved by the user against the CoqTL specification and guaranteed to hold on the transformation running on the extracted implementation of CoqTL. The design of the transformation engine specification in CoqTL aims at simplifying the certification step, but this requirement harms the execution performance of the extracted engine. In this paper, we aim at providing a scalable distributed implementation of the CoqTL specification. To achieve this objective we proceed in two steps. First, we introduce a refined specification of CoqTL that increases the engine parallelization. We present a mechanized proof of the equivalence with standard CoqTL. Second, we develop a prototype implementation of the refined specification, on top of Spark, a modern data-analytics distributed framework. Finally, by evaluating the performance of a simple case study, we assess the speedup our solution can reach.