Google aplica IA à verificação formal do Signal
Em 10 de novembro de 2026, o Google DeepMind apresentou o AlphaProof Code, uma estrutura de agentes de IA e revisão humana para verificar formalmente propriedades de software complexo.
- Combina especificações revisadas por especialistas, agentes e verificação de provas em Lean.
- O projeto analisou propriedades de segurança selecionadas do código do Signal e incluiu um teste com falhas conhecidas.
- Fonte e data: Google DeepMind, 10 de novembro de 2026; os resultados são da equipe responsável.
Contexto e análise do Noosigma AI
Resumo e contextualização editorial elaborados a partir da fonte indicada. Alegações e resultados atribuídos à organização são relatos da própria fonte; não representam validação independente do Noosigma AI.
No trabalho sobre o protocolo Signal, especialistas definiram propriedades de segurança que deveriam ser provadas e revisaram as especificações matemáticas. Agentes apoiados pelo Gemini Carbon produziram provas em Lean para partes do código real; o verificador da linguagem checa mecanicamente cada prova.
O que isso muda
A equipe informa que a produção ultrapassou seis milhões de linhas de Lean e levou quatro semanas. O sistema também destacou uma pequena parte para inspeção humana. Em um teste controlado, os pesquisadores reinseriram duas falhas corrigidas em uma cópia isolada e relatam que a abordagem as identificou.
O resultado trata das propriedades escolhidas e formalizadas pelos pesquisadores, não de uma garantia de que todo o protocolo ou todos os defeitos estejam cobertos. A descrição e a alegação de prioridade histórica vêm dos autores e de seus parceiros. Fonte e data: Google DeepMind, 10 de novembro de 2026.