Novas ferramentas de IA podem revolucionar a verificação formal de software. Startups como &Truth e Harmonic estão desenvolvendo ferramentas de IA para automatizar a verificação formal de software, reduzindo custos e tempo.

A pesquisa da Stanford, liderada por Chuyue Sun, demonstrou que a verificação formal de software pode ser realizada em menos de um dia por menos de US$ 500, comparado a cinco meses de trabalho manual por três engenheiros experientes.

&Truth, uma das startups envolvidas, já recebeu investimentos de US$ 70 milhões e está planejando verificar qualquer linguagem de programação. A rival Harmonic, cofundada pelo CEO de Robinhood, Vlad Tenev, também está investindo em soluções matemáticas para a verificação de software.

Embora haja potencial para melhorar a confiabilidade e segurança dos sistemas de software, ainda há dúvidas sobre a adesão generalizada dessas tecnologias. O processo de verificação formal depende de várias suposições sobre como computadores e humanos interagem com o software, levantando questionamentos sobre sua eficácia em detectar erros relacionados ao uso do software e falhas de hardware.