Agentes do AlphaProof Code escreveram três milhões de linhas de provas em Lean para verificar a criptografia central da Signal.
O que aconteceu: Agentes do AlphaProof Code, desenvolvido pela Google DeepMind, escreveram 3 milhões de linhas de provas em Lean para validar a criptografia central do aplicativo Signal.
Contexto: O avanço representa um marco na verificação formal de softwares complexos, usando técnicas de prova automática em larga escala.
Por que importa: Pode elevar a segurança de aplicativos críticos no Brasil, como os de mensageria, ao permitir verificação rigorosa de código.
O que acompanhar: Observar a adoção dessa técnica em outros projetos de software aberto ou comercial.