# Código e Sinal AlphaProof: provas de segurança de código de máquina verificadas e suposições confiáveis

Published: 2026-11-11

Google DeepMind relata provas verificadas por máquina de propriedades de segurança selecionadas para um "harness" de linha de comando libsignal compilado. O Lean verifica a prova, enquanto os humanos aprovam a especificação e suas suposições. Um comparador separado verifica o teorema e todas as definições dependentes em relação ao alvo aprovado.

Canonical: https://thedailydiff.dev/pt-BR/video/2026-11-10-signal-machine-proof/

## O que este vídeo aborda

- Agentes de IA produzem provas candidatas; o kernel do Lean verifica se elas estabelecem a reivindicação formal aprovada por humanos.
- O alvo verificado é um "harness" CLI libsignal compilado específico, com semântica e contratos criptográficos confiáveis.
- Provar o binário compilado remove o compilador Rust da base confiável para as propriedades declaradas desse binário.
- Os pesquisadores relatam duas reintroduções isoladas de bugs previamente corrigidos que violam seu teorema de segurança simbólico.
- O comparador verifica o teorema e cada definição dependente em relação a uma especificação aprovada protegida; as emendas passam por um processo revisado separado.

## Perguntas e respostas

### O que o AlphaProof Code provou sobre a implementação do Signal?

O Google DeepMind relata provas verificadas de propriedades de segurança selecionadas para um "harness" de linha de comando libsignal compilado. O artigo técnico abrange confidencialidade e autenticação de mensagens, com sigilo de encaminhamento e segurança pós-comprometimento sob modelos declarados. O resultado mantém condições sobre o atacante, sessão e suposições criptográficas. Seu escopo exclui uma garantia geral para cada aplicativo ou instalação do Signal.

### Quem decide o que uma prova de segurança gerada por IA deve estabelecer?

Revisores humanos aprovam a especificação e suas suposições. O artigo técnico do Google DeepMind descreve agentes elaborando especificações com orientação humana e revisores testando se as declarações capturam propriedades de segurança significativas. O Lean verifica a lógica da prova resultante. Os humanos permanecem responsáveis por escolher um alvo forte, revisar suposições e julgar as alterações propostas na especificação aprovada.

### Por que verificar o código de máquina compilado em vez de confiar no compilador Rust?

Uma prova sobre o binário compilado estabelece as propriedades declaradas para esse artefato diretamente. O artigo do Google DeepMind explica que um erro do compilador que violasse uma dessas propriedades tornaria o teorema falso. O compilador Rust, portanto, sai da base confiável para esta reivindicação. A prova ainda confia no modelo de instrução, no kernel do Lean e nos contratos criptográficos especificados.

### Como o comparador impede que um agente de prova enfraqueça seu alvo?

O comparador verifica o teorema e todas as definições das quais ele depende em relação a uma especificação aprovada protegida. O artigo do Google DeepMind diz que os agentes de prova não podem escrever nessa cópia retida. O verificador também verifica axiomas permitidos e reproduz a prova em um novo kernel. As emendas de especificação propostas seguem um processo revisado separado, enquanto os humanos permanecem responsáveis pela força do alvo.

### Qual foi o veredito do The Daily Diff sobre o fluxo de trabalho de prova verificada?

O veredito do The Daily Diff foi SHIP IT. Niko enviaria o fluxo de trabalho de prova verificada porque a reivindicação aprovada permanece separada do agente que produz a resposta. Ele manteria o escopo e as suposições anexados a cada resultado. O episódio relata o artefato de prova publicado do Google sem reconstruí-lo independentemente e aprova o fluxo de trabalho dentro desses limites de evidência.

## Capítulos

- 0:00 Quem verifica uma prova de segurança de IA?
- 0:57 Como uma reivindicação se torna um alvo de prova?
- 1:39 Por que provar o binário compilado?
- 2:16 Quais propriedades de segurança sobreviveram à lacuna de implementação?
- 2:59 A especificação pode rejeitar código quebrado?
- 3:36 Uma prova correta pode responder à pergunta errada?
- 4:13 O que impede que as metas mudem?
- 4:53 Eu usaria este fluxo de trabalho de prova?

## Transcrição traduzida

Traduzido da narração original em inglês. Áudio e legendas disponíveis são controlados pelo YouTube.

### Quem verifica uma prova de segurança de IA?

0:00 Uma auditoria de segurança de IA ainda soa como confiar em um chatbot. O novo resultado do Google sobre o Signal vem com provas matemáticas que um kernel separado verifica. Neste vídeo, o que o Google provou? E como eles impedem que um agente mude as metas? Aqui está a resposta útil. Os modelos escrevem provas candidatas, e o Lean verifica as provas contra uma reivindicação aprovada por humanos sobre código compilado selecionado. Os humanos ainda possuem a reivindicação e as suposições.

0:21 Você pode verificar o resultado sem acreditar no discurso de vitória do modelo. Uma verificação separada impede que a pergunta seja alterada silenciosamente. Vamos seguir até as definições. É terça-feira, dez de novembro, e este é The Daily Diff. AlphaProof Code é a estrutura do Google para escrever especificações de software com orientação humana e gerar provas verificadas com agentes de IA. Este estudo visa o libsignal, a biblioteca Rust que implementa o protocolo de mensagens do Signal, dentro de um programa de linha de comando específico.

0:45 O Google anunciou o trabalho hoje. Seu artigo diz que cinco pesquisadores trabalharam por quatro semanas. Os agentes escreveram as provas, enquanto os humanos dedicaram a maior parte de seu esforço às especificações. Os requisitos encontraram uma maneira de se tornar reuniões ainda mais caras. A especificação diz o que o programa deve fazer,

### Como uma reivindicação se torna um alvo de prova?

0:59 o que um atacante controla e quais suposições o argumento precisa. Os revisores perguntam se ele captura a segurança que as pessoas se importam. Uma resposta lindamente verificada a uma pergunta fraca deixa essa pergunta intacta. A equipe se baseia em pesquisas anteriores sobre o handshake do Signal e seu mecanismo de "ratchet" de chave de mensagem. Análises formais já estudaram esses designs. A reivindicação do Google conecta seus argumentos de segurança a uma biblioteca de produção não modificada implementação compilada, onde o design precisa sobreviver ao contato com código real. O diretor de tecnologia do Signal, Ehren Kret,

1:27 descreve uma expansão além dos escopos menores de verificação anteriores. Detalhes de implementação incluem mensagens fora de ordem e sessões arquivadas para mensagens atrasadas. O software real guarda os recibos que seu diagrama elegante jogou fora. Os pesquisadores compilam a biblioteca Rust não modificada com o compilador padrão

### Por que provar o binário compilado?

1:41 em um executável Arm de sessenta e quatro bits para Linux. Seus teoremas descrevem esse binário usando um modelo de instrução formal, atravessando a lacuna entre o código fonte e o código de máquina otimizado. Um erro do compilador que quebra uma propriedade declarada tornaria seu teorema falso. O compilador, portanto, sai da base confiável para este binário. Você ainda confia no modelo de instrução e no verificador do Lean. O limite de confiança mudou e tem um endereço. Cerca de seis milhões e meio de linhas de prova verificada repousam sobre aproximadamente vinte e seis

2:06 mil linhas de especificação e semântica de instrução confiáveis. Estes são contagens de artefatos. Tratá-los como pontuações de inteligência é como classificar desenvolvedores pelo tamanho de sua pasta de módulos node.

### Quais propriedades de segurança sobreviveram à lacuna de implementação?

2:16 Os argumentos cobrem confidencialidade e autenticação de mensagens, com sigilo de encaminhamento e segurança pós-comprometimento sob modelos declarados. Os dois últimos descrevem limites para danos por chaves roubadas e recuperação após novas trocas. Cada garantia tem condições sobre o atacante e a sessão. Primitivas criptográficas ficam por trás de contratos confiáveis. A prova assume que essas rotinas se comportam conforme especificado e depende de suposições de segurança criptográficas. Uma prova idealiza a criptografia; a outra raciocina sobre probabilidades de sucesso do atacante.

2:42 Ambos têm restrições sobre os cenários que cobrem. Pergunte qual "build", qual propriedade e quais suposições. Este resultado diz respeito ao "harness" de linha de comando dos pesquisadores. Mensagens em grupo são trabalho futuro, e o modelo computacional exclui o estado de vários dispositivos. Chamar cada instalação do Signal de livre de bugs sai do teorema. Os pesquisadores reintroduziram dois bugs do Signal previamente corrigidos em

### A especificação pode rejeitar código quebrado?

3:02 cópias isoladas e os compilaram. Provas verificadas mostraram que esses binários violavam o teorema de segurança simbólico. Isso testou se a especificação poderia rejeitar implementações quebradas reais. Seu visto verde precisa de um teste vermelho. O Google publica as especificações e provas com instruções de verificação. O repositório diz que uma "build" limpa leva horas e memória substancial. Ler o anúncio é consideravelmente mais fácil no laptop. O modelo de hardware e os contratos confiáveis ainda precisam de revisão.

3:26 Não reconstruí o enorme artefato para este episódio. Estamos relatando o resultado publicado e seus limites. Pessoas de fora têm um caminho para inspecioná-lo, o que importa mais para mim do que outra volta da vitória da IA. Agora a armadilha.

### Uma prova correta pode responder à pergunta errada?

3:36 O Lean pode aceitar uma prova correta de uma afirmação que pede quase nada. Suposições impossíveis podem tornar um teorema vazio. Alterar uma definição enterrada sob o teorema principal pode enfraquecer o objetivo. O artigo projeta verificações contra isso. O guardião mantém uma especificação aprovada separada para a qual os agentes de prova não podem escrever. Eles podem propor correções por meio de um processo de emenda separado. O enfraquecimento da segurança é escalado como um bug potencial. A declaração de sucesso do provador não tem autoridade aqui.

4:00 Os humanos julgam as mudanças nas suposições confiáveis, diretamente ou por meio de sua política, e revisam as emendas após cada campanha. O julgamento de especialistas permanece em jogo. O agente pode solicitar uma atribuição diferente. Ele não pode se dar uma nota de aprovação.

### O que impede que as metas mudem?

4:13 Aqui está a verificação prometida. O comparador do Lean compara o teorema e todas as definições das quais ele depende com essa cópia aprovada protegida. Ele também verifica axiomas permitidos e reproduz a prova em um novo kernel. Enfraquecer silenciosamente uma definição auxiliar, portanto, altera o que está sendo comparado. Uma prova aceita tem que estabelecer o alvo aprovado. Isso ainda deixa os humanos responsáveis por escolher um alvo forte e suposições honestas. Para seu próprio fluxo de trabalho de IA, mantenha os critérios de aceitação fora das

4:37 permissões de edição do trabalhador e revise as alterações propostas separadamente. O resultado do Google torna essa separação concreta. O escritor da prova faz o trabalho; o limite de verificação decide se isso conta. Se você preferir ler isso a me ouvir dizer, o "diff" chega à sua caixa de entrada todas as manhãs, gratuitamente em the daily diff dot dev, link abaixo. Então o veredito de hoje é SHIP IT.

### Eu usaria este fluxo de trabalho de prova?

4:54 Eu enviaria este fluxo de trabalho de prova verificada porque a reivindicação aprovada permanece separada do agente que produz a resposta. Eu manteria o escopo e as suposições anexados a cada resultado. Inscreva-se, ative o sino e me diga nos comentários se você teria carimbado diferentemente. E esse é o "diff" de hoje. Sou Niko da Axrisi. Mesclar com responsabilidade.

## Fontes

- [AlphaProof Code: Verifying Signal's Security at the Machine-Code Level — technical scope, trusted base and gatekeeping](https://google-deepmind.github.io/code-verification/) — Swarat Chaudhuri and colleagues / Google DeepMind and Google
- [Introducing AlphaProof Code — November 10 announcement and attributed Signal CTO response](https://deepmind.google/blog/introducing-alphaproof-code/) — Pushmeet Kohli and Swarat Chaudhuri / Google DeepMind
- [Code-verification repository — initial commit, public artifacts and checking instructions](https://github.com/google-deepmind/code-verification) — Google DeepMind / GitHub
- [The PQXDH Key Agreement Protocol — older official specification and prior-analysis context](https://signal.org/docs/specifications/pqxdh/) — Ehren Kret and Rolfe Schmidt / Signal
- [The Double Ratchet Algorithm — Triple Ratchet section](https://signal.org/docs/specifications/doubleratchet/) — Trevor Perrin, Moxie Marlinspike and Rolfe Schmidt / Signal
- [Google DeepMind leadership — Demis Hassabis's relevant lab identity](https://deepmind.google/about/) — Google DeepMind
- [Demis Hassabis in 2025 — authentic portrait, cropped/resized/compressed and unflipped; no background removal or generated expression/detail; lab identity only, no authorship, proof writing, current reaction or endorsement](https://commons.wikimedia.org/wiki/File:Demis_Hassabis_in_2025_by_Christopher_Michel.jpg) — Christopher P. Michel / Cmichel67 / Wikimedia Commons
- [Portrait licence — CC BY-SA 4.0; attribution, adaptation disclosure and ShareAlike](https://creativecommons.org/licenses/by-sa/4.0/) — Creative Commons
- [Expanding Brain template — cropped/captioned artifact-count satire, brief transformed <=2s commentary; no benchmark, hosting licence, legal-clearance or blanket reuse claim](https://imgflip.com/memetemplate/Expanding-Brain) — Imgflip / user-uploaded meme template
- [Tom and Jerry — Boomerang Official actual animated reaction, silent resized/captioned 1.875s excerpt; brief transformed process commentary, no actual researcher or executive reaction, hosting licence, legal-clearance or blanket reuse claim](https://giphy.com/gifs/boomerangtoons-mad-upset-1gdkNV0hroZjOXSHOU) — Boomerang Official / GIPHY / Tom and Jerry
- [Boomerang GIF source link — uploader-provided provenance](https://boomtn.co/GIPHY) — Boomerang
- [AlphaProof Code discussion — attention context, anonymous opinions excluded from factual proof claims](https://news.ycombinator.com/item?id=50439193) — Hacker News
- [Code-verification licence — Apache 2.0 for Google code, third-party licences retained](https://github.com/google-deepmind/code-verification/blob/808b4b7ffef198e6a91f71ed776d641a1c236882/LICENSE) — Google / GitHub