Verificação formal com IA

Em 2024, pesquisadores da Google DeepMind utilizaram inteligência artificial para gerar a primeira prova formal de segurança das mensagens do aplicativo Signal, conforme relatório técnico divulgado pela empresa.

Desafio da Beneficial AI Foundation

A equipe respondeu a um desafio lançado pela Beneficial AI Foundation em abril de 2024, transformando metas de segurança em especificações matemáticas revisadas por humanos e usando o AlphaProof Code para produzir milhões de linhas de código em Lean que testam a correção do software.

Colaboração humano‑máquina

Segundo Swat Chaudhuri, pesquisador da Google DeepMind e professor da Universidade do Texas, citado pelo The Register, a verificação formal historicamente exigia esforço humano intenso; a IA permitiu escalar o processo, mudando o foco da dificuldade para a escolha do que será verificado.

Defesas pós‑quânticas

O Signal incorporou o Sparse Post Quantum Ratchet (SPQR) ao seu sistema Triple Ratchet, combinando chaves tradicionais e pós‑quânticas para reforçar a proteção de dados diante de ameaças de computadores quânticos.

Com o AlphaProof Code, a verificação foi integrada ao fluxo de desenvolvimento no GitHub, reduzindo prazos e custos operacionais em comparação com métodos anteriores que dependiam exclusivamente de revisão manual.