Los sistemas geográficamente distribuidos replican su estado sobre diferentes nodos (llamados también réplicas) con el fin de satisfacer requerimientos no-funcionales como la alta disponibilidad. Sin embargo, dado que la comunicación entre réplicas es asincrónica, los usuarios de estos sistemas pueden, temporalmente, observar discrepancias en la información debido a que acceden a distintas replicas. Por lo tanto, razonar sobre la correctitud de sistemas geo-replicados se convierte en una tarea difícil. Es así como hoy en día existe la necesidad de contar con herramientas que nos permitan especificar, modelar y analizar sistemas geo-replicados. Los tipos de datos replicados han sido propuestos a tal fin. Los tipos de datos replicados son análogos a los tipos de datos abstractos, pero sus operaciones tienen en cuenta los distintos niveles de consistencia, es decir, las anomalías o inconsistencias que el sistema puede aceptar hasta que las réplicas converjan a el mismo estado.

En esta tesis abordamos el problema de probar invariantes de datos sobre tipos de datos replicados. Como modelo formal de computación de sistemas geo-replicados adoptamos Quelea, un modelo formal de consistencia mixta, es decir, que permite combinar operaciones con diferentes niveles de consistencia. Si bien Quelea está equipado con un lenguaje de contratos que permite razonar sobre la consistencia de las operaciones, no provee herramientas que permitan escribir y probar invariantes de datos a nivel aplicación. Concretamente, proponemos una técnica para probar invariantes de datos sobre el framework Quelea. Para ello, proponemos una semántica operacional alternativa que garantiza una propiedad de consistencia conocida como visibilidad causal. Luego, presentamos un conjunto de proof-rules que permiten verificar invariantes de datos y finalmente ilustramos como estas proof-rules pueden implementarse en F*, un lenguaje de programación que descarga pruebas sobre un SMT solver.