O potencial da IA para revolucionar a verificação de software desperta interesse na indústria

Pesquisadores da Universidade de Stanford, liderados por Chuyue Sun, desenvolveram uma ferramenta de IA que completou um projeto de engenharia em menos de meio dia, por menos de 500 dólares, em comparação com cinco meses de trabalho de especialistas humanos. Esta descoberta, detalhada em um artigo recente, está a despertar interesse na verificação formal, um campo especializado de codificação e matemática. A startup Truth, fundada por Sun, foi lançada esta semana e tem como objetivo verificar qualquer linguagem de programação. Empresas como Harmonic e Anthropic também estão a desenvolver ferramentas de verificação baseadas em IA. Líderes da indústria, como Ilya Sergey, argumentam que a verificação formal, semelhante a provas matemáticas em engenharia, é essencial para a fiabilidade do software. No entanto, ainda existe ceticismo, com especialistas como Will Wilson a considerá-la uma 'armadilha' para entusiastas da matemática. Apesar do seu potencial, a adoção é limitada pelos custos, pela falta de experiência e pelas preocupações com a possível lentidão da inovação. Projetos de código aberto e startups estão a experimentar a verificação assistida por IA, enquanto empresas como Boeing e Apple revelam o uso de código verificado formalmente em sistemas críticos. No entanto, muitas empresas permanecem cautelosas, destacando a necessidade de financiamento sustentável e de confiança nas especificações geradas por IA.