&Truth capta US$ 70 milhões em rodada-semente para criar uma máquina universal de verificação de código

A &Truth, uma corporação de benefício público que desenvolve tecnologia para provar matematicamente que o software é seguro, saiu do modo sigiloso em 29 de outubro de 2026, divulgando um financiamento-semente de US$ 70 milhões e o plano de criar o que chama de máquina universal de verificação de código.

Em seu anúncio de lançamento, a empresa afirmou que foi fundada no início de 2026 e recebeu US$ 70 milhões em capital-semente de um grupo que descreveu como formado por líderes pioneiros em segurança de IA e capital de risco. A empresa disse que está desenvolvendo sua máquina de verificação para ler código em qualquer linguagem de programação e provar matematicamente que ele é seguro, protegido e correto, com provas que qualquer pessoa pode verificar de forma independente.

Automação de provas baseada em Lean

A verificação formal existe há décadas, mas antes era inacessível e cara, segundo o anúncio, porque especialistas precisavam formular as provas manualmente, o que restringia a prática a um punhado de sistemas críticos. A empresa afirmou que a IA agora acelera o trabalho com provas formais em 100 vezes ou mais e que sua tecnologia de automação de provas acelera o processo em outras 100 vezes, reduzindo o tempo de geração de provas de anos ou meses para horas ou minutos.

A empresa também descreveu a tecnologia que chama de «fábrica de especificações», que, segundo ela, permite que empresas e desenvolvedores convertam a intenção humana e os requisitos de negócio em especificações formais precisas em grande escala, gerando garantias que podem ser verificadas de forma independente, em vez de depender de testes ou de alegações dos fornecedores.

A &Truth está desenvolvendo sua tecnologia com base em Lean, um sistema de provas de código aberto, e Mathlib, uma biblioteca com mais de dois milhões de linhas de definições e teoremas matemáticos, além de tecnologias de código aberto como CSLib. Segundo a empresa, o objetivo é criar um vocabulário formal universal para o software: modelos matemáticos de linguagens de programação e sistemas, técnicas de prova e especificações precisas que permitam a verificação automatizada em diferentes linguagens. A &Truth afirmou que trabalha com a Lean Focused Research Organization e pretende disponibilizar suas bibliotecas fundamentais como código aberto.

O cofundador e codiretor-executivo Clark Barrett afirmou que Lean e Mathlib deram à IA uma linguagem precisa para raciocinar em matemática e que faltava ao software uma base equivalente. O cofundador e diretor científico Ilya Sergey disse que a confiança no software deve se apoiar em provas que possam ser verificadas de forma independente, e não na palavra de qualquer empresa.

Fundadores e sedes em dois países

Barrett é professor Corbel de ciência da computação na Stanford University, codiretor fundador do Stanford Center for AI Safety, diretor do Stanford Center for Automated Reasoning, cocriador da CSLib e líder do projeto do mecanismo de raciocínio automatizado cvc5. Sergey fundou o VERSE Lab na National University of Singapore e cocriou os verificadores de código aberto Veil e Velvet. O cofundador, codiretor-executivo e presidente executivo Chris Hsu integra o conselho consultivo estratégico da Lean FRO e é presidente da Infinitude Foundation; anteriormente, foi CEO da Kilometre Capital e diretor-gerente do Citadel Investment Group.

O anúncio também citou Gregory Malecha, que anteriormente liderou a área de métodos formais na BlueRock Security e foi um dos principais arquitetos da estrutura de verificação BRiCk; Sebastian Ullrich, coarquiteto do Lean 4 e cofundador da Lean Focused Research Organization; Linus Lee, ex-sócio-gerente da Kilometre Capital; e Drew Harman, ex-diretor comercial da Fastino Labs e sócio operacional da Insight Partners e da Shasta Ventures. A &Truth afirmou que seu trabalho se apoia em décadas de pesquisa em verificação formal e raciocínio automatizado na Stanford University e na National University of Singapore.

A sede da &Truth nos Estados Unidos fica em Palo Alto, e sua sede internacional fica em Singapura, onde, segundo a empresa, o escritório será ampliado significativamente nas áreas de pesquisa, engenharia, produto e comercialização. Low Jin Yong, vice-presidente sênior e codiretor da Digital Industry Singapore, afirmou no anúncio que a sede aprofundará as capacidades de confiança e segurança em Singapura e fortalecerá o país como base para empresas que desenvolvem IA confiável.

O site da empresa também apresenta uma mesa-redonda com Leonardo de Moura, inventor de Lean e vice-presidente e cientista ilustre da AWS, e Simone Severini, integrante do conselho consultivo estratégico da Lean FRO e engenheira ilustre do Google.

Ensaios complementares explicam os argumentos da empresa

Em um ensaio complementar datado de 29 de outubro de 2026, Hsu detalhou as tendências que, segundo a empresa, tornam urgente a verificação. Ele citou declarações do CEO do Google, Sundar Pichai, segundo as quais 75% do novo código do Google agora é gerado por IA e aprovado por engenheiros, e os testes da Veracode de 2026, que constataram que os modelos de IA falharam em quase metade das tarefas de programação em que a segurança era importante. O ensaio também cita uma campanha de setembro de 2026 na qual um invasor implantou centenas de agentes de IA para invadir 395 organizações em 48 países por meio de falhas em um software de gerenciamento de impressão amplamente utilizado, além do número recorde de 14.959 vulnerabilidades de software publicadas em setembro de 2026, que, segundo o ensaio, corresponde a 3,5 vezes o total publicado um ano antes.

O ensaio relembra marcos anteriores da verificação formal: a prova original do microkernel seL4 exigiu cerca de 20 anos-pessoa de trabalho especializado para aproximadamente 8.700 linhas de código; em 2015, no âmbito do programa HACMS da DARPA, o seL4 foi integrado ao helicóptero Unmanned Little Bird da Boeing, cujos controles de voo uma equipe profissional de especialistas em segurança, com semanas de acesso, não conseguiu violar; e, em setembro de 2026, um modelo de IA desenvolvido pela Anthropic formalizou em Lean a prova completa do Último Teorema de Fermat em 11 dias. O ensaio também observa que, no início de 2026, Kim Morrison, engenheiro sênior de software de pesquisa na Lean FRO, usou o Claude, da Anthropic, com orientação humana mínima para criar uma versão em Lean da biblioteca de compressão zlib e provar que ela sempre restaura exatamente os dados que comprimiu.

O ensaio cita o criador do Lean, Leonardo de Moura: «Os testes geram confiança. A prova oferece uma garantia.»

Em um segundo ensaio, publicado em 29 de outubro de 2026, Sergey explica os mecanismos da verificação de programas, começando pelo artigo de Alan Turing de 1949, «Checking a Large Routine», que propunha que os programadores acompanhassem o código de afirmações precisas, que um verificador pudesse checar individualmente. O ensaio descreve especificações, invariantes de laço e provas verificadas em Lean, e afirma que o objetivo da &Truth é permitir que os desenvolvedores obtenham evidências verificáveis de forma independente, como uma prova formal em Lean, a um custo que torne a verificação uma etapa rotineira do desenvolvimento.

A &Truth descreve sua visão de longo prazo como uma transição da «programação por intuição» para a «programação verificável», na qual o código gerado por IA é verificado matematicamente antes da implantação, os agentes de IA operam em ambientes cujo confinamento pode ser comprovado, os sistemas legados são modernizados com segurança e a infraestrutura crítica é protegida por garantias matemáticas verificáveis de forma independente.