Broken by Default: A Formal Verification Study of Security Vulnerabilities in AI-Generated Code
El estudio "Broken by Default" demuestra mediante verificación formal con el solver Z3 que el 55,8% del código generado por siete modelos de IA líderes contiene vulnerabilidades de seguridad matemáticamente probadas, revelando que las herramientas actuales de la industria pasan por casi el 98% de estos fallos y que las instrucciones de seguridad explícitas apenas reducen la tasa de errores.