La liquidación financiera transfronteriza sigue siendo lenta y costosa, con costes medios de remesa en torno al 6% del importe enviado y solo un tercio de los pagos minoristas internacionales liquidándose en menos de una hora. Keeta es una red blockchain de reciente lanzamiento, diseñada para pagos globales de alto volumen, que incorpora un algoritmo de consenso bifásico dirigido por el cliente. Hasta ahora, el protocolo solo se había descrito de forma informal en un whitepaper, sin un análisis formal que avalara sus propiedades de seguridad. Este artículo presenta la primera especificación formal del algoritmo, escrita en Quint y verificada con TLC bajo un modelo de faltas bizantinas. La investigación demuestra que el protocolo preserva el acuerdo (safety) con un conjunto fijo de representatives con el mismo peso, argumenta que esa garantía se generaliza a cualquier número de representatives e identifica condiciones bajo las cuales una cuenta en disputa puede quedar bloqueada de forma permanente. La verificación cubre únicamente la fase con peso igual; la cuestión de si el acuerdo se mantiene con la votación real de Keeta, ponderada por stake, queda abierta. El modelo generado es comprobable por máquina y queda publicado como artefacto reutilizable para investigaciones futuras. El trabajo se estructura en siete secciones que cubren introducción, contexto sobre verificación formal y verificación de modelos, descripción del protocolo Keeta, el modelo formal, la verificación de seguridad, el análisis de bloqueos y escalabilidad, la discusión y las líneas de trabajo futuro. La principal fuente es el whitepaper de Keeta, complementada con ingeniería inversa del bundle compilado del cliente y consultas directas a los diseñadores del protocolo para resolver ambigüedades restantes.
Noticias agregadas con IA