En este articulo se presentan dos de las principales técnicas para especificación y verificación de sistemas distribuidos, como son las Técnicas de Descripción Formales (TDFs) y los lenguajes lógicos concurrentes (LLCs).Para cada una de estas técnicas se presentan los elementos con que se modelan sistemas distribuidos y la metodología asociada para llevar a cabo una especificación de un sistema distribuido y la verificación de sus propiedades. Como aporte principal, este articulo realiza un análisis comparativo de las dos técnicas presentadas, mostrando sus ventajas y desventajas relativas a los aspectos de especificación y verificación de sistemas distribuidos.