À medida que a inteligência artificial remodela o desenvolvimento de software, uma pequena startup aposta que o próximo grande gargalo da indústria não será escrever código – será confiar nele.
Teoremauma empresa com sede em São Francisco que surgiu da Y Combinator Primavera de 2025 lote, anunciou na terça-feira que levantou US$ 6 milhões em financiamento inicial para construir ferramentas automatizadas que verificam a exatidão do software gerado por IA. Khosla Ventures liderou a rodada, com a participação de Combinador Y, e14, SAIF, Halcyone investidores anjos, incluindo Blake Borgesson, cofundador da Recursion Pharmaceuticals, e Arthur Breitman, cofundador da plataforma blockchain Tezos.
O investimento chega num momento crucial. Assistentes de codificação de IA de empresas como GitHub, Amazôniae Google agora geram bilhões de linhas de código anualmente. A adoção empresarial está se acelerando. Mas a capacidade de verificar se o software escrito por IA realmente funciona como pretendido não acompanhou o ritmo – criando o que os fundadores do Teorema descrevem como uma expansão cada vez maior. "lacuna de supervisão" que ameaça infra-estruturas críticas, desde sistemas financeiros até redes eléctricas.
"Já estamos lá," disse Jason Gross, cofundador do Theorem, quando perguntamos se o código gerado por IA está ultrapassando a capacidade de revisão humana. "Se você me pedisse para revisar 60.000 linhas de código, eu não saberia como fazer."
Por que a IA está escrevendo código mais rápido do que os humanos conseguem verificá-lo
A tecnologia central do Teorema combina verificação formal – uma técnica matemática que prova que o software se comporta exatamente conforme especificado – com modelos de IA treinados para gerar e verificar provas automaticamente. A abordagem transforma um processo que historicamente exigia anos de engenharia em nível de doutorado em algo que a empresa afirma poder ser concluído em semanas ou até dias.
A verificação formal existe há décadas, mas permaneceu confinada às aplicações mais críticas: sistemas aviônicos, controles de reatores nucleares e protocolos criptográficos. O custo proibitivo da técnica – muitas vezes exigindo oito linhas de prova matemática para cada linha de código – tornou-a impraticável para o desenvolvimento de software convencional.
Gross sabe disso em primeira mão. Antes de fundar a Theorem, ele obteve seu doutorado no MIT trabalhando em código de criptografia que agora alimenta o protocolo de segurança HTTPS protegendo trilhões de conexões de internet diariamente. Esse projeto, segundo sua estimativa, consumiu quinze pessoas-ano de trabalho.
"Ninguém prefere ter código incorreto," disse Gross. "A verificação de software simplesmente não era econômica antes. As provas costumavam ser escritas por engenheiros com nível de doutorado. Agora, a IA escreve tudo isso."
Como a verificação formal detecta os bugs que os testes tradicionais não percebem
O sistema do teorema opera segundo um princípio que Gross chama "decomposição de prova fracionária." Em vez de testar exaustivamente todos os comportamentos possíveis – computacionalmente inviáveis para softwares complexos – a tecnologia aloca recursos de verificação proporcionalmente à importância de cada componente do código.
A abordagem identificou recentemente um bug que passou despercebido nos testes da Anthropic, a empresa de segurança de IA por trás do chatbot Claude. Gross disse que a técnica ajuda os desenvolvedores "detecte seus bugs agora sem gastar muito esforço computacional."
Em uma demonstração técnica recente chamada SFBench, o Teorema usou IA para traduzir 1.276 problemas de Rocq (um assistente de prova formal) para Lean (outra linguagem de verificação), depois provou automaticamente cada tradução equivalente ao original. A empresa estima que uma equipe humana precisaria de aproximadamente 2,7 pessoas-ano para concluir o mesmo trabalho.
"Todos podem executar agentes em paralelo, mas também podemos executá-los sequencialmente," Gross explicou, observando que a arquitetura do Teorema lida com código interdependente – onde as soluções se baseiam em dezenas de arquivos – que tropeçam nos agentes convencionais de codificação de IA limitados por janelas de contexto.
Como uma empresa transformou uma especificação de 1.500 páginas em 16.000 linhas de código confiável
A startup já está trabalhando com clientes em laboratórios de pesquisa de IA, automação de projetos eletrônicos e computação acelerada por GPU. Um estudo de caso ilustra o valor prático da tecnologia.
Um cliente chegou ao Theorem com uma especificação em PDF de 1.500 páginas e uma implementação de software legado atormentada por vazamentos de memória, travamentos e outros bugs indescritíveis. O problema mais urgente: melhorar o desempenho de 10 megabits por segundo para 1 gigabit por segundo — um aumento de 100 vezes — sem introduzir erros adicionais.
O sistema da Theorem gerou 16.000 linhas de código de produção, que o cliente implantou sem nunca revisá-lo manualmente. A confiança veio de uma especificação executável compacta – algumas centenas de linhas que generalizavam o enorme documento PDF – combinada com um equipamento de verificação de equivalência que verificava se a nova implementação correspondia ao comportamento pretendido.
"Agora eles têm um analisador de nível de produção operando a 1 Gbps que podem implantar com a confiança de que nenhuma informação será perdida durante a análise," disse Gross.
Os riscos de segurança ocultos no software gerado por IA para infraestruturas críticas
O anúncio de financiamento chega num momento em que os decisores políticos e os tecnólogos examinam cada vez mais a fiabilidade dos sistemas de IA incorporados em infraestruturas críticas. O software já controla os mercados financeiros, os dispositivos médicos, as redes de transporte e as redes elétricas. A IA está acelerando a rapidez com que o software evolui – e a facilidade com que bugs sutis podem se propagar.
Gross enquadra o desafio em termos de segurança. À medida que a IA torna mais barato encontrar e explorar vulnerabilidades, os defensores precisam do que ele chama "defesa assimétrica" — proteção que aumenta sem aumentos proporcionais de recursos.
"A segurança de software é um delicado equilíbrio entre ataque e defesa," ele disse. "Com o hacking de IA, o custo de hackear um sistema está caindo drasticamente. A única solução viável é a defesa assimétrica. Se quisermos uma solução de segurança de software que possa durar mais do que algumas gerações de melhorias no modelo, será por meio de verificação."
Questionado se os reguladores deveriam exigir a verificação formal do código gerado por IA em sistemas críticos, Gross ofereceu uma resposta incisiva: "Agora que a verificação formal é suficientemente barata, pode ser considerado negligência grave não utilizá-la para garantias sobre sistemas críticos."
O que separa o Teorema de outras startups de verificação de código de IA
A Theorem entra em um mercado onde inúmeras startups e laboratórios de pesquisa estão explorando a interseção entre IA e verificação formal. A diferenciação da empresa, argumenta Gross, reside no seu foco singular em dimensionar a supervisão de software, em vez de aplicar a verificação à matemática ou a outros domínios.
"Nossas ferramentas são úteis para equipes de engenharia de sistemas, que trabalham próximo ao metal, que precisam de garantias de correção antes de mesclar alterações," ele disse.
A equipe fundadora reflete essa orientação técnica. Gross traz profundo conhecimento em teoria de linguagens de programação e um histórico de implantação de código verificado em produção em grande escala. O cofundador Rajashree Agrawal, engenheiro de pesquisa de aprendizado de máquina, concentra-se no treinamento dos modelos de IA que alimentam o pipeline de verificação.
"Estamos trabalhando no raciocínio formal do programa para que todos possam supervisionar não apenas o trabalho de uma IA média de nível de engenheiro de software, mas realmente aproveitar os recursos de uma IA de nível Linus Torvalds," Agrawal disse, referindo-se ao lendário criador do Linux.
A corrida para verificar o código da IA antes que ele controle tudo
Teorema planeja usar o financiamento para expandir sua equipe, aumentar os recursos computacionais para treinar modelos de verificação e entrar em novos setores, incluindo robótica, energia renovável, criptomoeda e síntese de medicamentos. A empresa emprega atualmente quatro pessoas.
O surgimento da startup sinaliza uma mudança na forma como os líderes de tecnologia empresarial podem precisar avaliar as ferramentas de codificação de IA. A primeira onda de desenvolvimento assistido por IA prometia ganhos de produtividade – mais código, mais rápido. O teorema aposta que a próxima onda exigirá algo diferente: prova matemática de que a velocidade não vem à custa da segurança.
Gross enquadra o que está em jogo em termos rígidos. Os sistemas de IA estão melhorando exponencialmente. Se essa trajetória se mantiver, ele acredita que a engenharia de software sobre-humana é inevitável – capaz de projetar sistemas mais complexos do que qualquer coisa que os humanos já construíram.
"E sem uma economia de supervisão radicalmente diferente," ele disse, "acabaremos implantando sistemas que não controlamos."
As máquinas estão escrevendo o código. Agora alguém tem que verificar seu trabalho.
