Software Engineering is trying to adapt its tools, mechanisms and techniques to cope with the challenges involved when developing BIG DATA software systems. In particular, formal verification in one of the areas that more urgently is required to step in. In this work we introduce two crucial aspects to consolidate the FVS tool to tackle this issue. For one side, FVS’s parallel algorithm is proved to be sound and correct. For the other side, we developed a compelling empirical validation of our approach, employing a communication protocol relevant in the industrial world within a context of parallel systems, introducing a load-balancer process and comparing several implementations.La Ingeniería de Software viene adaptando sus herramientas, métodos y técnicas para enfrentar los desafíos de los denominados sistemas de BIG-DATA. En particular, el área de verificación formal ha sido señalada como unas de las áreas de las que se requiere inmediatas contribuciones. En este trabajo se presentan aspectos claves para consolidar al lenguaje FVS como un lenguaje de verificación formal para BIG DATA. Por un lado se presenta una demostración formal de la correctitud del esquema paralelo de FVS. Por otro, se presenta una desafiante validación empírica del enfoque propuesto utilizando un protocolo relevante a nivel industrial con un balanceador de carga y comparando varias implementaciones.