Victor Taelin lança o Bend 2, linguagem que usa verificação de provas para barrar erros de IA

O desenvolvedor brasileiro reformulou o Bend. A promessa é checar mecanicamente o que o código gerado por IA faz.

O desenvolvedor brasileiro Victor Taelin anunciou o Bend 2, nova versão da linguagem Bend. Segundo o anúncio dele no X, a linguagem bloqueia erros de IA por meio de verificação de provas (proof checking), a mesma técnica que grandes laboratórios de IA usaram para resolver problemas matemáticos em aberto. O projeto está no repositório bendlang/bend, no GitHub.

Segundo o site do projeto, o verificador de tipos do Bend funciona como um verificador de provas, como os de Lean e Rocq, que podem levar minutos em projetos de tamanho médio. O Bend promete fazer isso em até um segundo, para que um agente de IA possa usá-lo em ciclos rápidos. A ideia é que as provas permitam conferir mecanicamente se a IA implementou o que foi pedido, e que um compilador rápido execute esse código com alto desempenho.

A primeira versão do Bend, lançada em 2024, ficou conhecida por usar threads de CPU e GPU para executar operações em paralelo.

Ponto de atenção

Esses são os objetivos declarados pelo autor e pelo projeto. Não encontramos avaliação independente do desempenho nem da eficácia contra erros de IA, e há discussão na comunidade sobre os limites da abordagem.

Contexto

O anúncio é de setembro de 2026.