Título: Verificación Automática de Smart Contracts Move en Sui
Director: Diego Garbervetsky
Jurados: Juan Pablo Galeotti, Javier Godoy

Resumen
En el ecosistema de las blockchains, la verificación formal de contratos inteligentes es fundamental para garantizar su seguridad y confiabilidad, evitando vulnerabilidades que podrían resultar en pérdidas económicas o fallas de funcionamiento. Sui, una blockchain que utiliza el lenguaje Move, presenta un enfoque innovador para la gestión de objetos y transacciones, pero aún cuenta con un ecosistema de herramientas de verificación en desarrollo.
Este trabajo tiene como objetivo explorar métodos para la verificación automática de contratos en Sui. Se realiza un estudio del estado actual de la verificación en Move, evaluando la herramienta Move Prover en su capacidad para comprobar propiedades de seguridad en módulos escritos para Sui. Además, se propone un flujo de trabajo alternativo que traduce código Move a Rust de manera controlada, con el fin de habilitar el uso del verificador Kani, herramienta enfocada en análisis exhaustivo de propiedades y detección de errores en tiempo de compilación.
Los resultados muestran que Move Prover no es capaz de interpretar el modelo actual de objetos de Move, mientras que la traducción a Rust permitió aprovechar verificadores externos con mucha mejor capacidad de verificación, aunque requirió ajustes manuales y simplificaciones del código para poder representar el funcionamiento de Move en Rust.