Bend 2: la trampa del vibe coding que reinventa la rueda

El caso Bend 2: cuando la IA reinventa la rueda

El desarrollador Liam Powell publicó esta semana una crítica directa a Bend 2, un lenguaje que se promociona como "el lenguaje de la era de la programación con IA": los humanos escriben "leyes", el modelo escribe implementaciones y pruebas, y el compilador verifica que las pruebas sean correctas. Powell reprodujo la demo oficial del lenguaje — un juego donde el jugador no debe tocar la bandera — y encontró un dato revelador: el programa necesita 58 líneas para definir las reglas y 442 líneas adicionales para demostrar que se cumplen. Para el mismo problema, Powell pidió a una IA que lo reescribiera en SPARK, un lenguaje open source de verificación formal sobre Ada, sin más guía. Resultado: las 12 verificaciones se resuelven automáticamente con GNATprove en un archivo mucho más corto.

La diferencia no es estética. Es la distancia entre reinventar la rueda y apoyarse en un campo — la verificación formal — que existe desde hace décadas y que, según Powell, no aparece ni una sola vez en la web ni en el repositorio de Bend.

Verificación formal: el campo que Bend no vio

La verificación formal es una disciplina consolidada. SPARK, mantenido por AdaCore y Altran, lleva años usándose en aviación, ferrocarriles y software crítico donde un fallo cuesta vidas o millones. Su enfoque es declarar invariantes y precondiciones junto al código; herramientas como GNATprove intentan demostrar automáticamente que se cumplen, sin pedir a un LLM que "rellene" una prueba a mano. En el ejemplo de Bend, GNATprove demuestra 12 checks sin intervención manual extensa.

🤖 La IA no es solo para leer sobre ella

En la comunidad la aplicamos: automatización, agentes IA y herramientas reales para emprender, no solo para informarte.

👥 Aplicarla en la comunidad

La disciplina tiene además un campo académico y comercial en plena expansión. La empresa Pramaana Labs anunció en junio de 2026 una ronda semilla de US$27 millones liderada por Khosla Ventures, con Accel, Boldcap, Nexus Venture Partners, Premji Invest y Unbound, para construir un sistema que combina un LLM con un verificador estilo LEAN — el proof assistant open source nacido en Microsoft Research en 2013 y premiado por ACM SIGPLAN en 2025, según TechTimes. Su CEO, Ranjan Rajagopalan, lo resume así: "AI aprendió a sonar correcta antes de aprender a ser correcta".

Hay un matiz importante: la verificación formal demuestra que el código cumple la especificación que un humano escribió, no que la especificación capture la regla del mundo real. El investigador de Cambridge Martin Kleppmann lo planteó en diciembre de 2025 — citado por TechTimes —: "A medida que el proceso de verificación se automatiza, el reto se traslada a definir correctamente la especificación: ¿cómo sabes que la propiedad que verificaste es realmente la que querías?".

¿Cuándo deja de funcionar el vibe coding?

El término vibe coding lo acuñó Andrej Karpathy en febrero de 2025, y Collins English Dictionary lo eligió palabra del año. Karpathy lo pensó como un proyecto de fin de semana: pulsar "Aceptar todo" sin mirar los diffs. Un año después, el propio Karpathy lo sustituyó por agentic engineering, una práctica donde el desarrollador dirige y supervisa al agente en vez de aceptar lo que produzca, según Unite AI.

Los datos de adopción ya son masivos. El Stack Overflow 2025 Developer Survey, con 49.000 desarrolladores de 177 países, encontró que más del 80% usa herramientas de IA en su flujo y el 51% lo hace a diario. El informe DORA 2025 de Google cifra la adopción en 90%, pero también registra que cerca de un tercio confía poco o nada en lo que la IA genera. Y según el paper "Vibe Coding Kills Open Source" (Koren, Békés, Hinz y Lohmann, arXiv 2601.15494v1, enero de 2026), a una adopción del 70% la monetización por usuario en proyectos open source cae un 70%, mientras las ganancias de productividad solo compensan un 12% de los costes de mantenimiento — TechTarget.

Los fallos de seguridad documentados respaldan la preocupación. La app Tea, orientada a seguridad de mujeres en citas, expuso decenas de miles de fotos de ID y más de un millón de mensajes privados por un bucket de almacenamiento sin protección. Una app construida sobre Lovable tenía la lógica de autorización invertida: bloqueaba a usuarios autenticados y dejaba entrar a atacantes anónimos, afectando a más de 18.000 usuarios — Unite AI. Gartner, a través de su jefe de investigación de ciberseguridad Pete Shoard, sitúa al vibe coding como el principal riesgo de seguridad empresarial del momento, sobre todo por secretos hardcodeados que se filtran a repositorios públicos al sincronizar.

Un estudio de las universidades Massey y Auckland cifra en 62% la motivación principal para hacer vibe coding: velocidad y eficiencia — Computerworld. Eso, dicen los investigadores, es exactamente el entorno donde los errores lógicos y de seguridad pasan desapercibidos hasta que explotan en producción.

Qué significa esto para tu startup

La historia de Bend 2 no va solo de un lenguaje experimental. Va de cómo usas la IA en tu equipo de ingeniería sin terminar pagando el coste doble de reescribir lo que ya existía o de saltarte la investigación previa. Tres acciones concretas:

Antes de pedirle a un LLM que construya algo, pregúntale qué campo lo estudia. Un buen prompt inicial es: "¿Cuál es el estándar actual y qué herramientas maduras existen para este problema?" Si la IA no nombra ninguna alternativa, busca tú antes de aceptar la primera implementación. El caso Bend lo demuestra: la respuesta (SPARK, LEAN) ya estaba ahí.
Aplica la regla de Simon Willison: no subas código que no puedas explicar a otra persona. No necesitas leer cada línea, sí entender la lógica central y poder justificar por qué hace lo que hace. Esto filtra tanto el vibe coding puro como el código inseguro que ya hemos visto filtrar millones de datos.
Audita con checkers formales o tests de contrato en código crítico. Para código que toca autenticación, pagos o datos sensibles, integra herramientas de análisis estático (linters de seguridad, type checkers estrictos, pruebas con SPARK/LEAN o equivalentes) y un gate de revisión humana antes de mergear. El coste de añadir esta capa es bajo comparado con el coste de un incidente: el paper arXiv estima que, sin contributors al ecosistema open source, los modelos de negocio actuales del software no son sostenibles al 70% de adopción de vibe coding.

Conclusión

La IA generativa te da velocidad. Pero la velocidad sin contexto produce el patrón Bend: código funcional que reinventa un campo entero porque nadie — ni humano ni máquina — se paró a investigar qué existía ya. La lección para founders es incómoda pero simple: usar IA para construir no te exime de saber qué estás construyendo, ni de auditarlo. Las herramientas de verificación formal llevan décadas madurando; descubrirlas tarde puede costarte tu próxima crisis de seguridad o un trimestre perdido rehaciendo el producto.