Google DeepMind verifica formalmente o código do protocolo da Signal com agentes de IA

A verificação formal, que demonstra matematicamente que o código funciona sem falhas, é o nível mais alto de garantia de segurança, mas dá muito trabalho. Segundo a empresa, é a primeira vez que a implementação de um protocolo deste tipo, amplamente usado, é verificada formalmente, com ou sem IA.

Peritos humanos reviram todas as especificações de segurança. Depois, agentes baseados no Gemini Carbon geraram milhões de linhas de Lean e assinalaram para revisão humana apenas um por cento do código. A empresa diz que o processo demorou semanas, numa tarefa que costuma ocupar equipas especializadas durante anos.

Para testar o sistema, a equipa reintroduziu erros reais, já corrigidos, numa versão isolada do código da Signal. Em ambos os casos, o sistema produziu uma prova de que essa versão era insegura. Os artefactos da verificação passam a estar em código aberto.

Fonte: Google DeepMind — Introducing AlphaProof Code: a breakthrough in verifying complex software at depth