De 'El código es ley' a 'La especificación es ley': Cómo la verificación formal podría acabar con la crisis de exploits de 3.4 mil millones de dólares en DeFi
Un solo error de redondeo — una pérdida de precisión de menos de un centavo en la división de enteros de Solidity — drenó $ 128 millones de Balancer en nueve cadenas de bloques en menos de 30 minutos. Los pools habían estado activos durante años. Múltiples auditorías habían revisado el código. Nadie lo detectó. Este es el estado de la seguridad de DeFi en 2026: miles de millones de dólares protegidos por un paradigma que ha fallado demostrable y repetidamente.
Ahora, a16z crypto está proponiendo un replanteamiento radical. En su informe "Big Ideas" de 2026, la firma de capital de riesgo argumenta que la industria debe abandonar "el código es ley" — la creencia fundacional de que el código del contrato inteligente desplegado es la autoridad última — y reemplazarlo por "la especificación es ley", donde las propiedades de seguridad definidas matemáticamente se conviertan en el estándar exigible. El cambio podría remodelar fundamentalmente cómo se construyen, auditan y defienden los protocolos.
El problema de $ 3,4 mil millones que las auditorías no pueden resolver
Las cifras cuentan una historia condenatoria. Solo en 2025, la industria de las criptomonedas perdió más de 1,5 mil millones de ese total. Los errores en contratos inteligentes causaron aproximadamente 10,77 mil millones de los protocolos.
El modelo de seguridad tradicional — escribir código, contratar auditores, desplegar y esperar — ha tocado techo. Incluso los protocolos bien financiados con múltiples auditorías de firmas de primer nivel siguen siendo vulnerables. El exploit de Balancer demostró esto sin lugar a dudas: una vulnerabilidad oculta a plena vista durante años, pasada por alto por revisiones de seguridad profesionales y explotada en minutos una vez descubierta.
Más preocupante es la sofisticación evolutiva de los ataques. Los exploits de préstamos flash (flash loans) aumentaron en 2024, representando el 83,3 % de los exploits elegibles. La mayoría de los grandes hackeos de 2025 combinaron de dos a cuatro tipos de vulnerabilidades simultáneamente. Solo los hackers norcoreanos robaron $ 2,02 mil millones en 2025, un aumento del 51 % interanual. Los atacantes se están volviendo más inteligentes más rápido que los defensores.
Anatomía de un error de redondeo de $ 128 millones
El exploit de Balancer merece un examen detallado porque ilustra perfectamente por qué falla "el código es ley". El 3 de noviembre de 2025, un atacante explotó una vulnerabilidad matemática en cómo los ComposableStablePools de Balancer manejan swaps de bajo valor.
Esto es lo que sucedió: cuando los balances de los tokens se llevan a un rango específico (8-9 wei), la división de enteros de Solidity provoca una pérdida de precisión significativa. La función _upscaleArray redondea hacia abajo durante el escalado, lo que hace que el invariante del pool — la constante matemática que debería regir los tipos de cambio justos — sea subestimado. Esto suprime artificialmente los precios de BPT (Balancer Pool Token).
El atacante convirtió esto en un arma ejecutando una secuencia de swap de tres etapas dentro de una sola transacción batchSwap que contenía más de 65 operaciones:
- Supresión de precios: Intercambiar grandes cantidades de BPT por tokens subyacentes, empujando el balance de un token al umbral crítico de 8-9 wei donde los errores de redondeo se maximizan.
- Adquisición barata: Mintear o comprar BPT al precio suprimido artificialmente.
- Redención total: Redimir inmediatamente BPT por activos subyacentes a su valor total.
Todo el ataque se ejecutó dentro del constructor de un contrato inteligente desplegado — una sola transacción que drenó 19 millones, pero la gran mayoría se perdió.
La lección crítica: esta no fue una vulnerabilidad exótica. Fue una violación del invariante matemático — el tipo de error que una especificación formal habría detectado por definición.
Qué significa realmente "la especificación es ley"
La propuesta de a16z opera en dos niveles: estático (antes del despliegue) y dinámico (después del despliegue).
En el lado estático, la seguridad de DeFi debe pasar de verificar propiedades locales seleccionadas a mano a probar sistemáticamente invariantes globales. En lugar de preguntar "¿esta función maneja correctamente los casos de borde?", la pregunta pasa a ser "¿mantiene todo este sistema sus propiedades matemáticas centrales bajo todas las entradas y estados posibles?".
Aquí es donde entran las herramientas de verificación formal como Certora Prover y K Framework de Runtime Verification. Estas herramientas comparan el bytecode del contrato inteligente con reglas matemáticas que definen el comportamiento esperado, verificando cada estado de contrato y ruta de ejecución posible. Certora Prover, por ejemplo, utiliza especificaciones escritas en CVL (Certora Verification Language) para detectar violaciones de propiedades mediante análisis estático y resolución de restricciones.
En el lado dinámico, esos mismos invariantes se convierten en barreras de protección activas — aserciones en tiempo de ejecución que cada transacción debe satisfacer. Si una transacción violara una propiedad de seguridad central, se revierte automáticamente. Este es el concepto de "última línea de defensa": incluso un ataque novedoso y nunca antes visto debe seguir satisfaciendo las propiedades de seguridad fundamentales del sistema.
La elegancia de este enfoque es su asimetría. Los atacantes deben encontrar violaciones; los defensores solo necesitan definir cómo se ve lo "correcto". Como dice a16z: "Incluso un ataque novedoso debe satisfacer las mismas propiedades de seguridad que mantienen el sistema intacto, por lo que los únicos ataques que quedan son minúsculos o extremadamente difíciles de ejecutar".
Quién está construyendo ya de esta manera
La visión de "la especificación es la ley" no es puramente teórica. Varios protocolos importantes han comenzado a adoptar la verificación formal como una parte central de su proceso de desarrollo.
Aave, el protocolo de préstamos más grande por TVL, ha integrado Certora Prover directamente en su pipeline de integración continua. Cada cambio de código se verifica automáticamente contra las especificaciones formales antes de que pueda fusionarse. Esto no es una auditoría ocasional — es una prueba matemática que se ejecuta en cada commit.
Uniswap V2 se sometió a una verificación formal de su modelo central de creador de mercado "x * y = k" utilizando el K Framework de Runtime Verification. La verificación cubrió la formalización del modelo matemático, su implementación en contratos inteligentes y la ejecución simbólica del bytecode compilado para cuatro funciones críticas.
Kamino, un protocolo de préstamos basado en Solana, comenzó a verificar invariantes críticos utilizando Certora Prover a principios de 2025. El XRP Ledger también ha implementado la verificación de invariantes a nivel de protocolo. Estos no son desarrollos exclusivos de Ethereum — el enfoque de "la especificación es la ley" se está extendiendo por todos los ecosistemas de blockchain.
La IA se encuentra con la verificación formal: AI Composer de Certora
Uno de los obstáculos más significativos para la verificación formal ha sido su complejidad. Escribir especificaciones formales requiere una experiencia especializada de la que carecen la mayoría de los equipos de desarrollo. Esto está cambiando.
En diciembre de 2025, Certora lanzó AI Composer — una plataforma de codificación de IA de código abierto que integra la verificación formal directamente en el proceso de generación de código. A diferencia de las herramientas de codificación de IA genéricas que priorizan la velocidad, AI Composer garantiza que cada fragmento de código generado por IA cumpla con las reglas de seguridad matemáticas antes de su ejecución.
La plataforma representa una potencial democratización de la verificación formal. Si la IA puede ayudar a escribir especificaciones, proponer invariantes y reducir los costos de ingeniería de pruebas manuales, entonces "la especificación es la ley" se vuelve accesible más allá de los pocos equipos que actualmente pueden permitirse ingenieros dedicados a la verificación formal.
Esta fusión de IA y verificación también aborda la observación de a16z de que la seguridad actual de DeFi debería "probar sistemáticamente los invariantes globales en lugar de verificar los locales seleccionados a mano". La IA puede explorar el espacio de las especificaciones de manera más amplia que los ingenieros humanos, capturando potencialmente los tipos de violaciones matemáticas sutiles — como el error de redondeo de Balancer — que escapan a la revisión manual.
Las implicaciones legales y de gobernanza
"La especificación es la ley" conlleva implicaciones que van más allá del código. Si un protocolo publica especificaciones formales que definen su comportamiento previsto, esas especificaciones podrían convertirse en el estándar legal por el cual se juzga al protocolo.
Bajo un régimen de "el código es la ley", cualquier exploit del código desplegado es técnicamente un "funcionamiento según lo previsto" — el código hizo exactamente lo que fue programado para hacer, incluso si eso no era lo que los desarrolladores pretendían. Bajo "la especificación es la ley", una especificación formal define la intención. Los desarrolladores de protocolos serían responsables de las desviaciones de las especificaciones publicadas, pero no de cada posible vector de exploit que quede fuera de esas especificaciones.
Esto crea un marco de responsabilidad más claro. Si Balancer hubiera publicado una especificación formal declarando que los invariantes del pool deben permanecer dentro de los límites definidos independientemente de la secuencia de transacciones, el exploit del error de redondeo habría sido una violación clara de la especificación — y potencialmente motivo de recursos legales o reclamaciones de seguros.
Desafíos y limitaciones
La tesis de "la especificación es la ley" es convincente pero enfrenta obstáculos reales.
La integridad de la especificación es el desafío fundamental. ¿Cómo se especifica formalmente cada propiedad que importa? Las especificaciones son escritas por humanos, y los humanos pueden pasar por alto propiedades críticas — de la misma manera que los auditores pasan por alto errores críticos. Una especificación que no captura los invariantes correctos proporciona una falsa confianza.
El riesgo de composibilidad añade otra capa. El valor de DeFi proviene de los protocolos que interactúan entre sí. Verificar formalmente los invariantes de un solo protocolo no garantiza la seguridad cuando ese protocolo se compone con otros de maneras inesperadas. La superficie de interacción entre protocolos sigue siendo una frontera en gran medida no especificada.
El rendimiento y el costo son preocupaciones prácticas. La verificación formal es computacionalmente costosa. La verificación de invariantes en tiempo de ejecución añade costos de gas a cada transacción. Para los protocolos de alta frecuencia que procesan miles de transacciones por segundo, estos costos importan.
La inercia de adopción puede ser el mayor obstáculo. La mayoría de los equipos de DeFi lanzan código bajo una intensa presión competitiva. Añadir la verificación formal al pipeline de desarrollo ralentiza el despliegue. Hasta que el mercado recompense a los protocolos verificados con un mayor TVL o primas de seguro más bajas, el incentivo para adoptar sigue siendo débil.
El camino a seguir
A pesar de estos desafíos, la trayectoria es clara. El costo de los exploits — 3.4 mil millones de dólares en 2025, 10.77 mil millones de dólares acumulados — hace que el status quo sea insostenible. Los mercados de seguros, el capital institucional y los marcos regulatorios exigirán cada vez más garantías de seguridad demostrables.
La convergencia de la escritura de especificaciones asistida por IA, las herramientas maduras de verificación formal y la infraestructura de cumplimiento en tiempo de ejecución está reduciendo la barrera de adopción. Cuando Aave puede ejecutar Certora Prover en cada commit y Kamino puede verificar invariantes en Solana, las herramientas han pasado de la investigación académica a la infraestructura de producción.
La evolución de la industria de "el código es la ley" a "la especificación es la ley" refleja un patrón visto en cada disciplina de ingeniería en maduración: desde "lo construimos y parece funcionar" hasta "podemos demostrar matemáticamente que cumple con su especificación". La aviación, la ingeniería nuclear y el diseño de semiconductores pasaron por esta transición. DeFi, con más de 100 mil millones de dólares en TVL dependiendo de la corrección matemática, lleva tiempo de retraso.
La cuestión no es si "la especificación es la ley" se convertirá en el estándar. Es cuántos miles de millones más se perderán antes de que lo haga.
BlockEden.xyz proporciona infraestructura de API de blockchain de grado empresarial que impulsa aplicaciones DeFi en múltiples cadenas. A medida que la verificación formal se convierte en el estándar de la industria, una infraestructura de nodos confiable forma la base para las interacciones de protocolos verificados. Explore nuestro marketplace de APIs para construir sobre una infraestructura diseñada para la era de la seguridad ante todo.