Muchos servicios en la nube dependen de almacenes de clave-valor distribuidos como ZooKeeper, Cassandra, HBase, etc. Sin embargo, los almacenes de clave-valor distribuidos son conocidos por ser difíciles de diseñar e implementar sin cometer errores. Las violaciones de consistencia pueden confundir a las aplicaciones de cliente al mostrar valores inválidos, lo que puede resultar en consecuencias graves como pérdida de datos, corrupción de datos y comportamientos inesperados de las aplicaciones de cliente. Los errores de software son una de las principales razones por las que pueden ocurrir violaciones de consistencia. Las técnicas de verificación formal pueden utilizarse para garantizar que los diseños sean correctos y minimizar los riesgos de errores en la implementación. Sin embargo, la verificación formal no es una panacea debido a limitaciones como el costo de la verificación, la incapacidad para verificar implementaciones existentes y los errores humanos involucrados. La verificación del modelo a nivel de implementación ha sido ampliamente explorada por investigadores en las últimas décadas para verificar formalmente si la implementación subyacente de sistemas distribuidos tiene errores o no. No obstante, propuestas anteriores son limitadas porque su verificación de invariantes no es lo suficientemente versátil como para verificar el amplio espectro de modelos de consistencia, desde la consistencia eventual hasta la consistencia fuerte. En este trabajo, se emplean oráculos de consistencia para la verificación de invariantes de consistencia que pueden ser utilizados por verificadores de modelos a nivel de implementación para verificar formalmente las implementaciones de modelos de consistencia de datos de almacenes de clave-valor distribuidos. Para integrar los oráculos de consistencia con los verificadores de modelos de sistemas distribuidos a nivel de implementación, se aprovecha la información de orden parcial obtenida a través de la API para evitar la búsqueda exhaustiva durante la verificación de invariantes de consistencia. Nuestros resultados de evaluación muestran que, al utilizar el método propuesto para la verificación de invariantes de consistencia, nuestro verificador de modelos prototipo, VConMC, puede detectar violaciones de consistencia causadas por varios errores de software del mundo real en un conocido almacén de clave-valor distribuido, ZooKeeper.