Sui Prover se vuelve de código abierto: por qué la verificación formal es el eslabón perdido en la seguridad de los contratos inteligentes
En 2025, el sector DeFi perdió 3,3 mil millones de dólares debido a exploits en contratos inteligentes, a pesar de que la mayoría de los protocolos atacados habían sido auditados, algunos en múltiples ocasiones. La brecha de Bybit de 1,5 mil millones de dólares en febrero, el exploit de GMX de 42 millones de dólares e innumerables ataques de reentrada demostraron una verdad incómoda: las auditorías de seguridad tradicionales son necesarias pero no suficientes. Cuando la precisión matemática importa, probar casos límite no basta. Es necesario demostrarlos.
Por esta razón, el hecho de que Sui Prover se convierta en código abierto importa mucho más que cualquier otro lanzamiento en GitHub. Desarrollado por Asymptotic y ahora disponible de forma gratuita para la comunidad de desarrolladores de Sui, Sui Prover lleva la verificación formal —la misma técnica matemática que garantiza que los sistemas de control de vuelo y los diseños de procesadores no fallen— al desarrollo cotidiano de contratos inteligentes. En un panorama donde un solo caso límite ignorado puede drenar cientos de millones, la capacidad de demostrar matemáticamente que el código se comporta correctamente no es un lujo. Se está convirtiendo en una necesidad.
La paradoja de la auditoría: cuando lo "seguro" no es lo suficientemente seguro
El panorama de la seguridad blockchain en 2025 expuso un patrón preocupante. Según el informe de los 100 principales hackeos DeFi de Halborn, los protocolos que habían superado rigurosas auditorías aún fueron víctimas de exploits. Las razones variaron: vulnerabilidades en la cadena de suministro, fallos en el control de acceso, sutiles errores matemáticos en los modelos económicos. Pero el hilo conductor fue que el análisis de código tradicional —ya fuera revisión manual o escaneo automatizado— no pudo detectar todos los posibles modos de fallo.
Consideremos el error yETH de Yearn y los exploits por errores de redondeo de Balancer. No fueron errores de aficionados. Fueron sutiles fallos matemáticos que utilizaron la precisión de redondeo como arma a través de miles de rutas de ejecución potenciales. Un auditor podría pasar semanas revisando el código y aún así pasar por alto la única combinación de entradas que desencadena un comportamiento catastrófico.
El exploit de GMX ilustró otra dimensión del problema. La vulnerabilidad no existía en la lógica central de trading; surgió en los límites entre componentes, donde los oráculos se encontraban con los cálculos de margen y la lógica de liquidación interactuaba con la infraestructura del puente. Probar componentes individuales no fue suficiente cuando el fallo surgió de su interacción.
Aquí es donde la verificación formal difiere fundamentalmente de los enfoques de seguridad tradicionales. En lugar de verificar casos de prueba específicos, la verificación formal demuestra matemáticamente que ciertas propiedades se mantienen en todas las entradas y rutas de ejecución posibles. Si puedes demostrar que una bóveda no puede ser drenada bajo ninguna circunstancia, no necesitas preocuparte por el oscuro caso límite que tus pruebas pasaron por alto.
Qué hace realmente la verificación formal
La verificación formal transforma el código en enunciados matemáticos y luego demuestra que estos enunciados coinciden con una especificación formal del comportamiento previsto. El proceso funciona de la siguiente manera:
Primero, los desarrolladores escriben especificaciones que describen lo que su código debería hacer —no en un lenguaje de programación, sino en un lenguaje de especificación especializado diseñado para expresar propiedades matemáticas. Para los contratos inteligentes, estas especificaciones podrían incluir enunciados como "el suministro total de tokens nunca cambia a menos que se llame a mint o burn" o "los saldos de los usuarios solo pueden disminuir con la autorización explita del usuario".
Luego, una herramienta de prueba (prover) —en este caso, Sui Prover, basado en el motor de verificación Boogie y el solucionador SMT Z3— comprueba exhaustivamente si el código cumple con estas especificaciones en todas las entradas posibles. A diferencia de las pruebas tradicionales, que verifican valores específicos, el prover evalúa todas las entradas posibles simultáneamente a través del razonamiento matemático.
Cuando la verificación tiene éxito, se tiene una prueba matemática de que se cumplen las propiedades especificadas. Cuando falla, el prover suele proporcionar un contraejemplo —una entrada específica que violaría la especificación, lo que a menudo revela errores que las pruebas habrían pasado por alto.
El lenguaje de programación Move, utilizado tanto por Sui como por Aptos, fue diseñado con la verificación formal en mente desde el principio. Su modelo orientado a recursos y su fuerte tipado estático proporcionan una base que hace que la verificación formal sea más práctica que en lenguajes como Solidity. El Lenguaje de Especificación de Move (MSL) permite a los desarrolladores expresar tres categorías de propiedades:
- Invariantes de estructura (Struct Invariants): qué estado debe mantener una estructura a lo largo de su vida útil.
- Especificaciones de función: precondiciones, postcondiciones y garantías de comportamiento para cada función.
- Especificaciones de estado global: propiedades de todo el sistema que deben mantenerse en todas las transiciones de estado.
Sui Prover: de herramienta interna a recurso comunitario
Asymptotic desarrolló inicialmente Sui Prover para respaldar su trabajo de auditoría en los protocolos construidos sobre Sui. Como único proveedor de verificación formal en Sui, necesitaban herramientas que pudieran ir más allá de la revisión manual para verificar matemáticamente las áreas de alto riesgo de las bases de código de los clientes.
La decisión de liberar la herramienta como código abierto refleja tanto la madurez de la tecnología de verificación formal como el reconocimiento de que la seguridad es un bien público. Cuando más desarrolladores pueden acceder a la verificación formal, todo el ecosistema se vuelve más seguro —lo que beneficia a todos, incluidos los auditores de seguridad que pueden centrarse en preocupaciones de mayor nivel.
Sui Prover está disponible en GitHub y se puede instalar a través de Homebrew (brew install asymptotic-code/sui-prover/sui-prover). El desarrollo activo continúa, con problemas recientes abiertos en enero de 2026 que abordan mejoras continuas.
Lo que hace que Sui Prover sea particularmente valioso es su integración con el flujo de trabajo de desarrollo existente de Sui Move. Los desarrolladores pueden añadir especificaciones a su código existente de forma incremental, verificando primero las funciones críticas mientras expanden gradualmente la cobertura. Las especificaciones cumplen una doble función como controles de seguridad y documentación —cualquiera que revise o integre el contrato puede leer las especificaciones para comprender los comportamientos garantizados.
Propiedades del mundo real que se pueden demostrar
El poder de la verificación formal se vuelve concreto cuando se consideran propiedades específicas que pueden demostrarse:
Bóvedas no drenables: Para los protocolos DeFi que custodian fondos de usuarios, demostrar que ninguna secuencia de operaciones puede drenar la bóveda sin la autorización adecuada elimina categorías enteras de ataques. Esto no es un "hemos probado muchos vectores de ataque"; es la certeza matemática de que el drenaje es imposible.
Precios de participación no decrecientes: Las bóvedas de rendimiento y los pools de liquidez a menudo necesitan garantizar que los precios de las participaciones nunca disminuyan inesperadamente (fuera del deslizamiento esperado). La verificación formal puede demostrar que esta propiedad se mantiene independientemente de las condiciones del mercado o de las acciones del usuario.
Preservación exacta del saldo: Los contratos de tokens pueden demostrar que el suministro total permanece constante en todas las operaciones, que las transferencias mueven exactamente la cantidad especificada y que no se crean ni destruyen tokens excepto a través de funciones designadas.
Garantías de control de acceso: Demostrar que solo las direcciones autorizadas pueden llamar a funciones privilegiadas, independientemente del estado del contrato o de la secuencia de operaciones previas.
Invariantes económicos: Los protocolos DeFi complejos pueden demostrar propiedades sobre sus modelos económicos: que se respetan las restricciones de liquidez, que se mantienen los coeficientes de colateralización y que los bucles de arbitraje no pueden extraer un valor ilimitado.
Estos no son ejemplos teóricos. Los desarrolladores en el ecosistema Sui ya han aplicado especificaciones formales para verificar contratos DeFi, incluidos AMM y sistemas de agricultura de rendimiento apalancada (leveraged yield farming). Cuando estas propiedades se demuestran en lugar de asumirse, la postura de seguridad cambia fundamentalmente.
El panorama de la seguridad exige mejores herramientas
Las estadísticas de 2025 hacen que el caso de la verificación formal sea convincente. Según investigadores de seguridad, los incidentes fuera de la cadena (off-chain) representaron el 56.5 % de los ataques y el 80.5 % de los fondos perdidos en 2024, pero las vulnerabilidades de los contratos inteligentes siguen siendo devastadoras cuando se explotan. Las vulnerabilidades de control de acceso por sí solas causaron $ 953.2 millones en daños documentados a lo largo de 2024.
El Top 10 de Contratos Inteligentes de OWASP para 2025 documentó más de $ 1.42 mil millones en pérdidas colectivas en los ecosistemas descentralizados. Las herramientas de seguridad tradicionales — Mythril para ejecución simbólica, Echidna para fuzzing basado en propiedades, auditorías manuales de firmas como OtterSec, Halborn y MoveBit — abordan diferentes aspectos del problema. Pero a medida que los protocolos se vuelven más complejos y manejan más valor, las brechas entre estos enfoques se vuelven más peligrosas.
CertiK ha desplegado técnicas de verificación formal para verificar matemáticamente contratos inteligentes, protegiendo más de $ 300 mil millones en activos según sus informes. Esta escala demuestra tanto la demanda de garantías de seguridad matemáticas como la viabilidad de aplicar métodos formales a los sistemas blockchain.
El consenso emergente entre los investigadores de seguridad es que las auditorías, los programas de recompensas por errores (bug bounties), el monitoreo, los lanzamientos graduales y los métodos formales deben trabajar juntos como capas de defensa. Para sistemas de alto valor, la verificación formal de invariantes críticos se está convirtiendo en una práctica estándar en lugar de un rigor excepcional.
Por qué Move hace que la verificación formal sea práctica
No todos los lenguajes de programación son igualmente susceptibles a la verificación formal. La flexibilidad de Solidity y la complejidad de la EVM hacen que la verificación formal sea un desafío: es posible, pero requiere una sobrecarga significativa de herramientas y experiencia.
Move fue diseñado de manera diferente. Su modelo orientado a recursos significa que los activos tienen tipos lineales que no se pueden duplicar ni descartar implícitamente. El sistema de tipos detecta categorías enteras de errores en el tiempo de compilación que requerirían comprobaciones en tiempo de ejecución en otros lenguajes. El Move Prover se desarrolló junto con el lenguaje, lo que garantiza una integración estrecha entre las características del lenguaje y las capacidades de verificación.
Esta herencia de diseño significa que las propias bibliotecas estándar de Move fueron verificadas formalmente. Cuando construyes sobre Sui o Aptos, lo haces sobre una base que cuenta con pruebas matemáticas de corrección; pruebas que se acumulan a medida que superpones tu propio código verificado.
La implicación práctica: la verificación formal en Move requiere menos experiencia especializada que en otras plataformas. La documentación de Sui Prover, los ejemplos y la integración con los flujos de trabajo de desarrollo estándar lo hacen accesible para desarrolladores que no son especialistas en métodos formales. Puedes aprender a escribir especificaciones de forma incremental, comenzando con contratos de funciones simples y progresando hacia invariantes complejos a medida que profundizas tus conocimientos.
Qué significa esto para los desarrolladores de Sui
Para los desarrolladores que construyen sobre Sui, el Sui Prover de código abierto crea nuevas posibilidades:
Diferenciación de seguridad: En un panorama DeFi competitivo, demostrar las propiedades de seguridad no es solo mitigación de riesgos; es una ventaja competitiva. Los usuarios y auditores pueden verificar las afirmaciones sobre la seguridad del protocolo en lugar de confiar en aserciones.
Costos de auditoría reducidos: Cuando las funciones críticas tienen pruebas formales, los auditores pueden centrarse en preocupaciones de nivel superior en lugar de probar exhaustivamente casos extremos. Esto puede reducir el alcance y el costo de la auditoría, al tiempo que mejora los resultados de seguridad.
Calidad de la documentación: Las especificaciones formales son documentación precisa que no puede quedar obsoleta. Cuando la especificación dice que una función preserva cierto invariante, eso es demostrablemente cierto o el verificador señalará una violación.
Adopción incremental: No es necesario verificar formalmente todo. Comienza con las funciones de mayor riesgo — aquellas que manejan retiros, colaterales u operaciones privilegiadas — y expande la cobertura con el tiempo.
El ecosistema Sui ya alberga múltiples firmas de auditoría experimentadas, incluidas MoveBit (pioneros en la verificación formal de Move), Certora, OtterSec y Zellic. El Sui Prover añade una herramienta que los desarrolladores pueden usar directamente, sin necesidad de contratar auditores externos para cada tarea de verificación.
La trayectoria más amplia
El lanzamiento de código abierto de Sui Prover se ajusta a un patrón más amplio de maduración de las herramientas de seguridad en toda la industria de blockchain. La verificación formal está pasando de la investigación académica a la infraestructura de producción, de consultorías especializadas a herramientas accesibles para los desarrolladores.
Esta trayectoria es importante porque la escala del valor asegurado por los contratos inteligentes sigue creciendo. Los protocolos DeFi gestionan colectivamente cientos de miles de millones en activos. Un solo error en un protocolo importante puede causar pérdidas que superan lo que las empresas de software tradicionales enfrentan en toda su existencia.
La industria del software tradicional terminó adoptando métodos formales para sistemas de seguridad crítica: aviónica, dispositivos médicos, sistemas financieros. La industria de blockchain, donde "el código es ley" y los errores suelen ser irreversibles, tiene razones aún más poderosas para adoptar la verificación matemática.
El Sui Prover representa un paso en esta dirección: hacer que la verificación formal sea lo suficientemente accesible para que los desarrolladores realmente la utilicen, en lugar de relegarla a documentación de "teatro de seguridad" que nadie lee.
Cómo empezar
Para los desarrolladores interesados en explorar la verificación formal en Sui:
- Instale el Sui Prover:
brew install asymptotic-code/sui-prover/sui-prover - Empiece poco a poco: Añada especificaciones a una sola función crítica y verifique que se cumplan.
- Aprenda el lenguaje de especificación: El Lenguaje de Especificación de Move (Move Specification Language) cuenta con una excelente documentación para expresar propiedades comunes.
- Itere: Amplíe la cobertura a más funciones e invariantes más complejos a medida que gane confianza.
La inversión en aprender la especificación formal paga dividendos compuestos. Una vez que haya verificado que los módulos de nivel inferior son correctos, puede construir lógica de nivel superior sabiendo que esos cimientos están probados matemáticamente.
Para una industria que perdió miles de millones por errores evitables en 2025, la pregunta no es si la verificación formal vale la pena. La pregunta es qué tan rápido puede adoptarla el ecosistema. El lanzamiento de código abierto de Sui Prover elimina una barrera; ahora el conocimiento y la práctica deben seguir su ejemplo.
Construir aplicaciones seguras en Sui requiere una infraestructura confiable que coincida con los estándares de seguridad de su protocolo. BlockEden.xyz ofrece endpoints RPC de nivel empresarial para Sui, Aptos y más de 20 cadenas con el tiempo de actividad y la confiabilidad que exigen las aplicaciones de producción. Explore nuestro marketplace de APIs para potenciar sus contratos inteligentes verificados formalmente.