Una publicación etiquetados con "auditoría IA"

Verificación Formal en la Auditoría de Contratos Inteligentes​

La verificación formal se refiere al uso de técnicas matemáticas y lógicas para probar la corrección y seguridad de los contratos inteligentes. En la práctica, esto abarca un espectro de metodologías: desde pruebas de fuzzing basadas en propiedades y ejecución simbólica, hasta la demostración rigurosa de teoremas y la verificación de modelos. El objetivo es asegurar que un contrato cumpla con sus especificaciones y no contenga errores explotables en todas las posibles entradas y estados. Dado el alto riesgo (miles de millones de dólares están bloqueados en protocolos DeFi), los métodos formales se han vuelto cada vez más importantes para Ethereum y otras plataformas blockchain.

Enfoques Tradicionales: Los primeros métodos formales para Ethereum incluyeron herramientas de ejecución simbólica como Oyente y Mythril, y analizadores estáticos como Slither y Securify. La ejecución simbólica explora las rutas del programa con entradas simbólicas para detectar problemas (por ejemplo, reentrada, desbordamiento de enteros), mientras que el análisis estático utiliza la coincidencia de patrones basada en reglas. Estas herramientas han tenido éxito pero también limitaciones: por ejemplo, Oyente sufría de muchas falsas alarmas incluso en contratos simples, y los detectores basados en patrones de Slither pueden producir varios falsos positivos. Además, un estudio de 2023 encontró que más del 80 % de los errores explotables en contratos (especialmente los complejos errores de “lógica de negocio”) no fueron detectados por las herramientas actuales, lo que subraya la necesidad de técnicas de verificación más robustas.

La Promesa y el Desafío de la Verificación Completa: En teoría, la verificación formal puede probar la ausencia de errores al verificar exhaustivamente los invariantes para todos los estados. Herramientas como el Certora Prover o el marco KEVM de la Fundación Ethereum tienen como objetivo verificar matemáticamente los contratos inteligentes contra una especificación formal. Por ejemplo, el “auditor matemático automatizado” de Certora utiliza un lenguaje de especificación (CVL) para probar o refutar reglas definidas por el usuario. En la práctica, sin embargo, probar completamente las propiedades en contratos del mundo real es a menudo inalcanzable o muy laborioso. Es posible que el código deba reescribirse en formas simplificadas para la verificación, se deben escribir especificaciones personalizadas, los bucles y la aritmética compleja pueden requerir límites o abstracciones manuales, y los solucionadores SMT frecuentemente se agotan en lógica compleja. Como señalaron los ingenieros de Trail of Bits, “probar la ausencia de errores es generalmente inalcanzable” en bases de código no triviales, y lograrlo a menudo requiere una gran intervención y experiencia del usuario. Debido a esto, las herramientas de verificación formal se han utilizado tradicionalmente con moderación para piezas críticas de código (por ejemplo, verificar el invariante de un token o un algoritmo de consenso), en lugar de contratos completos de principio a fin.

Fuzz Testing y Pruebas de Invariantes de Foundry​

En los últimos años, las pruebas basadas en propiedades han surgido como una alternativa práctica a las pruebas formales completas. Foundry, un popular marco de desarrollo de Ethereum, tiene soporte integrado para fuzz testing y pruebas de invariantes, técnicas que mejoran enormemente la cobertura de las pruebas y pueden considerarse una verificación formal ligera. El fuzz testing de Foundry genera automáticamente un gran número de entradas para intentar violar las propiedades especificadas, y las pruebas de invariantes extienden esto a secuencias de operaciones que cambian el estado:

• Fuzz Testing: En lugar de escribir pruebas unitarias para entradas específicas, el desarrollador especifica propiedades o invariantes que deben mantenerse para cualquier entrada. Foundry luego genera cientos o miles de entradas aleatorias para probar la función y verifica que la propiedad siempre se cumpla. Esto ayuda a detectar casos límite que un desarrollador podría no pensar en probar manualmente. Por ejemplo, una prueba de fuzzing podría afirmar que el valor de retorno de una función siempre es no negativo o que una cierta postcondición es verdadera independientemente de las entradas. El motor de Foundry utiliza heurísticas inteligentes —analiza las firmas de las funciones e introduce valores de casos límite (0, uint máximo, etc.)— para encontrar los casos extremos que probablemente rompan la propiedad. Si una aserción falla, Foundry informa una entrada de contraejemplo que viola la propiedad.

• Pruebas de Invariantes: Las pruebas de invariantes de Foundry (también llamadas fuzzing con estado) van más allá al ejecutar múltiples llamadas a funciones y transiciones de estado en secuencia. El desarrollador escribe funciones invariantes que deben mantenerse verdaderas durante toda la vida del contrato (por ejemplo, activos totales = suma de los saldos de los usuarios). Foundry luego genera secuencias aleatorias de llamadas (con entradas aleatorias) para simular muchos escenarios de uso posibles, verificando periódicamente que las condiciones invariantes sigan siendo verdaderas. Esto puede descubrir errores complejos que solo se manifiestan después de una secuencia particular de operaciones. Esencialmente, las pruebas de invariantes exploran el espacio de estados del contrato de manera más exhaustiva, asegurando que ninguna secuencia de transacciones válidas pueda violar las propiedades establecidas.

Por qué Foundry es Importante: Foundry ha hecho accesibles estas técnicas de prueba avanzadas. Las características de fuzzing e invariantes son nativas del flujo de trabajo del desarrollador: no se necesita ningún arnés especial o herramienta externa, y las pruebas se escriben en Solidity junto con las pruebas unitarias. Gracias a un motor basado en Rust, Foundry puede ejecutar miles de pruebas rápidamente (paralelizándolas) y proporcionar trazas de fallos detalladas para cualquier violación de invariantes. Los desarrolladores informan que el fuzzer de Foundry es fácil de usar y de alto rendimiento, requiriendo solo una configuración menor (por ejemplo, establecer el número de iteraciones o agregar suposiciones para restringir las entradas). Un ejemplo simple de la documentación de Foundry es una prueba de fuzzing para una función divide(a,b), que utiliza vm.assume(b != 0) para evitar entradas inválidas triviales y luego afirma postcondiciones matemáticas como result * b <= a. Al ejecutar dicha prueba con miles de pares (a,b) aleatorios, Foundry podría descubrir rápidamente casos límite (como los límites de desbordamiento) que serían difíciles de encontrar mediante el razonamiento manual.

Comparaciones: El enfoque de Foundry se basa en trabajos anteriores de la comunidad. El fuzzer Echidna de Trail of Bits fue una herramienta de pruebas basadas en propiedades anterior para Ethereum. Echidna genera de manera similar transacciones aleatorias para encontrar violaciones de invariantes expresadas como funciones de Solidity que devuelven un booleano. Es conocido por su generación de entradas “inteligente” (incorporando fuzzing guiado por cobertura) y se ha utilizado para encontrar muchos errores. De hecho, los investigadores de seguridad señalan que el motor de Echidna es extremadamente efectivo —“el Echidna de Trail of Bits es el mejor fuzzer que existe debido a su selección inteligente de números aleatorios”— aunque el flujo de trabajo integrado de Foundry hace que escribir pruebas sea más simple para los desarrolladores. En la práctica, el fuzz testing de Foundry a menudo se considera el nuevo “mínimo indispensable” para el desarrollo seguro en Solidity, complementando las pruebas unitarias tradicionales. No puede probar la ausencia de errores (ya que es aleatorio y no exhaustivo), pero aumenta en gran medida la confianza al cubrir una vasta gama de entradas y combinaciones de estados.

Más Allá del Fuzzing: Pruebas Formales y Herramientas Avanzadas​

Aunque el fuzzing y los invariantes detectan muchos problemas, hay casos en los que se utilizan métodos formales más potentes. La verificación de modelos y la demostración de teoremas implican especificar las propiedades deseadas en una lógica formal y usar probadores automáticos para verificarlas contra el código del contrato. Certora Prover (recientemente de código abierto) es una herramienta prominente en esta categoría. Permite a los desarrolladores escribir reglas en un lenguaje específico de dominio (CVL) y luego verifica automáticamente el contrato en busca de violaciones de esas reglas. Certora se ha utilizado para verificar invariantes críticos en protocolos como MakerDAO y Compound; por ejemplo, identificó el error del “invariante de deuda DAI” en MakerDAO (una sutil inconsistencia contable) que pasó desapercibido durante cuatro años. Notablemente, el motor de Certora ahora admite múltiples plataformas (EVM, la VM de Solana y eWASM), y al hacerlo de código abierto en 2025, hizo que la verificación formal de grado industrial estuviera disponible gratuitamente en Ethereum, Solana y Stellar. Este movimiento reconoce que las pruebas formales no deberían ser un lujo solo para equipos bien financiados.

Otras herramientas formales incluyen enfoques de verificación en tiempo de ejecución (por ejemplo, la semántica KEVM de Ethereum, o el Move Prover para cadenas basadas en Move). El Move Prover en particular está integrado en el lenguaje Move (utilizado por las blockchains Aptos y Sui). Permite escribir especificaciones formales junto con el código y puede probar automáticamente ciertas propiedades con una experiencia de usuario similar a un linter o un verificador de tipos. Esta estrecha integración reduce la barrera para que los desarrolladores en esas plataformas utilicen la verificación formal como parte del desarrollo.

Resumen: La auditoría de contratos inteligentes de hoy en día combina estas metodologías. El fuzzing y las pruebas de invariantes (ejemplificadas por Foundry y Echidna) son ampliamente adoptadas por su facilidad de uso y eficacia para detectar errores comunes. La ejecución simbólica y los analizadores estáticos todavía sirven para escanear rápidamente en busca de patrones de vulnerabilidad conocidos (con herramientas como Slither a menudo integradas en los pipelines de CI). Mientras tanto, las herramientas de verificación formal están madurando y expandiéndose a través de las cadenas, pero generalmente se reservan para propiedades críticas específicas o son utilizadas por firmas de auditoría especializadas debido a su complejidad. En la práctica, muchas auditorías combinan estos enfoques: por ejemplo, usando fuzzers para encontrar errores en tiempo de ejecución, herramientas estáticas para señalar errores obvios y verificaciones de especificaciones formales para invariantes clave como “ningún saldo de token excede el suministro total”.

Auditoría Asistida por IA con Modelos de Lenguaje Grandes​

La llegada de los modelos de lenguaje grandes (LLM) como GPT-3/4 (ChatGPT) y Codex de OpenAI ha introducido un nuevo paradigma para el análisis de contratos inteligentes. Estos modelos, entrenados en vastas cantidades de código y lenguaje natural, pueden razonar sobre el comportamiento del programa, explicar el código e incluso detectar ciertas vulnerabilidades mediante el reconocimiento de patrones y el conocimiento de “sentido común”. La pregunta es: ¿puede la IA aumentar o incluso automatizar la auditoría de contratos inteligentes?

Herramientas de Análisis de Vulnerabilidades Basadas en LLM​

Han surgido varios esfuerzos de investigación y herramientas prototipo que aplican LLM a la auditoría de contratos inteligentes:

• OpenAI Codex / ChatGPT (modelos generales): Los primeros experimentos simplemente consistían en proporcionar a GPT-3 o Codex el código del contrato y preguntar por posibles errores. Los desarrolladores descubrieron que ChatGPT podía identificar algunos patrones de vulnerabilidad bien conocidos e incluso sugerir correcciones. Sin embargo, las respuestas eran inconsistentes y no eran fiablemente exhaustivas. Una evaluación académica reciente señaló que el uso ingenuo de ChatGPT para la detección de vulnerabilidades “no produjo resultados significativamente mejores en comparación con la predicción aleatoria” en un conjunto de datos de referencia; esencialmente, si el modelo no se guía adecuadamente, puede alucinar problemas que no existen o pasar por alto vulnerabilidades reales. Esto destacó la necesidad de prompts cuidadosamente diseñados o de un ajuste fino para obtener resultados útiles.

• AuditGPT (2024): Esta es una herramienta académica que aprovechó ChatGPT (GPT-3.5/4) específicamente para verificar el cumplimiento del estándar ERC en contratos de Ethereum. Los investigadores observaron que muchos contratos de tokens ERC20/ERC721 violan reglas sutiles del estándar (lo que puede llevar a problemas de seguridad o compatibilidad). AuditGPT funciona dividiendo la auditoría en pequeñas tareas y diseñando prompts especializados para cada tipo de regla. El resultado fue impresionante: en pruebas con contratos reales, AuditGPT “identifica con éxito 418 violaciones de reglas ERC y solo informa 18 falsos positivos”, demostrando una alta precisión. De hecho, el artículo afirma que AuditGPT superó a un servicio de auditoría profesional en la búsqueda de errores de cumplimiento de ERC, a un costo menor. Esto sugiere que para dominios bien definidos y estrechos (como hacer cumplir una lista de reglas estándar), un LLM con buenos prompts puede ser notablemente efectivo y preciso.

• LLM-SmartAudit (2024): Otro proyecto de investigación, LLM-SmartAudit, adopta un enfoque más amplio al utilizar un sistema de conversación multiagente para auditar el código de Solidity. Establece múltiples agentes especializados de GPT-3.5/GPT-4 (por ejemplo, un “Auditor” centrado en la corrección, un “Atacante” pensando en cómo explotar) que conversan entre sí para analizar un contrato. En su evaluación, LLM-SmartAudit fue capaz de detectar una amplia gama de vulnerabilidades. Notablemente, en una prueba comparativa contra herramientas convencionales, el sistema basado en GPT-3.5 logró el recall general más alto (74 %), superando a todos los analizadores estáticos y simbólicos tradicionales que probaron (el siguiente mejor fue Mythril con un 54 % de recall). También fue capaz de encontrar todos los 10 tipos de vulnerabilidades en su conjunto de pruebas (mientras que cada herramienta tradicional tuvo dificultades con algunas categorías). Además, al cambiar a GPT-4 y enfocar el análisis (lo que llaman modo de Análisis Dirigido), el sistema pudo detectar fallos lógicos complejos que herramientas como Slither y Mythril pasaron por alto por completo. Por ejemplo, en un conjunto de contratos DeFi del mundo real, el enfoque basado en LLM encontró cientos de errores lógicos, mientras que las herramientas estáticas “no demostraron ninguna efectividad en la detección” de esos problemas. Estos resultados muestran el potencial de los LLM para detectar errores sutiles que están más allá del alcance de coincidencia de patrones de los analizadores tradicionales.

• Prometheus (PromFuzz) (2023): Un enfoque híbrido es usar LLM para guiar otras técnicas. Un ejemplo es PromFuzz, que utiliza un “agente auditor” basado en GPT para identificar áreas sospechosas en el código, luego genera automáticamente verificadores de invariantes y los alimenta a un motor de fuzzing. Esencialmente, el LLM realiza un primer análisis (tanto desde una perspectiva benigna como de atacante) para enfocar el fuzz testing en las vulnerabilidades probables. En las evaluaciones, este enfoque logró tasas de detección de errores muy altas —por ejemplo, más del 86 % de recall con cero falsos positivos en ciertos conjuntos de referencia— superando significativamente a los fuzzers independientes o herramientas anteriores. Esta es una dirección prometedora: usar la IA para orquestar y mejorar técnicas clásicas como el fuzzing, combinando las fortalezas de ambas.

• Otras Herramientas de IA: La comunidad ha visto varios otros conceptos de auditoría asistida por IA. Por ejemplo, el proyecto “Toucan” de Trail of Bits integró OpenAI Codex en su flujo de trabajo de auditoría (más sobre sus hallazgos a continuación). Algunas startups de seguridad también anuncian auditores de IA (por ejemplo, servicios de “Auditoría ChainGPT”), que generalmente envuelven GPT-4 con prompts personalizados para revisar contratos. Entusiastas del código abierto han creado bots de auditoría basados en ChatGPT en foros que toman un fragmento de Solidity y emiten posibles problemas. Si bien muchos de estos son experimentales, la tendencia general es clara: la IA se está explorando en todos los niveles del proceso de revisión de seguridad, desde la explicación y generación de documentación de código automatizada hasta la detección de vulnerabilidades e incluso la sugerencia de correcciones.

Capacidades y Limitaciones de los Auditores LLM​

Los LLM han demostrado capacidades notables en la auditoría de contratos inteligentes:

• Conocimiento Amplio: Un LLM como GPT-4 ha sido entrenado con innumerables códigos y vulnerabilidades. “Conoce” las trampas de seguridad comunes (reentrada, desbordamiento de enteros, etc.) e incluso algunos exploits históricos. Esto le permite reconocer patrones que podrían indicar un error y recordar las mejores prácticas de la documentación. Por ejemplo, podría recordar que transferFrom de ERC-20 debe verificar los permisos (y señalar la ausencia de dicha verificación como una violación). A diferencia de una herramienta estática que solo señala patrones conocidos, un LLM puede aplicar el razonamiento a código novedoso e inferir problemas que no fueron codificados explícitamente por un desarrollador de herramientas.

• Explicaciones Naturales: Los auditores de IA pueden proporcionar explicaciones legibles por humanos de posibles problemas. Esto es extremadamente valioso para la experiencia del desarrollador. Las herramientas tradicionales a menudo emiten advertencias crípticas que requieren experiencia para interpretar, mientras que una herramienta basada en GPT puede generar un párrafo explicando el error en un lenguaje sencillo e incluso sugerir una solución. AuditGPT, por ejemplo, no solo señaló las violaciones de las reglas ERC, sino que describió por qué el código violaba la regla y cuáles eran las implicaciones. Esto ayuda a incorporar a desarrolladores menos experimentados a los conceptos de seguridad.

• Flexibilidad: Con la ingeniería de prompts, los LLM pueden ser dirigidos para enfocarse en diferentes aspectos o seguir políticas de seguridad personalizadas. No están limitados por un conjunto fijo de reglas: si puedes describir una propiedad o patrón en palabras, el LLM puede intentar verificarlo. Esto los hace atractivos para auditar nuevos protocolos que podrían tener invariantes o lógicas únicas (donde escribir un análisis estático personalizado desde cero sería inviable).

Sin embargo, se han observado importantes desafíos y problemas de fiabilidad:

• Limitaciones de Razonamiento: Los LLM actuales a veces tienen dificultades con el complejo razonamiento lógico requerido para el análisis de seguridad. Trail of Bits informó que “los modelos no son capaces de razonar bien sobre ciertos conceptos de nivel superior, como la propiedad de los contratos, la reentrada y las relaciones entre funciones”. Por ejemplo, GPT-3.5/4 podría entender qué es la reentrada en teoría (e incluso explicarlo), pero puede fallar en reconocer una vulnerabilidad de reentrada si requiere comprender una secuencia de llamadas entre funciones y cambios de estado. El modelo también podría pasar por alto vulnerabilidades que involucran interacciones entre múltiples contratos o lógica dependiente del tiempo, porque eso va más allá del alcance del análisis de un solo fragmento de código.

• Falsos Positivos y Alucinaciones: Una preocupación importante es que los LLM pueden producir conclusiones que suenan seguras pero son incorrectas. En la auditoría, una “alucinación” podría ser señalar una vulnerabilidad que en realidad no existe, o malinterpretar el código. El experimento de Trail of Bits con Codex (GPT) encontró que a medida que escalaban a contratos del mundo real más grandes, “las tasas de falsos positivos y alucinaciones [se volvieron] demasiado altas”, hasta el punto de que ralentizarían a los auditores con demasiados informes espurios. Esta imprevisibilidad es problemática: una herramienta que grita “lobo” con demasiada frecuencia no será confiable para los desarrolladores. El éxito de AuditGPT en mantener bajos los falsos positivos (solo 18 de cientos de hallazgos) es alentador, pero eso fue en un dominio restringido. En el uso general, se necesita un diseño cuidadoso de los prompts y quizás bucles de revisión humana para filtrar los hallazgos de la IA.

• Limitaciones de Contexto: Los LLM tienen una limitación de ventana de contexto, lo que significa que solo pueden “ver” una cierta cantidad de código a la vez. Los contratos complejos a menudo abarcan múltiples archivos y miles de líneas. Si una IA no puede ingerir toda la base de código, podría pasar por alto conexiones importantes. Se utilizan técnicas como el corte de código (alimentar el contrato en trozos), pero corren el riesgo de perder la visión general. El equipo de LLM-SmartAudit señaló que con el límite de 4k tokens de GPT-3.5, no pudieron analizar algunos contratos grandes del mundo real hasta que cambiaron a GPT-4 con un contexto más grande. Incluso entonces, dividir el análisis en partes puede hacer que pase por alto errores que solo se manifiestan al considerar el sistema en su conjunto. Esto hace que el análisis de IA de protocolos enteros (con múltiples contratos que interactúan) sea un verdadero desafío en la actualidad.

• Integración y Herramientas: Hay una falta de herramientas de desarrollo robustas en torno a los auditores de IA. Ejecutar un análisis de LLM no es tan sencillo como ejecutar un linter. Implica llamadas a la API de un modelo, manejar la ingeniería de prompts, los límites de velocidad y analizar las respuestas de la IA. “El ecosistema de software en torno a la integración de LLM con software tradicional es demasiado rudimentario y todo es engorroso”, como lo expresó un equipo de auditoría. Prácticamente no existen marcos listos para usar para desplegar continuamente un auditor de IA en pipelines de CI mientras se gestionan sus incertidumbres. Esto está mejorando lentamente (algunos proyectos están explorando bots de CI que usan GPT-4 para la revisión de código), pero es temprano. Además, depurar por qué una IA dio un cierto resultado es difícil: a diferencia de las herramientas deterministas, no se puede rastrear fácilmente la lógica que llevó al modelo a señalar o pasar por alto algo.

• Costo y Rendimiento: Usar modelos grandes como GPT-4 es caro y puede ser lento. Si deseas incorporar una auditoría de IA en un pipeline de CI/CD, podría agregar varios minutos por contrato e incurrir en costos significativos de API para código grande. Los modelos ajustados o los LLM de código abierto podrían mitigar el costo, pero tienden a ser menos capaces que GPT-4. Hay investigación en curso sobre modelos más pequeños y especializados para la seguridad del código, pero en la actualidad los mejores resultados provienen de los grandes modelos propietarios.

En resumen, la auditoría asistida por LLM es prometedora pero no una solución mágica. Estamos viendo enfoques híbridos donde la IA ayuda a generar pruebas o analizar aspectos específicos, en lugar de hacer toda la auditoría de principio a fin. Por ejemplo, una IA podría sugerir posibles invariantes o áreas de riesgo, que luego un humano u otra herramienta investiga. Como comentó un ingeniero de seguridad, la tecnología aún no está lista para reemplazar a los auditores humanos en tareas críticas, dadas las lagunas de razonamiento y los obstáculos de integración. Sin embargo, ya puede ser un asistente útil: “algo imperfecto puede ser mucho mejor que nada” en casos donde las herramientas tradicionales se quedan cortas.

Precisión y Fiabilidad de Diferentes Cadenas de Herramientas​

Es instructivo comparar la precisión, cobertura y fiabilidad de los diversos enfoques de auditoría discutidos. A continuación se presenta un resumen de los hallazgos de la investigación y las evaluaciones de la industria:

• Herramientas de Análisis Estático: Los analizadores estáticos como Slither son valorados por su retroalimentación rápida y facilidad de uso. Típicamente tienen alta precisión pero un recall moderado, lo que significa que la mayoría de los problemas que informan son problemas reales (pocos falsos positivos por diseño), pero solo detectan ciertas clases de vulnerabilidades. Un estudio de benchmarking de 2024 (RQ1 de LLM-SmartAudit) encontró que Slither detectó alrededor del 46 % de las vulnerabilidades conocidas en un conjunto de pruebas. Mythril (ejecución simbólica) lo hizo ligeramente mejor con un 54 % de recall. Cada herramienta tenía fortalezas en tipos de errores particulares (por ejemplo, Slither es muy bueno para detectar problemas aritméticos o el uso de tx.origin, mientras que las herramientas simbólicas sobresalen en encontrar escenarios simples de reentrada), pero ninguna tenía una cobertura completa. Los falsos positivos para herramientas maduras como Slither son relativamente bajos: sus desarrolladores anuncian “mínimas falsas alarmas y ejecución rápida (menos de 1s por contrato)”, lo que lo hace adecuado para su uso en CI. No obstante, las herramientas estáticas pueden fallar si el código utiliza patrones complejos; podrían señalar casos límite que en realidad están manejados o pasar por alto errores lógicos profundos que no coinciden con ningún antipatrón conocido.

• Fuzzing y Pruebas de Propiedades: Los fuzzers como las pruebas de fuzz/invariantes de Foundry o Echidna de Trail of Bits han demostrado ser muy efectivos para encontrar errores en tiempo de ejecución y violaciones de invariantes. Estas herramientas tienden a tener casi cero falsos positivos en el sentido de que si se informa un error (una aserción falló), es una ejecución de contraejemplo real. La contrapartida está en los falsos negativos: si un error no se manifiesta dentro del espacio de entrada probado o el número de ejecuciones, puede pasar desapercibido. La cobertura depende de qué tan bien el fuzzer explore el espacio de estados. Con suficiente tiempo y buenas heurísticas, los fuzzers han encontrado muchos errores de alta gravedad que el análisis estático pasó por alto. Por ejemplo, Echidna pudo reproducir rápidamente los errores de MakerDAO y Compound que requirieron esfuerzos de verificación formal para ser encontrados. Sin embargo, el fuzzing no garantiza encontrar todos los errores lógicos. A medida que los contratos se vuelven más complejos, los fuzzers pueden requerir escribir invariantes adicionales o usar estrategias de búsqueda más inteligentes para alcanzar estados más profundos. En términos de métricas, el fuzzing no tiene un único número de “recall”, pero la evidencia anecdótica muestra que los invariantes importantes generalmente pueden ser rotos por un fuzzer si son rompibles. La fiabilidad es alta para lo que encuentra (no se necesita triaje manual para informes falsos), pero uno debe recordar que una prueba de fuzzing superada no es una prueba de corrección, solo un aumento de la confianza.

• Herramientas de Verificación Formal: Cuando es aplicable, la verificación formal proporciona la máxima garantía: una prueba exitosa significa que el 100 % de los estados satisfacen la propiedad. En términos de precisión, es efectivamente perfecta (sólida y completa) para las propiedades que puede probar. El mayor problema aquí no es la precisión de los resultados, sino la dificultad de uso y el alcance limitado. Las herramientas formales también pueden tener falsos negativos en la práctica: simplemente podrían no ser capaces de probar una propiedad verdadera debido a la complejidad (dando como resultado ningún resultado o un tiempo de espera, lo cual no es un falso positivo, pero significa que no logramos verificar algo que en realidad es seguro). También pueden tener errores de especificación, donde la herramienta “prueba” algo que no era la propiedad que pretendías (error del usuario). En auditorías reales, los métodos formales han detectado algunos errores críticos (los éxitos de Certora incluyen la detección de un sutil error en SushiSwap y un problema en la biblioteca PRBMath antes del despliegue). Pero su historial está limitado por la poca frecuencia con la que se aplican de manera exhaustiva; como señaló Trail of Bits, fue “difícil encontrar problemas públicos descubiertos únicamente a través de la verificación formal, en contraste con los muchos errores encontrados por el fuzzing”. Por lo tanto, aunque la verificación formal es extremadamente fiable cuando tiene éxito, su impacto en la cobertura general de la cadena de herramientas está limitado por el esfuerzo y la experiencia requeridos.

• Análisis Basado en LLM: La precisión de los auditores de IA es actualmente un objetivo en movimiento, ya que nuevas técnicas (y modelos más nuevos) están empujando rápidamente los límites. Podemos extraer algunos puntos de datos:

  • El sistema AuditGPT, enfocado en las reglas ERC, logró una precisión muy alta (≈96 % por recuento de falsos positivos) y encontró cientos de problemas que las herramientas estáticas o los humanos pasaron por alto. Pero esto fue en un dominio estrecho con prompts estructurados. No debemos generalizar que ChatGPT será 96 % preciso en la caza de vulnerabilidades arbitrarias; fuera de una configuración controlada, su rendimiento es menor.
  • En la detección de vulnerabilidades más amplia, LLM-SmartAudit (GPT-3.5) mostró un recall de ~74 % en un benchmark con una tasa moderada de falsos positivos, lo cual es mejor que cualquier herramienta tradicional individual. Cuando se actualizó a GPT-4 con prompts especializados (modo TA), mejoró significativamente; por ejemplo, en un conjunto de 1,400 vulnerabilidades del mundo real, el agente GPT-4 encontró ~48 % de los problemas específicos y ~47 % de los problemas lógicos complejos, mientras que Slither/Mythril/Conkas encontraron cada uno ~0 % (ninguno) de esos problemas complejos particulares. Esto demuestra que los LLM pueden expandir drásticamente la cobertura a tipos de errores que el análisis estático pasa por alto por completo. Por otro lado, el LLM no encontró más de la mitad de los problemas (por lo que también tiene sustanciales falsos negativos), y no está claro cuántos falsos positivos hubo entre los que informó; el estudio se centró más en el recall que en la precisión.
  • El experimento “Toucan” de Codex/GPT-4 de Trail of Bits es ilustrativo de los problemas de fiabilidad. Inicialmente, en ejemplos pequeños, Codex podía identificar vulnerabilidades conocidas (problemas de propiedad, reentrada) con prompts cuidadosos. Pero tan pronto como intentaron escalar, encontraron resultados inconsistentes e incorrectos. Informaron que “el número de fallos fue alto incluso en código de tamaño promedio” y difícil de predecir. Finalmente, concluyeron que GPT-4 (a principios de 2023) era solo una mejora incremental y todavía “carecía de características clave” como el razonamiento sobre flujos entre funciones. El resultado fue que la IA no redujo materialmente los falsos positivos de sus herramientas estáticas, ni aceleró de manera fiable su flujo de trabajo de auditoría. En otras palabras, la fiabilidad actual de un LLM general como auditor fue considerada insuficiente por auditores profesionales en esa prueba.

Para resumir, cada cadena de herramientas tiene diferentes fortalezas:

• Herramientas estáticas: Fiables para la detección rápida de problemas conocidos; bajo ruido, pero tipos de errores limitados (recall medio ~40–50 % en benchmarks).
• Fuzzing/pruebas de invariantes: Precisión muy alta (casi sin falsas alarmas) y fuerte para encontrar errores funcionales y dependientes del estado; la cobertura puede ser amplia pero no garantizada (sin métrica simple, depende del tiempo y la calidad de los invariantes). A menudo encuentra los mismos errores que las pruebas formales encontrarían si se les da suficiente guía.
• Verificación formal: El estándar de oro para la corrección absoluta en propiedades específicas; esencialmente 100 % de recall/precisión para esas propiedades si se aplica con éxito. Pero prácticamente limitado a problemas estrechos y requiere un esfuerzo significativo (aún no es una solución de un solo botón para auditorías completas).
• Análisis de IA (LLM): Cobertura potencialmente alta —puede encontrar errores en todas las categorías, incluidos los que otras herramientas pasan por alto— pero precisión variable. Con configuraciones especializadas, puede ser tanto preciso como amplio (como demostró AuditGPT para las verificaciones de ERC). Sin restricciones cuidadosas, puede lanzar una red amplia y requerir la validación humana de los resultados. La precisión “promedio” de ChatGPT en la detección de vulnerabilidades no es espectacular (cercana a la adivinación, en un estudio), pero los sistemas mejor diseñados que utilizan LLM están superando el rendimiento de las herramientas tradicionales. Hay investigación activa para hacer que los resultados de la IA sean más confiables (por ejemplo, haciendo que múltiples agentes se verifiquen entre sí, o combinando LLM con razonamiento estático para verificar las conclusiones de la IA).

Vale la pena señalar que la combinación de enfoques produce los mejores resultados. Por ejemplo, se podría ejecutar Slither (para detectar los problemas más evidentes sin ruido), luego usar Foundry/Echidna para hacer fuzzing de comportamientos más profundos, y quizás usar una herramienta basada en LLM para escanear en busca de patrones o invariantes no considerados. Cada uno cubrirá diferentes puntos ciegos de los otros.

Desafíos y Limitaciones de la Adopción en el Mundo Real​

En la práctica, adoptar la verificación formal o las herramientas de IA en un flujo de trabajo de desarrollo conlleva desafíos pragmáticos. Algunos problemas clave incluyen:

• Experiencia y Conocimientos del Desarrollador: La verificación formal tradicional tiene una curva de aprendizaje pronunciada. Escribir especificaciones formales (en CVL, Coq, el lenguaje de especificación de Move, etc.) es más como escribir pruebas matemáticas que escribir código. Muchos desarrolladores carecen de esta formación, y los expertos en métodos formales son escasos. Por el contrario, hacer fuzzing con Foundry o escribir invariantes en Solidity es mucho más accesible: se siente como escribir pruebas adicionales. Esta es una gran razón por la que las pruebas de fuzzing han tenido una adopción más rápida que las pruebas formales en la comunidad de Ethereum. El equipo de Trail of Bits señaló explícitamente que el fuzzing “produce resultados similares pero requiere significativamente menos habilidad y tiempo” que los métodos formales en muchos casos. Por lo tanto, aunque la verificación formal puede detectar diferentes errores, muchos equipos optan por el enfoque más fácil que obtiene resultados suficientemente buenos con menor esfuerzo.

• Integración en el Flujo de Trabajo de Desarrollo: Para que una herramienta sea ampliamente adoptada, necesita encajar en los pipelines de CI/CD y en la codificación diaria. Herramientas como Slither brillan aquí: “se integra fácilmente en las configuraciones de CI/CD, agilizando la automatización y ayudando a los desarrolladores.” Un desarrollador puede agregar Slither o Mythril a una GitHub Action y hacer que la compilación falle si se encuentran problemas. Las pruebas de fuzzing de Foundry se pueden ejecutar como parte de forge test cada vez. Las pruebas de invariantes incluso se pueden ejecutar continuamente en la nube con herramientas como CloudExec, y cualquier fallo se puede convertir automáticamente en una prueba unitaria usando fuzz-utils. Estas integraciones significan que los desarrolladores obtienen retroalimentación rápida y pueden iterar. En contraste, algo como el Certora Prover históricamente se ejecutaba como un proceso separado (o por un equipo de auditoría externo) y podría tardar horas en producir un resultado, no es algo que ejecutarías en cada commit. Las herramientas basadas en IA también enfrentan obstáculos de integración: llamar a una API y manejar su salida de manera determinista en CI no es trivial. También está el asunto de la seguridad y la privacidad: muchas organizaciones se sienten incómodas al enviar código de contrato propietario a un servicio de IA de terceros para su análisis. Las soluciones de LLM autoalojadas aún no son tan potentes como las grandes API en la nube, por lo que este es un punto conflictivo para la adopción de auditores de IA en CI.

• Falsos Positivos y Ruido: Una herramienta que informa muchos falsos positivos o hallazgos de baja gravedad puede reducir la confianza del desarrollador. Los analizadores estáticos han luchado con esto en el pasado; por ejemplo, las primeras versiones de algunas herramientas inundaban a los usuarios con advertencias, muchas de las cuales eran irrelevantes. El equilibrio entre señal y ruido es crucial. Slither es elogiado por sus mínimas falsas alarmas, mientras que una herramienta como Securify (en su forma de investigación) a menudo producía muchas advertencias que requerían un filtrado manual. Los LLM, como se discutió, pueden generar ruido si no se dirigen adecuadamente. Es por eso que actualmente las sugerencias de IA generalmente se toman como un consejo, no como algo absoluto. Es más probable que los equipos adopten una herramienta ruidosa si es utilizada por un equipo de seguridad separado o en un contexto de auditoría, pero para el uso diario, los desarrolladores prefieren herramientas que den resultados claros y accionables con bajo ruido. Lo ideal es “hacer que la compilación falle” solo en errores definitivos, no en hipotéticos. Lograr esa fiabilidad es un desafío continuo, especialmente para las herramientas de IA.

• Escalabilidad y Rendimiento: La verificación formal puede ser computacionalmente intensiva. Como se señaló, los solucionadores pueden agotar el tiempo en contratos complejos. Esto dificulta la escalabilidad a sistemas grandes. Si verificar una propiedad lleva horas, no estarás verificando docenas de propiedades en cada cambio de código. El fuzz testing también enfrenta límites de escalabilidad: explorar un espacio de estados enorme o un contrato con muchos métodos combinatoriamente puede ser lento (aunque en la práctica los fuzzers pueden ejecutarse en segundo plano o durante la noche para profundizar su búsqueda). Los modelos de IA tienen tamaños de contexto fijos y aumentar la capacidad de un modelo es caro. Si bien el contexto de 128k tokens de GPT-4 es una bendición, alimentarlo con cientos de kilobytes de código de contrato es costoso y aún no es suficiente para proyectos muy grandes (imagina un protocolo complejo con muchos contratos, podrías exceder eso). También está la escalabilidad entre cadenas: si tu proyecto involucra interacciones entre contratos en diferentes cadenas (Ethereum ↔ otra cadena), verificar o analizar esa lógica cross-chain es aún más complejo y probablemente esté más allá de las herramientas actuales.

• Supervisión y Verificación Humana: Al final del día, la mayoría de los equipos todavía confían en auditores humanos expertos para la aprobación final. Las herramientas automatizadas son ayudas, no reemplazos. Una limitación de todas estas herramientas es que operan dentro de los límites de propiedades o patrones conocidos. Podrían pasar por alto un tipo de error totalmente nuevo o un fallo económico sutil en el diseño de un protocolo DeFi. Los auditores humanos usan la intuición y la experiencia para considerar cómo un atacante podría abordar el sistema, a veces de maneras que ninguna herramienta está explícitamente programada para hacer. Ha habido casos en los que los contratos pasaron todas las verificaciones automatizadas pero un humano encontró más tarde una vulnerabilidad en la lógica de negocio o un vector de ataque creativo. Por lo tanto, un desafío es evitar una falsa sensación de seguridad: los desarrolladores deben interpretar correctamente la salida de las herramientas formales y de la IA y no asumir que “no se encontraron problemas” significa que el código es 100 % seguro.

• Mantenimiento de Especificaciones y Pruebas: Para la verificación formal en particular, un problema práctico es la deriva de la especificación. La especificación (invariantes, reglas, etc.) puede quedar desactualizada a medida que el código evoluciona. Asegurar que el código y su especificación formal permanezcan sincronizados es una tarea de gestión no trivial. Si los desarrolladores no son vigilantes, las pruebas podrían “pasar” simplemente porque están probando algo que ya no es relevante para los requisitos reales del código. De manera similar, las pruebas de invariantes deben actualizarse a medida que cambia el comportamiento esperado del sistema. Esto requiere una cultura de desarrollo impulsado por invariantes que no todos los equipos tienen (aunque hay un impulso para fomentarla).

En resumen, las principales limitaciones son las personas y los procesos, más que la capacidad bruta de la tecnología. Los métodos formales y asistidos por IA pueden mejorar enormemente la seguridad, pero deben implementarse de una manera que se ajuste a los flujos de trabajo y conjuntos de habilidades de los desarrolladores. Alentadoramente, tendencias como el desarrollo impulsado por invariantes (escribir invariantes críticos desde el primer día) están ganando tracción, y las herramientas están mejorando lentamente para hacer que los análisis avanzados sean más plug-and-play. La apertura de herramientas importantes (por ejemplo, Certora Prover) y la integración del fuzzing en marcos populares (Foundry) están reduciendo las barreras. Con el tiempo, esperamos que la brecha entre lo que “un desarrollador promedio” puede hacer y lo que “un investigador con doctorado” puede hacer se reduzca, en términos de usar estas potentes técnicas de verificación.

Herramientas de Auditoría de Código Abierto vs. Comerciales​

El panorama de las herramientas de seguridad de contratos inteligentes incluye tanto proyectos de código abierto como servicios comerciales. Cada uno tiene su papel y, a menudo, se complementan entre sí:

• Herramientas de Código Abierto: La mayoría de las herramientas de auditoría ampliamente utilizadas en el ecosistema de Ethereum son de código abierto. Esto incluye Slither (analizador estático), Mythril (ejecución simbólica), Echidna (fuzzer), Manticore (ejecución simbólica/concólica), Securify (analizador de ETH Zurich), Solhint/Ethlint (linters) y, por supuesto, Foundry mismo. Las herramientas de código abierto son preferidas por algunas razones: (1) Transparencia – los desarrolladores pueden ver cómo funciona la herramienta y confiar en que no ocurre nada malicioso u oculto (importante en un ecosistema abierto). (2) Contribución de la Comunidad – las reglas y características son agregadas por una amplia comunidad (Slither, por ejemplo, tiene muchos detectores contribuidos por la comunidad). (3) Costo – son de uso gratuito, lo cual es importante para los muchos proyectos pequeños/startups en Web3. (4) Integración – las herramientas abiertas generalmente se pueden ejecutar localmente o en CI sin obstáculos legales, y a menudo se pueden personalizar o programar para necesidades específicas del proyecto.

  Las herramientas de código abierto han evolucionado rápidamente. Por ejemplo, el soporte de Slither para nuevas versiones y patrones de Solidity es actualizado continuamente por Trail of Bits. Mythril, desarrollado por ConsenSys, puede analizar no solo Ethereum sino cualquier cadena compatible con EVM trabajando sobre el bytecode, mostrando cómo las herramientas abiertas pueden ser reutilizadas fácilmente en diferentes cadenas. La desventaja de las herramientas abiertas es que a menudo vienen con un “úsese bajo su propio riesgo” – sin soporte oficial ni garantías. Puede que no escalen o no tengan el pulido de la interfaz de usuario de un producto comercial. Pero en blockchain, incluso muchas empresas utilizan herramientas de código abierto como sus herramientas principales internamente (a veces con ligeras modificaciones personalizadas).

• Servicios y Herramientas Comerciales: Algunas empresas han ofrecido análisis de seguridad como producto. Ejemplos incluyen MythX (una API de escaneo basada en la nube de ConsenSys Diligence), Certora (que ofrecía su probador como servicio antes de hacerlo de código abierto), CertiK y SlowMist (firmas que tienen escáneres internos e IA que utilizan en auditorías u ofrecen a través de paneles de control), y algunos nuevos participantes como Securify de ChainSecurity (la empresa fue adquirida y su herramienta se usó internamente) o SolidityScan (un escáner en la nube que genera un informe de auditoría). Las herramientas comerciales a menudo buscan proporcionar una experiencia más fácil de usar o un servicio integrado. Por ejemplo, MythX se integró con extensiones de IDE y plugins de CI para que los desarrolladores pudieran enviar sus contratos a MythX y recibir un informe detallado, incluyendo una puntuación de vulnerabilidad y detalles para solucionar los problemas. Estos servicios suelen ejecutar una combinación de técnicas de análisis bajo el capó (coincidencia de patrones, ejecución simbólica, etc.) ajustadas para minimizar los falsos positivos.

  La propuesta de valor de las herramientas comerciales suele ser la conveniencia y el soporte. Pueden mantener una base de conocimientos de vulnerabilidades continuamente actualizada y proporcionar soporte al cliente para interpretar los resultados. También pueden manejar cálculos pesados en la nube (para que no necesites ejecutar un solucionador localmente). Sin embargo, el costo es un factor: muchos proyectos optan por no pagar por estos servicios, dada la disponibilidad de alternativas gratuitas. Además, en el espíritu de la descentralización, algunos desarrolladores son reacios a depender de servicios de código cerrado para la seguridad (el ethos de “verifica, no confíes”). La apertura del Certora Prover en 2025 es un evento notable: convirtió lo que era una herramienta comercial de alta gama en un recurso comunitario. Se espera que este movimiento acelere la adopción, ya que ahora cualquiera puede intentar verificar formalmente sus contratos sin una licencia de pago, y la apertura del código permitirá a los investigadores mejorar la herramienta o adaptarla a otras cadenas.

• Servicios de Auditoría Humana: Vale la pena mencionar que más allá de las herramientas de software, muchas auditorías son realizadas por firmas profesionales (Trail of Bits, OpenZeppelin, Certik, PeckShield, etc.). Estas firmas utilizan una mezcla de las herramientas mencionadas (en su mayoría de código abierto) y scripts propietarios. Los resultados de estos esfuerzos a menudo se mantienen privados o solo se resumen en informes de auditoría. No hay exactamente una dicotomía “abierto vs. comercial” aquí, ya que incluso las firmas de auditoría comerciales dependen en gran medida de herramientas de código abierto. La diferenciación radica más en la experiencia y el esfuerzo manual. Dicho esto, algunas firmas están desarrollando plataformas de auditoría asistida por IA propietarias para obtener una ventaja (por ejemplo, hubo informes de que “ChainGPT” se usaba para auditorías internas, o que CertiK desarrollaba una IA llamada Skynet para el monitoreo en cadena). Esas no son herramientas públicas per se, por lo que su precisión y métodos no están ampliamente documentados.

En la práctica, un patrón común es código abierto primero, comercial opcional. Los equipos usarán herramientas abiertas durante el desarrollo y las pruebas (porque pueden integrarlas fácilmente y ejecutarlas tan a menudo como sea necesario). Luego, podrían usar uno o dos servicios comerciales como una verificación adicional antes del despliegue; por ejemplo, ejecutar un escaneo de MythX para obtener una “segunda opinión” o contratar a una firma que use herramientas avanzadas como Certora para verificar formalmente un componente crítico. Con las líneas difuminándose (Certora de código abierto, los resultados de MythX a menudo se superponen con las herramientas abiertas), la distinción es menos sobre la capacidad y más sobre el soporte y la conveniencia.

Un cruce notable es el soporte multi-cadena de Certora: al soportar formalmente Solana y Stellar, abordan plataformas donde existen menos alternativas abiertas (por ejemplo, Ethereum tiene muchas herramientas abiertas, Solana casi no tenía ninguna hasta hace poco). A medida que las herramientas de seguridad se expanden a nuevos ecosistemas, es posible que veamos más ofertas comerciales llenando los vacíos, al menos hasta que el código abierto se ponga al día.

Finalmente, vale la pena señalar que abierto vs. comercial no es un antagonismo aquí; a menudo aprenden el uno del otro. Por ejemplo, las técnicas pioneras en herramientas académicas/comerciales (como la interpretación abstracta utilizada en Securify) eventualmente llegan a las herramientas abiertas, y a la inversa, los datos del uso de herramientas abiertas pueden guiar las mejoras de las herramientas comerciales. El resultado final buscado por ambas partes es una mejor seguridad para todo el ecosistema.

Aplicabilidad entre Cadenas (Cross-Chain)​

Aunque Ethereum ha sido el punto focal para la mayoría de estas herramientas (dada su dominancia en la actividad de contratos inteligentes), los conceptos de verificación formal y auditoría asistida por IA son aplicables a otras plataformas blockchain también. Así es como se traducen:

• Cadenas Compatibles con EVM: Blockchains como BSC, Polygon, Avalanche C-Chain, etc., que utilizan la Ethereum Virtual Machine, pueden usar directamente todas las mismas herramientas. A una prueba de fuzzing o un análisis estático no le importa si tu contrato se desplegará en la mainnet de Ethereum o en Polygon: el bytecode y el lenguaje fuente (Solidity/Vyper) son los mismos. De hecho, Mythril y Slither pueden analizar contratos de cualquier cadena EVM extrayendo el bytecode de una dirección (Mythril solo necesita un punto final RPC). Muchos proyectos DeFi en estas cadenas ejecutan Slither y Echidna tal como lo haría un proyecto de Ethereum. Las auditorías de protocolos en BSC o Avalanche suelen utilizar el mismo conjunto de herramientas que las auditorías de Ethereum. Por lo tanto, cross-chain en el contexto de EVM significa principalmente reutilizar la cadena de herramientas de Ethereum.

• Solana: Los contratos inteligentes de Solana se escriben en Rust (generalmente a través del framework Anchor) y se ejecutan en la máquina virtual BPF. Este es un entorno muy diferente al de Ethereum, por lo que las herramientas específicas de Ethereum no funcionan directamente. Sin embargo, se aplican los mismos principios. Por ejemplo, se puede hacer fuzz testing en programas de Solana utilizando las bibliotecas de fuzzing nativas de Rust o herramientas como cargo-fuzz. La verificación formal en Solana había sido casi inexistente hasta hace poco. La colaboración entre Certora y los ingenieros de Solana produjo una herramienta de verificación interna para programas de Solana que puede probar contratos de Rust/Anchor contra especificaciones. Como se señaló, Certora extendió su probador a la VM de Solana, lo que significa que los desarrolladores pueden escribir reglas sobre el comportamiento del programa de Solana y verificarlas tal como lo harían para Solidity. Esto es significativo porque el enfoque de moverse rápido de Solana significaba que muchos contratos se lanzaron sin el tipo de pruebas rigurosas vistas en Ethereum; las herramientas formales podrían mejorar eso. La auditoría de IA para Solana también es plausible: un LLM que entienda Rust podría ser instruido para verificar un programa de Solana en busca de vulnerabilidades (como la falta de verificaciones de propiedad o errores aritméticos). Podría requerir un ajuste fino en patrones específicos de Solana, pero dada la popularidad de Rust, GPT-4 es bastante competente leyendo código Rust. Pronto podríamos ver surgir herramientas al estilo “ChatGPT para Anchor”.

• Polkadot y Cadenas Basadas en Substrate: Los contratos inteligentes de Polkadot se pueden escribir en Rust (compilado a WebAssembly) usando el framework ink!, o puedes ejecutar un pallet EVM (como lo hace Moonbeam) que nuevamente permite Solidity. En el caso de ink!/Wasm, las herramientas de verificación aún son incipientes. Se podría intentar verificar formalmente las propiedades de un contrato Wasm utilizando marcos de verificación generales de Wasm (por ejemplo, el Proyecto Verona de Microsoft u otros han investigado la seguridad de Wasm). El probador de código abierto de Certora también menciona soporte para los contratos inteligentes WASM de Stellar, que son similares en concepto a cualquier cadena basada en Wasm. Por lo tanto, es probable que también sea aplicable a los contratos Wasm de Polkadot. El fuzz testing de contratos ink! se puede hacer escribiendo pruebas en Rust (las pruebas de propiedades en Rust pueden cumplir un rol similar). La auditoría de IA de contratos ink! implicaría analizar código Rust también, lo cual un LLM puede hacer con el contexto adecuado (aunque podría no conocer las macros o traits específicos de ink! sin algunas pistas).

  Además, Polkadot está explorando el lenguaje Move para el desarrollo de contratos inteligentes paralelos (como se ha insinuado en algunos foros de la comunidad). Si Move se utiliza en las parachains de Polkadot, el Move Prover viene con él, trayendo capacidades de verificación formal por diseño. El énfasis de Move en la seguridad (programación orientada a recursos) y su probador integrado muestran una propagación cross-chain de los métodos formales desde el principio.

• Otras Blockchains: Plataformas como Tezos (contratos inteligentes Michelson) y Algorand (programas TEAL) han tenido esfuerzos de verificación formal. Tezos, por ejemplo, tiene una herramienta llamada Mi-Cho-Coq que proporciona una semántica formal de Michelson y permite probar propiedades. Estas son más del lado académico pero demuestran que cualquier blockchain con una semántica de contrato bien definida puede ser sometida a verificación formal. La auditoría de IA podría, en principio, aplicarse a cualquier lenguaje de programación; es cuestión de entrenar o instruir al LLM apropiadamente. Para lenguajes menos comunes, un LLM podría necesitar algún ajuste fino para ser efectivo, ya que puede no haber sido preentrenado con suficientes ejemplos.

• Interacciones Cross-Chain: Un desafío más nuevo es verificar las interacciones entre cadenas (como puentes o mensajería entre cadenas). La verificación formal aquí podría implicar modelar el estado de múltiples cadenas y el protocolo de comunicación. Esto es muy complejo y actualmente está más allá de la mayoría de las herramientas, aunque protocolos de puentes específicos han sido analizados manualmente por seguridad. La IA podría ayudar a revisar el código cross-chain (por ejemplo, revisar un contrato de Solidity que interactúa con un protocolo IBC en Cosmos), pero aún no hay una solución lista para usar.

En esencia, las herramientas de Ethereum han allanado el camino para otras cadenas. Muchas de las herramientas de código abierto están siendo adaptadas: por ejemplo, hay esfuerzos para crear un analizador estático similar a Slither para Solana (Rust), y los conceptos de pruebas de invariantes son agnósticos al lenguaje (las pruebas basadas en propiedades existen en muchos lenguajes). La apertura de motores potentes (como el de Certora para múltiples VM) es particularmente prometedora para la seguridad cross-chain: la misma plataforma podría usarse para verificar un contrato de Solidity, un programa de Solana y un contrato de Move, siempre que cada uno tenga una especificación adecuada escrita. Esto fomenta una postura de seguridad más uniforme en toda la industria.

También vale la pena señalar que la auditoría asistida por IA beneficiará a todas las cadenas, ya que al modelo se le puede enseñar sobre vulnerabilidades en cualquier contexto. Siempre que se le proporcione a la IA la información correcta (especificaciones del lenguaje, patrones de errores conocidos en ese ecosistema), puede aplicar un razonamiento similar. Por ejemplo, se le podría pedir a ChatGPT que audite un contrato de Solidity o un módulo de Move con el prompt apropiado, y hará ambas cosas; incluso podría detectar algo como “este módulo de Move podría violar la conservación de recursos” si tiene ese concepto. La limitación es si la IA fue expuesta a suficientes datos de entrenamiento para esa cadena. Ethereum, al ser el más popular, probablemente ha sesgado los modelos para que sean mejores en Solidity. A medida que otras cadenas crezcan, futuros LLM o derivados ajustados podrían cubrirlas también.

Conclusión​

La Verificación Formal de Contratos Inteligentes y Auditoría Asistida por IA es un campo en rápida evolución. Ahora tenemos un rico conjunto de herramientas: desde analizadores estáticos deterministas y marcos de fuzzing que mejoran la fiabilidad del código, hasta IA de vanguardia que puede razonar sobre el código de maneras similares a las humanas. La verificación formal, que alguna vez fue una actividad académica de nicho, se está volviendo más práctica a través de mejores herramientas e integración. La IA, a pesar de sus limitaciones actuales, ha mostrado destellos de capacidades revolucionarias en la automatización del análisis de seguridad.

Todavía no existe una solución única para todos: la auditoría del mundo real combina múltiples técnicas para lograr una defensa en profundidad. Las pruebas de fuzz e invariantes de Foundry ya están elevando el listón de lo que se espera antes del despliegue (detectando muchos errores que pasarían desapercibidos en las pruebas básicas). La auditoría asistida por IA, cuando se usa con cuidado, puede actuar como un multiplicador de fuerza para los auditores, destacando problemas y verificando el cumplimiento a una escala y velocidad que la revisión manual por sí sola no puede igualar. Sin embargo, la experiencia humana sigue siendo crucial para impulsar estas herramientas, interpretar sus hallazgos y definir las propiedades correctas a verificar.

De cara al futuro, podemos esperar una mayor convergencia de estos enfoques. Por ejemplo, la IA podría ayudar a escribir especificaciones formales o sugerir invariantes (“IA, ¿qué propiedades de seguridad deberían mantenerse para este contrato DeFi?”). Las herramientas de fuzzing podrían incorporar IA para guiar la generación de entradas de manera más inteligente (como lo hace PromFuzz). Los motores de verificación formal podrían usar el aprendizaje automático para decidir qué lemas o heurísticas aplicar. Todo esto contribuirá a contratos inteligentes más seguros no solo en Ethereum, sino en todas las plataformas blockchain. La visión final es un futuro donde los contratos inteligentes críticos puedan desplegarse con alta confianza en su corrección, un objetivo que probablemente se logrará mediante el uso sinérgico de métodos formales y asistencia de IA, en lugar de cualquiera de ellos por separado.

Fuentes:

• Resumen de fuzzing y pruebas de invariantes de Foundry
• Trail of Bits sobre fuzzing vs. verificación formal
• Trail of Bits sobre las limitaciones de la verificación formal
• Patrick Collins sobre fuzz/invariantes vs. métodos formales
• Trail of Bits sobre invariantes en auditorías
• Medium (BuildBear) sobre el uso de Slither y Mythril
• Resultados de AuditGPT (cumplimiento de ERC)
• Trail of Bits sobre las limitaciones de LLM (Codex/GPT-4)
• Rendimiento de LLM-SmartAudit vs. herramientas tradicionales
• Estudio “Detection Made Easy” sobre la precisión de ChatGPT
• Rendimiento de PromFuzz (LLM+fuzz)
• Anuncio de código abierto de Certora (multi-cadena)
• Descripción de Move Prover (Aptos)
• Antecedentes de análisis estático (literatura sobre seguridad de contratos inteligentes)