Keeta: primer análisis formal de su consenso de dos fases revela riesgo de bloqueo permanente

Modeling and Verification of Keeta's Consensus [pdf]

Keeta, la red blockchain para pagos globales de alto volumen, usa un algoritmo de consenso de dos fases dirigido por el cliente que solo se había descrito informalmente. Este artículo presenta la primera especificación formal del algoritmo, escrita en Quint y verificada con TLC bajo un modelo de fallos bizantinos. El modelo demuestra que el protocolo preserva el acuerdo con un conjunto fijo de representantes de igual peso, pero también muestra condiciones bajo las cuales una cuenta en disputa puede quedar bloqueada permanentemente. La seguridad con votación ponderada por participación queda como pregunta abierta.