Pesquisadores e cientistas da computação estão voltando suas atenções para uma área pouco explorada da programação e da matemática conhecida como verificação formal. A técnica consiste em utilizar fórmulas matemáticas para provar que um software está livre de erros. Tradicionalmente, o processo é longo, trabalhoso e exige que engenheiros convertam códigos e objetivos em declarações precisas. No entanto, avanços recentes indicam que a inteligência artificial pode tornar essa prática mais rápida e viável.
Segundo a pesquisadora Chuyue Sun, da Universidade de Stanford, uma ferramenta de IA desenvolvida por ela e outros cientistas concluiu um projeto de engenharia em menos de meio dia e por um custo inferior a 500 dólares. O mesmo trabalho havia consumido cinco meses de três especialistas humanos quando realizado manualmente. Sun utilizou a tecnologia para verificar parte do código de criptografia do aplicativo de mensagens Signal.
O potencial da tecnologia tem impulsionado o surgimento de novas empresas. A startup &Truth, que conta com a participação de Sun e levantou 70 milhões de dólares em investimentos, tem como objetivo viabilizar a verificação formal de qualquer linguagem de programação. Outro exemplo é a Harmonic, cofundada pelo CEO da Robinhood, Vlad Tenev, que recebeu 295 milhões de dólares e anunciou suporte para verificar softwares em C e projetos de hardware com grandes empresas do setor, como Nvidia e Tensordyne.
A Anthropic e a startup Theorem também anunciaram recentemente o uso de inteligência artificial para detectar falhas em códigos de código aberto que testes convencionais não haviam conseguido identificar. Além disso, a Anthropic introduziu um complemento na ferramenta Claude para auxiliar desenvolvedores no processo.
Apesar do entusiasmo e do uso já consolidado de softwares verificados em setores críticos — como em servidores da Amazon, aeronaves da Boeing e dispositivos Apple —, especialistas mantêm cautela sobre a expansão em massa da tecnologia. Críticos apontam que a verificação formal ainda está em estágio de prototipagem, pode gerar custos elevados e nem sempre captura falhas decorrentes de erros humanos ou de hardware. Para Will Wilson, fundador da Antithesis, a verificação formal isoladamente não substitui testes exaustivos e robustos.
Empresas de tecnologia de médio porte também citam desafios como a escassez de engenheiros especializados e o risco de que a lentidão no processo acabe atrasando a inovação de seus produtos. Ainda assim, defensores da abordagem acreditam que a automação por IA na verificação matemática será uma defesa essencial contra ciberataques impulsionados por sistemas automatizados no futuro.
Fonte: The ‘Pain in the Ass’ Math That Could Save Vibe Coding From Itself
