Testar não é provar: o que o DeepMind verificou no Signal

Testar mostra que deu certo onde você olhou; provar cobre tudo o que a regra permite

Imagine, como exemplo hipotético, uma loja virtual com uma função que calcula o preço final depois de um desconto. A regra de negócio é simples: o preço final nunca é negativo e nunca passa do preço original.

Você escreve testes. Preço 100 com desconto de 10%. Preço 0 com desconto de 50%. Preço 59,90 sem desconto. Todos passam. Mas existe um cupom de 120% que ninguém testou, e com ele o preço sai negativo. O teste não errou. Ele só não olhou ali.

É isso que um teste é: uma amostra. Ele pode encontrar defeitos, mas não pode garantir que não existem outros. Uma prova formal funciona de outro jeito. Ela parte de uma regra escrita com precisão (a especificação) e demonstra, por argumento lógico conferido por programa, que o código cumpre a regra para qualquer entrada permitida. Se o cupom de 120% é possível, a prova não fecha, e o defeito aparece.

Resumindo o contraste: teste procura falhas nos casos escolhidos; prova mostra ausência de falhas em relação a uma regra, para todos os casos.

No método descrito, a IA ajuda a escrever as regras e outro passo confere o código contra elas

Especificação é a descrição exata do que o código deve fazer, escrita em linguagem matemática. Escrevê-la sempre foi a parte cara da verificação formal, porque exige gente que entenda o sistema e a lógica ao mesmo tempo.

O ângulo do anúncio é este: agentes de IA ajudam a produzir essas especificações, e um passo separado prova que o código cumpre cada uma. As fontes que usei não detalham as ferramentas por dentro, então não vou descrever o mecanismo além disso.

Há uma consequência que vale registrar, e ela é inferência minha, não afirmação das fontes. Se a conferência da prova é um passo à parte, a prova aceita vale independentemente de quem escreveu a regra. Mas a regra em si continua precisando de olhos humanos. Uma IA pode escrever uma especificação plausível e incompleta. Nesse caso a prova fecha, e fecha sobre algo que não era exatamente o que você queria garantir.

Na aviação existe uma ideia parecida: o checklist só protege se tiver os itens certos. Conferir item por item não ajuda se faltou um item.

As quatro semanas são um número do DeepMind e não dizem tudo sobre o ganho

O que as reportagens relatam: o DeepMind diz que verificou o núcleo criptográfico do Signal em quatro semanas, no código compilado, e que um trabalho desse tipo antes levava anos. Ele também publicou os artefatos no GitHub.

O que esse número não prova. Não sabemos, pelas fontes, quem fez a comparação, com que equipe, sobre qual escopo nem contra qual projeto anterior. "Anos" é uma ordem de grandeza, não uma medida. Por isso eu trataria as quatro semanas como uma alegação interessante, que ganha peso quando alguém de fora reproduz ou revisa o trabalho.

Sobre o código compilado, a ideia geral é a seguinte. O que roda no seu celular é o resultado da compilação, não o texto que o programador escreveu. Provar propriedades do texto-fonte obriga você a confiar que o compilador não introduziu nada de errado. Provar sobre o código compilado, em princípio, reduz o que precisa ser aceito na confiança. É uma propriedade geral da abordagem, não um detalhe que eu possa atribuir ao método do DeepMind além do que foi relatado.

A prova só vale para o que foi especificado, e o escopo foi o núcleo, não o app inteiro

Este é o limite central. Uma prova formal garante que o código cumpre as propriedades escritas na especificação. Nada além disso. Se uma propriedade importante não foi escrita, ela não está coberta, mesmo que o código passe em tudo o que foi pedido.

O segundo limite é de escopo. Segundo as reportagens, o DeepMind verificou o núcleo criptográfico do Signal, a parte que lida com a cifragem. Isso não é o aplicativo inteiro. Interface, armazenamento no aparelho, sincronização, notificações e o sistema em que o app roda ficam fora dessa conclusão.

Então a leitura honesta do resultado é estreita. Para as propriedades especificadas, no núcleo verificado, existe uma prova conferível. Daí não se segue que o Signal esteja livre de falhas, nem que as conversas sejam inquebráveis em qualquer circunstância. Nenhuma das fontes diz isso, e eu também não digo.

O que muda na prática e como conferir por conta própria

O que muda na prática: quando alguém disser que um software foi "verificado", faça duas perguntas. Verificado contra quais propriedades? E em qual parte do sistema? Sem essas duas respostas, a palavra não informa quase nada. E o fato de os artefatos estarem públicos permite justamente esse tipo de pergunta: quem tem conhecimento pode ler o que foi especificado em vez de confiar na manchete.

Teste você mesmo: pegue uma função do seu trabalho, de uma planilha ou de um sistema que você use. Escreva em uma frase uma propriedade que deve valer sempre, como "o total nunca é negativo". Depois tente listar todas as entradas possíveis. Se a lista não fecha, você acabou de ver a diferença entre testar e provar. Se quiser ir além, leia as duas reportagens e procure os artefatos no GitHub para ver como as propriedades do Signal foram escritas.

Se quiser seguir nesse caminho de entender IA aplicada a problemas técnicos sem hype, os materiais gratuitos estão em /materiais. É só um convite.

— @mvellas.ai