Vitalik Buterin rechaza la tesis de que la IA condena la ciberseguridad

Buterin escribió en su publicación del 17 de septiembre en X que no está de acuerdo con la opinión cada vez más común de que «el hackeo con IA significa que la ciberseguridad está condenada». Afirmó que las personas que siguen teniendo criptomonedas están apostando implícitamente a que los sistemas digitales seguros pueden sobrevivir a ataques automatizados más potentes, y añadió que aproximadamente el 90 % de su propio patrimonio neto sigue en cripto.

Su argumento se centra en la verificación formal, una técnica que utiliza especificaciones matemáticas y demostraciones para determinar si el software se comporta de acuerdo con propiedades predefinidas. Buterin usó como analogía la demostración avanzada de teoremas matemáticos y dijo que una IA suficientemente capaz podría ayudar a demostrar que «este programa es seguro» incluso cuando el propio software es complejo.

Buterin afirma que la verificación formal puede favorecer a los defensores

El argumento de Buterin no trata la seguridad con IA como una carrera en la que los investigadores defensivos simplemente encuentran errores antes que los atacantes. Su publicación describe, en cambio, un modelo en el que los desarrolladores definen las propiedades que debe cumplir un sistema y luego utilizan herramientas de demostración automatizadas para establecer que la implementación las respeta.

La propia documentación de verificación formal de Ethereum describe la técnica en términos más limitados. Señala que la verificación formal puede demostrar matemáticamente que un contrato inteligente cumple una especificación formal, ofreciendo garantías más sólidas que las pruebas ordinarias para las propiedades incluidas en esa especificación.

La misma documentación de Ethereum identifica una limitación importante detrás de los comentarios de Buterin. Una demostración establece que el software satisface la especificación que se está comprobando; no demuestra automáticamente que los desarrolladores hayan definido correctamente todas las propiedades de seguridad. Las especificaciones mal elegidas o incompletas pueden dejar comportamientos fuera de la demostración.

Buterin hizo la misma distinción en su publicación. Sostuvo que definir la «seguridad» de forma demasiado restringida puede omitir vías de ataque que afectan a áreas como protocolos, servidores, bases de datos, capas de red, cachés u otros componentes de soporte. Por ello, su dirección propuesta es verificar una mayor parte del sistema completo en lugar de etiquetar a un pequeño grupo de módulos como críticos para la seguridad.

Buterin ya había descrito la verificación formal asistida por IA como una posible «forma final» del desarrollo de software. Sus comentarios anteriores aplicaban este enfoque a áreas como el consenso de Ethereum, los sistemas de conocimiento cero y la criptografía resistente a la computación cuántica.

Ethereum ya está probando la seguridad asistida por IA

Los investigadores de Ethereum ya están utilizando la IA en trabajos de seguridad, aunque los sistemas actuales siguen lejos de la demostración automática de la seguridad de todo el sistema.

El equipo de Seguridad del Protocolo de la Fundación Ethereum informó en julio de que agentes de IA coordinados habían encontrado defectos reales en sistemas utilizados por Ethereum. Uno de los hallazgos confirmados implicaba un fallo alcanzable de forma remota en la implementación de red Gossipsub de libp2p en Rust.

La falla se convirtió en CVE-2026-34219. El registro de la Base de Datos Nacional de Vulnerabilidades de EE. UU. indica que las versiones anteriores a la 0.49.4 podían bloquearse de forma remota mediante un mensaje PRUNE manipulado que provocaba un desbordamiento aritmético durante el manejo de backoff de Gossipsub. La versión 0.49.4 corrigió el problema.

El equipo de seguridad de la Fundación afirmó que el descubrimiento de vulnerabilidades no era la parte más difícil del flujo de trabajo con IA. Los investigadores descubrieron que los agentes de IA generaban con frecuencia informes convincentes que implicaban rutas de ejecución inalcanzables, fallos solo de depuración o demostraciones formales que técnicamente pasaban pero demostraban una propiedad más débil de lo previsto.

La reproducción independiente siguió siendo un requisito antes de que el equipo aceptara un hallazgo. La Fundación señaló que se necesitaban comprobaciones automatizadas y revisión humana porque un agente podía producir una demostración de apariencia válida que no lograba restringir el comportamiento del software que los investigadores realmente querían probar.

La experiencia de la Fundación se describió como un problema de clasificación: la IA podía generar un gran número de vulnerabilidades candidatas, pero los investigadores aún tenían que determinar si cada problema era alcanzable y relevante en producción.

La verificación formal entra en la hoja de ruta del protocolo de Ethereum

La Fundación Ethereum ha incorporado por separado la verificación formal a su programa actual de investigación del protocolo. En su actualización de prioridades del protocolo del 7 de septiembre, la Fundación afirmó que la verificación formal serviría como herramienta transversal en sus áreas de investigación plurianuales restantes. El documento cubre el trabajo sobre privacidad, estado, desarrollo de zkEVM, seguridad poscuántica y otros componentes del protocolo hasta 2029.

La misma hoja de ruta señala que se espera que el desarrollo de un zkEVM de L1 impulse las herramientas de verificación formal, los flujos de trabajo y los componentes criptográficos verificados. Los investigadores de Ethereum trabajan hacia un sistema en el que los validadores acaben verificando pruebas de ejecución sucintas en lugar de volver a ejecutar cada bloque de forma independiente.

Otro proyecto de la Fundación Ethereum lanzado en agosto ya combina agentes de IA con demostraciones comprobadas por máquina. El proyecto better.codes permite a los investigadores dirigir sistemas de IA hacia un problema de solidez criptográfica formalizado en Lean, mientras que el núcleo de Lean comprueba si las demostraciones presentadas satisfacen un enunciado de teorema fijo.

El informe de financiación del segundo trimestre de la Fundación enumera más trabajos que combinan grandes modelos de lenguaje con métodos formales. Los proyectos incluyen ETHeorem para comprobar las implementaciones del cliente Ethereum frente a las especificaciones, SPECA y LeanAgent para el trabajo automatizado de cumplimiento del protocolo, y la verificación formal relacionada con la infraestructura zkVM de RISC-V.

La hoja de ruta técnica actualizada de Ethereum otorga a la verificación formal un papel junto a la privacidad, las pruebas de conocimiento cero y la protección poscuántica. Por lo tanto, los comentarios de Buterin del 17 de septiembre continúan una dirección de investigación existente en lugar de anunciar una nueva actualización o una bifurcación programada. Su publicación no mencionó un nuevo EIP, una fecha de despliegue ni una regla obligatoria que exija que todos los programas de Ethereum se sometan a verificación formal.

La evidencia actual de IA también muestra una mayor capacidad ofensiva

Investigaciones recientes en ciberseguridad respaldan la preocupación de que la IA está haciendo a los atacantes más capaces, incluso cuando el uso defensivo se expande. Anthropic afirmó en su informe de inteligencia de amenazas de septiembre que había observado a actores maliciosos utilizando IA para automatizar la investigación de vulnerabilidades, el desarrollo de exploits y campañas contra múltiples objetivos. La compañía señaló que algunos operadores mantenían flujos de trabajo automatizados capaces de realizar investigaciones de vulnerabilidades de forma continua.

Investigaciones anteriores de Anthropic encontraron evidencia similar a gran escala. Su panel de divulgación coordinada indicó que, hasta el 26 de agosto, la compañía había divulgado 2.300 vulnerabilidades descubiertas por IA en 392 proyectos de código abierto, con 421 parches aplicados en los proyectos originales en ese momento.

Anthropic ha descrito la misma tecnología como útil para la defensa. Su iniciativa Project Glasswing informó del uso de modelos de frontera con empresas de seguridad y proveedores de software para localizar fallos de gravedad alta y crítica antes de que los actores maliciosos pudieran explotarlos.

El lado ofensivo sigue siendo medible. El estudio de Anthropic de junio examinó 832 cuentas asociadas con actividad cibernética maliciosa desde marzo de 2025 hasta marzo de 2026 y encontró actores de amenazas utilizando IA en múltiples etapas de las operaciones cibernéticas. Buterin ya había rechazado un argumento separado según el cual los riesgos de seguridad impulsados por la IA podrían dañar gravemente la confianza en Bitcoin. Afirmó que los problemas de la capa de red a menudo podían abordarse mediante actualizaciones de software y de la infraestructura de minería, al tiempo que describió como muy improbables las rupturas reales de los hashes de Bitcoin o de su mecanismo de prueba de trabajo.

El informe de septiembre de Anthropic señaló que sus investigadores habían identificado a operadores que utilizaban cadenas de exploits construidas con IA contra dispositivos de seguridad y objetivos gubernamentales, y que algunas campañas producían vulnerabilidades previamente desconocidas que los atacantes validaban en sus propios entornos de prueba.