La IA transforma la verificación formal de software para mejorar la seguridad

Las startups &Truth, Harmonic y Theorem están utilizando inteligencia artificial para hacer viable la verificación formal de software, un proceso tradicionalmente laborioso que busca garantizar la ausencia de errores en el código. &Truth, lanzada recientemente, ha invertido 70 millones de dólares para verificar el código de cifrado de la aplicación de mensajería Signal, mientras que Harmonic, cofundada por Vlad Tenev, ha recaudado 295 millones y evalúa su agente de IA, Aristotle, con fabricantes de chips como Nvidia. Recientemente, Anthropic y Theorem anunciaron el uso de IA para detectar vulnerabilidades en software de código abierto que miles de pruebas habían pasado por alto. Aunque la tecnología está en fase de prototipado y su adopción masiva sigue siendo incierta, la verificación formal ya se utiliza en sistemas críticos como los aviones de Boeing, los servidores de Amazon y los dispositivos Apple. Expertos como Vitalik Buterin y Will Wilson advierten que la IA no es una solución mágica y que la verificación formal puede ser costosa y lenta, pero la industria busca automatizar el proceso para integrar la seguridad en el desarrollo de software generado por IA.